paper-with-me

홈 › Papers

Combining LLM Code Generation with Formal Specifications and Reactive Program Synthesis

2024-09-18 · William Murphy, Nikolaus Holzer, Feitong Qiao, Leyi Cui, Raven Rothkopf, Nathan Koenig, Mark Santolucito

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.

📄 PDF Abstract BibTeX arXiv:2410.19736

Code (0)

등록된 구현이 없습니다.

Tasks

Code GenerationProgram Synthesis

Similar Papers 제목 키워드 기반

Iterative Circuit Repair Against Formal Specifications

2023-03-02 · Matthias Cosler, Frederik Schmitt, Christopher Hahn, Bernd Finkbeiner

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 Learning

Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models

2026-05-14 · Frederik Schmitt, Matthias Cosler, Niklas Metzger, Julian Siber 외 arxiv

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

2026-03-12 · Liao Zhang, Tong Chen, Xiwei Wu, Qi Liu 외 arxiv

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

2025-01-27 · Daniel Neider, Rajarshi Roy

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 SearchSurvey

The Challenges in Specifying and Explaining Synthesized Implementations of Reactive Systems

2019-01-03 · Hadas Kress-Gazit, Hazem Torfah

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…