Combining LLM Code Generation with Formal Specifications and Reactive Program Synthesis
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.
Code (0)
등록된 구현이 없습니다.
Tasks
Code GenerationProgram SynthesisSimilar Papers 제목 키워드 기반
Iterative Circuit Repair Against Formal Specifications
We present a deep learning approach for repairing sequential circuits against formal specifications given in linear-time temporal logic (LTL). Given a defective circuit and its formal specification, we train Transformer …
Representation LearningNatural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models
Reactive synthesis, the problem of automatically constructing a hardware circuit from a logical specification, is a long-standing challenge in formal verification. It is elusive for two reasons: It is algorithmically har…
Neuro-Symbolic Generation and Validation of Memory-Aware Formal Function Specifications
Formal verification of memory-manipulating programs critically depends on precise function specifications that capture memory states written by experts. This requirement has become a major bottleneck as large language mo…
What is Formal Verification without Specifications? A Survey on mining LTL Specifications
Virtually all verification techniques using formal methods rely on the availability of a formal specification, which describes the design requirements precisely. However, formulating specifications remains a manual task …
Enumerative SearchSurveyThe Challenges in Specifying and Explaining Synthesized Implementations of Reactive Systems
In formal synthesis of reactive systems an implementation of a system is automatically constructed from its formal specification. The great advantage of synthesis is that the resulting implementation is correct by constr…