Lemur: Integrating Large Language Models in Automated Program Verification

“Lemur: Integrating Large Language Models in Automated Program Verification” by Haoze Wu, Clark Barrett, and Nina Narodytska. In The Twelfth International Conference on Learning Representations (ICLR '24), May 2024. Vienna, Austria.

Abstract

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 derivation rules and prove its soundness. We instantiate the calculus as a sound automated verification procedure, which led to practical improvements on a set of synthetic and competition benchmarks.

BibTeX entry:

@inproceedings{WCB24,
   author = {Haoze Wu and Clark Barrett and Nina Narodytska},
   title = {Lemur: Integrating Large Language Models in Automated Program
	Verification},
   booktitle = {The Twelfth International Conference on Learning
	Representations (ICLR '24)},
   month = may,
   year = {2024},
   note = {Vienna, Austria},
   url = {https://openreview.net/forum?id=Q3YaCghZNt}
}

(This webpage was created with bibtex2web.)