[zero_k]

Yes, we should use LLMs to translate human requirements that are ambiguous and have a lot of hidden assumptions (e.g. that football matches should preferably be at times when people are not working & awake [3]), and use them to create formal requirements, e.g. generating SMT [1] or ASP [2] queries. Then the formal methods tool, e.g. Z3/cvc5 or clingo can solve these now formal queries. Then we can translate back the solution to human language via the LLM. This does not solve some problems, e.g. the LLM not correctly guessing the implicit requirements. But it does go around a bunch of issues.

We do need to pump up the jam when it comes to formal methods tools, though. And academia is still rife with quantum and AI buzzword generators if you wanna get funding. Formal methods doesn't get enough funding from Academia. Amazon has put a bunch of money into it (hiring all good talent :sadface:), and Microsoft is funding both Z3 and Lean4. Industry is ahead of the game, again. This is purely failure of Academic leadership, nothing else.

[1] https://en.wikipedia.org/wiki/Satisfiability_modulo_theories

[2] https://en.wikipedia.org/wiki/Answer_set_programming

[3] Anecdotal, but this was a "bug" in a solution offered by a tool that optimally schedules football matches in Spain.

[dmonitor]

> Yes, we should use LLMs to translate human requirements that are ambiguous and have a lot of hidden assumptions (e.g. that football matches should preferably be at times when people are not working & awake [3]), and use them to create formal requirements

Why would an LLM trained on human language patterns be good at this? If anything, I would expect it to follow the same pattern that humans do.

[zero_k]

It doesn't need to be good at solving the problem. It only needs to be good at translating the problem of "If the unknown x is divided by 3 it has the same value as if I subtracted 9 from it" into "x/3 == x-9 && x is an Real number". The formal method tool will do the rest.

Note that if the LLM gets the implicit assumptions wrong, the solution will be unsatisfactory, and the query can be refined. This is exactly what happens with actual human experts, as per the anecdote I shared in [3]. So the LLM can replace some of the human-in-the-loop that makes it so hard to use formal methods tools. Humans are good at explaining the problem in human language, but have difficulty formulating them in ways that a formal tool can deal with. Humans, i.e. consultants, help with formalizing them in e.g. SMT. We could skip some of that, and make formal methods tools much more accessible.

[croes]

Your example isn't ambiguous and if it was LLMs won't be better in choosing the right interpretation.

[wakawaka28]

The problem is not that writing input for formal method tools is tricky syntactically. The problem is that it is hard to produce the actual semantic content of the input. Humans don't need help with that, especially not the kind of human that is capable of authoring that content. It's much more technical than stuff like "Make me a website with a blue background" or some crap like that. The potential for an LLM to mistranslate the English input is probably unacceptable.

[zero_k]

Correction, Lean4 [1] is sponsored by Amazon, the lead developer, Leonardo de Moura is at AWS now [2]. He was previously at Microsoft Research [3]. Meeting him is a real ride, I only had the chance to talk with him once.

[1] https://lean-lang.org/

[2] https://leodemoura.github.io/about.html

[3] https://www.microsoft.com/en-us/research/blog/the-inner-magi...