Elamur Research⌕
☰
home / papers / 2024 / Lemur: Integrating Large Language Models in Automated Program Verification

Lemur: Integrating Large Language Models in Automated Program Verification

Paper · 2024 · Haoze Wu, Clark Barrett and Nina Narodytska

Summary

Proving that a program meets a specification often depends on finding useful intermediate facts, such as loop invariants, and breaking the proof into smaller steps. Conventional verifiers find this kind of high-level reasoning hard to automate. The authors introduce LEMUR, a framework in which an LLM (OpenAI's GPT models) suggests candidate invariants as sub-goals and an automated verifier, such as ESBMC or UAutomizer, checks each one precisely. They formalize this collaboration as a calculus of transition rules and prove it sound. LLM suggestions count only as assumptions until the verifier confirms them as invariants, so wrong guesses cannot produce false proofs. From the calculus they derive a sound, terminating algorithm. Prompts ask the model for C assert statements at marked program lines, and proposals that turn out false or too weak are sent back to the model for repair. On synthetic benchmarks and SV-COMP competition benchmarks, LEMUR solves clearly more tasks than the standalone verifiers. By the authors' account, this is the first fully automated and provably sound integration of LLMs with formal reasoners.

Key points

  • The calculus has rules named Propose, Repair 1, Repair 2, Decide, Backtrack, Success 1, Success 2 and Fail. The LLM serves two roles: one oracle proposes new properties and another repairs earlier ones.
  • On 47 SV-COMP benchmarks with a 15-minute limit, UAutomizer and ESBMC each solved only 1 task. Extending their limit to 12 hours raised this to just 2 and 4 tasks.
  • Across three runs, LEMUR (GPT4) solved 24–25 of the 47 tasks, compared with 14–15 for LEMUR (GPT3). The choice of LLM therefore has a large effect.
  • An ablation without the repair rules, LEMUR (GPT4, NO REPAIR), solved 19–20 tasks. This shows that repairing weak or incorrect proposals contributes real gains.
  • The prompts ask the model for loop invariants or facts written as assert(...) lines. They are queried several times with different penalty settings, and the distinct answers are collected as candidate sub-goals.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓Stanford UniversityStanford · United States567 works · 335,189 citations

 Fields, topics and concepts

📚 Shelves 4The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 worksSoftware · 150 works

🧭 Topics 1Research subjects and languages the work is about.Language models & pretraining · 4,145 works

Cite

Cite as Haoze Wu, Clark Barrett and Nina Narodytska. 2024. Lemur: Integrating Large Language Models in Automated Program Verification. arXiv:2310.04870.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2310.04870 · arXiv 2310.04870

@misc{wu2024lemur,
  title = {{Lemur: Integrating Large Language Models in Automated Program Verification}},
  author = {Haoze Wu, Clark Barrett and Nina Narodytska},
  year = {2024},
  doi = {10.48550/arxiv.2310.04870},
  eprint = {2310.04870},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2310.04870}
}

References

24 references, 7 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Dirk Beyer. Competition on software verification and witness validation: Sv-comp 2023. In Sriram Sankaranarayanan and Natasha Sharygina (eds.), Tools and Algorithms for the Construction and Analysis of Systems, pp. 495–522, Cham, 2023. Springer Nature Switzerland. ISBN 978-3-031-30820-8. find
  2. Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel Ziegler, Jeffrey Wu, Clemens Winter, Chri… find
  3. Curran Associates, Inc., 2020. URL https://proceedings.neurips.cc/paper_files/paper/2020/ file/1457c0d6bfcb4967418bfb8ac142f64a-Paper.pdf. ↗
  4. Yiannis Charalambous, Norbert Tihanyi, Ridhi Jain, Youcheng Sun, Mohamed Amine Ferrag, and Lucas C. Cordeiro. A new era in software security: Towards self-healing software via large language models and formal verification, 2023. find
  5. Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Pondé de Oliveira Pinto, Jared Kaplan, Harrison Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, Alex Ray, Raul Puri, Gretchen Krueger, Michael Petrov, Heidy Khlaaf, Girish Sastry, Pamela Mishkin, Brooke Chan, Scott Gray, Nick Ryder, Mi… — Evaluating Large Language Models Trained on Code
  6. Aakanksha Chowdhery, Sharan Narang, Jacob Devlin, Maarten Bosma, Gaurav Mishra, Adam Roberts, Paul Barham, Hyung Won Chung, Charles Sutton, Sebastian Gehrmann, Parker Schuh, Kensen Shi, Sasha Tsvyashchenko, Joshua Maynez, Abhishek Rao, Parker Barnes, Yi Tay, Noam Shazeer, Vinodkumar Prabhakaran, Emi… — PaLM: Scaling Language Modeling with Pathways
  7. Edmund M Clarke, Thomas A Henzinger, Helmut Veith, Roderick Bloem, et al. Handbook of model checking, volume 10. Springer, 2018. find
  8. Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova. BERT: pre-training of deep bidirectional transformers for language understanding. In Jill Burstein, Christy Doran, and Thamar Solorio (eds.), Proceedings of the 2019 Conference of the North American Chapter of the Association for Comp…
  9. Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models. CoRR, abs/2303.04910, 2023. doi: 10.48550/arXiv.2303. 04910. URL https://doi.org/10.48550/arXiv.2303.04910. ↗
  10. Mikhail R Gadelha, Felipe R Monteiro, Jeremy Morse, Lucas C Cordeiro, Bernd Fischer, and Denis A Nicole. Esbmc 5.0: an industrial-strength c model checker. In Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, pp. 888–891, 2018. find
  11. Pranav Garg, Daniel Neider, P. Madhusudan, and Dan Roth. Learning invariants using decision trees and implication counterexamples. In Rastislav Bodı́k and Rupak Majumdar (eds.), Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersb… find
  12. ACM, 2016. doi: 10.1145/2837614.2837664. URL https://doi.org/10.1145/2837614.2837664. ↗
  13. Inc. GitHub. GitHub Copilot. https://copilot.github.com/, 2021. Accessed: September 2023. ↗
  14. Matthias Heizmann, Jürgen Christ, Daniel Dietsch, Evren Ermis, Jochen Hoenicke, Markus Lin-denmann, Alexander Nutz, Christian Schilling, and Andreas Podelski. Ultimate automizer with smtinterpol: (competition contribution). In International Conference on Tools and Algorithms for the Construction an… find
  15. Daniel Kroening and Michael Tautschnig. Cbmc–c bounded model checker: (competition contribution). In Tools and Algorithms for the Construction and Analysis of Systems: 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS… find
  16. Aitor Lewkowycz, Anders Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay V. Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, Yuhuai Wu, Behnam Neyshabur, Guy Gur-Ari, and Vedant Misra. Solving quantitative reasoning problems with language models. In NeurIPS, 2022. UR…
  17. OpenAI. Gpt-4 technical report, 2023.
  18. Kexin Pei, David Bieber, Kensen Shi, Charles Sutton, and Pengcheng Yin. Can large language models reason about program invariants? In Andreas Krause, Emma Brunskill, Kyunghyun Cho, Barbara Engelhardt, Sivan Sabato, and Jonathan Scarlett (eds.), Proceedings of the 40th International Conference on Mac… find
  19. Rahul Sharma, Saurabh Gupta, Bharath Hariharan, Alex Aiken, Percy Liang, and Aditya V. Nori. A data driven approach for algebraic loop invariants. In Matthias Felleisen and Philippa Gardner (eds.), Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of… find
  20. Springer, 2013. doi: 10.1007/978-3-642-37036-6\\ 31. URL https://doi.org/10.1007/978-3-642-37036-6_31. — [doi:10.1007/978-3-642-37036-6\](https://doi.org/10.1007/978-3-642-37036-6\) ↗
  21. Xujie Si, Aaditya Naik, Hanjun Dai, Mayur Naik, and Le Song. Code2inv: A deep learning framework for program verification. In Shuvendu K. Lahiri and Chao Wang (eds.), Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II,… find
  22. Springer, 2020. doi: 10.1007/978-3-030-53291-8\\ 9. URL https://doi.org/10.1007/ 978-3-030-53291-8_9. — [doi:10.1007/978-3-030-53291-8\](https://doi.org/10.1007/978-3-030-53291-8\) find
  23. Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Fei Xia, Ed Chi, Quoc V Le, Denny Zhou, et al. Chain-of-thought prompting elicits reasoning in large language models. Advances in Neural Information Processing Systems, 35:24824–24837, 2022.
  24. Martin White, Michele Tufano, Matias Martinez, Martin Monperrus, and Denys Poshyvanyk. Sorting and transforming program repair ingredients via deep learning code similarities. In 2019 IEEE 26th International Conference on Software Analysis, Evolution and Reengineering (SANER). IEEE, feb 2019. doi: 1… — [doi:10.1109/saner.2019.8668043](https://doi.org/10.1109/saner.2019.8668043) find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/wu-2024-lemur-integrating-large-language-models/