Combining LLM Code Generation with Formal Specifications and Reactive Program Synthesis
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866916455702855680 |
|---|---|
| author | Murphy, William Holzer, Nikolaus Qiao, Feitong Cui, Leyi Rothkopf, Raven Koenig, Nathan Santolucito, Mark |
| author_facet | Murphy, William Holzer, Nikolaus Qiao, Feitong Cui, Leyi Rothkopf, Raven Koenig, Nathan Santolucito, Mark |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_19736 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Combining LLM Code Generation with Formal Specifications and Reactive Program Synthesis Murphy, William Holzer, Nikolaus Qiao, Feitong Cui, Leyi Rothkopf, Raven Koenig, Nathan Santolucito, Mark Software Engineering Machine Learning Logic in Computer Science 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. |
| title | Combining LLM Code Generation with Formal Specifications and Reactive Program Synthesis |
| topic | Software Engineering Machine Learning Logic in Computer Science |
| url | https://arxiv.org/abs/2410.19736 |