Lemur: Integrating Large Language Models in Automated Program Verification
Fuente:
arXiv
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2023
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866916221834756096 |
|---|---|
| author | Wu, Haoze Barrett, Clark Narodytska, Nina |
| author_facet | Wu, Haoze Barrett, Clark Narodytska, Nina |
| contents | The demonstrated code-understanding capability of LLMs raises the question of whether they can be used for automated program verification, a task that demands high-level abstract reasoning about program properties that is challenging for verification tools. We propose a general methodology to combine the power of LLMs and automated reasoners for automated program verification. We formally describe this methodology as a set of transition rules and prove its soundness. We instantiate the calculus as a sound automated verification procedure and demonstrate practical improvements on a set of synthetic and competition benchmarks. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2310_04870 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Lemur: Integrating Large Language Models in Automated Program Verification Wu, Haoze Barrett, Clark Narodytska, Nina Formal Languages and Automata Theory Artificial Intelligence Machine Learning Logic in Computer Science The demonstrated code-understanding capability of LLMs raises the question of whether they can be used for automated program verification, a task that demands high-level abstract reasoning about program properties that is challenging for verification tools. We propose a general methodology to combine the power of LLMs and automated reasoners for automated program verification. We formally describe this methodology as a set of transition rules and prove its soundness. We instantiate the calculus as a sound automated verification procedure and demonstrate practical improvements on a set of synthetic and competition benchmarks. |
| title | Lemur: Integrating Large Language Models in Automated Program Verification |
| topic | Formal Languages and Automata Theory Artificial Intelligence Machine Learning Logic in Computer Science |
| url | https://arxiv.org/abs/2310.04870 |