Current browse context:
cs.FL
Change to browse by:
References & Citations
Computer Science > Formal Languages and Automata Theory
Title: Lemur: Integrating Large Language Models in Automated Program Verification
(Submitted on 7 Oct 2023 (v1), last revised 25 Apr 2024 (this version, v5))
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 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.
Submission history
From: Haoze Wu [view email][v1] Sat, 7 Oct 2023 16:44:53 GMT (2709kb,D)
[v2] Tue, 10 Oct 2023 03:54:36 GMT (2709kb,D)
[v3] Sun, 24 Mar 2024 18:10:03 GMT (2714kb,D)
[v4] Sat, 20 Apr 2024 18:33:50 GMT (2715kb,D)
[v5] Thu, 25 Apr 2024 01:16:21 GMT (2724kb,D)
Link back to: arXiv, form interface, contact.