Combining LLM Code Generation with Formal Specifications and Reactive Program Synthesis
This addresses the need for reliable code generation in high-risk applications, though it appears incremental as it builds on existing LLM and formal methods techniques.
The paper tackles the problem of LLMs struggling with accuracy and verification in code generation for complex systems by combining LLM code generation with formal specifications and reactive program synthesis, showing that their method solves problems previously intractable for LLMs.
In the past few years, Large Language Models (LLMs) have exploded in usefulness and popularity for code generation tasks. However, LLMs still struggle with accuracy and are unsuitable for high-risk applications without additional oversight and verification. In particular, they perform poorly at generating code for highly complex systems, especially with unusual or out-of-sample logic. For such systems, verifying the code generated by the LLM may take longer than writing it by hand. We introduce a solution that divides the code generation into two parts; one to be handled by an LLM and one to be handled by formal methods-based program synthesis. We develop a benchmark to test our solution and show that our method allows the pipeline to solve problems previously intractable for LLM code generation.