Elamur Research⌕
☰
home / papers / 2024 / AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement

AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement

Paper · 2024 · Pranjal Aggarwal, Bryan Parno and Sean Welleck

Summary

Code produced by large language models comes with no correctness guarantee, and the usual checks (unit tests, human review) are weak stand-ins. Verification-aware languages such as Verus, which targets Rust, can prove that a program meets its specification for every input. However, models rarely manage to write such code, mainly because almost no Verus training data exists. AlphaVerus tackles this bootstrapping problem by translating programs from Dafny, an older and better-resourced verification language, into Verus. Each iteration has three steps:

  • Exploration: sample many candidate translations and keep those that partially verify.
  • Treefinement: repair the candidates with a tree search in which nodes are complete programs and edges are fixes guided by verifier feedback.
  • Critique: models discard translations whose specifications are trivial, incomplete or exploited, which limits reward hacking.

Successful trajectories become few-shot exemplars for the next round. The pipeline therefore improves using only Llama-3.1-70B, with no human input or fine-tuning. The collected exemplars let the model write full verified implementations, including code and proofs, for HumanEval and MBPP specifications. This points toward trustworthy code generation in a mainstream language.

Key points

  • Source data is DafnyBench (562 Dafny programs). The pipeline produces the DAFNY2VERUS-COLLECTION, which contains translated Verus programs, error-correction pairs and critique examples.
  • Motivation: Verus has fewer than 10 public repositories, while Rust has millions of code examples.
  • With AlphaVerus exemplars, a Llama-70B model solves 33% of Verified-HumanEval and outperforms GPT-4o-based methods. The authors report this as the first non-zero result on a verified HumanEval.
  • Compared with the concurrent SAFE++, AlphaVerus needs no month-long GPT-4 initialization and uses about 100× less data. Its tree-based refinement also beats SAFE++'s linear refinement.
  • Ablations show that every component (exploration, Treefinement, critique) is necessary. Code is available at alphaverus.github.io.

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

 Fields, topics and concepts

📚 Shelves 4The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksInformation Systems · 1,888 worksComputer Science Applications · 184 works

🧭 Topics 1Research subjects and languages the work is about.Code & programming languages · 194 works

Cite

Cite as Pranjal Aggarwal, Bryan Parno and Sean Welleck. 2024. AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement. arXiv:2412.06176.

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

@misc{aggarwal2024alphaverus,
  title = {{AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement}},
  author = {Pranjal Aggarwal, Bryan Parno and Sean Welleck},
  year = {2024},
  doi = {10.48550/arxiv.2412.06176},
  eprint = {2412.06176},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2412.06176}
}

References

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

  1. Denison, C., MacDiarmid, M., Barez, F., Duvenaud, D., Kravec, S., Marks, S., Schiefer, N., Soklaski, R., Tamkin, A., Kaplan, J., Shlegeris, B., Bowman, S. R., Perez, E., and Hubinger, E. Sycophancy to subterfuge: Investigating reward-tampering in large language models. https://arxiv.org/abs/2406.10… ↗
  2. Aggarwal, P., Madaan, A., Yang, Y., and Mausam. Let’s sample step by step: Adaptive-consistency for efficient reasoning and coding with llms, 2023. URL https://arxiv.org/abs/2305.11860. ↗
  3. Akyürek, A. F., Akyürek, E., Madaan, A., Kalyan, A., Clark, P., Wijaya, D., and Tandon, N. Rl4f: Generating natural language feedback with reinforcement learning for repairing model outputs. arXiv preprint arXiv:2305.08844, 2023.
  4. Elgedawy, R., Sadik, J., Dutta, S., Gautam, A., Georgiou, K., Gholamrezae, F., Ji, F., Lim, K., Liu, Q., and Ruoti, S. Occasionally secure: A comparative analysis of code generation assistants. https://arxiv.org/abs/ 2402.00689, 2024. ↗
  5. Austin, J., Odena, A., Nye, M., Bosma, M., Michalewski, H., Dohan, D., Jiang, E., Cai, C., Terry, M., Le, Q., et al. Program synthesis with large language models. https://arxiv.org/abs/2108.07732, 2021. ↗
  6. First, E., Brun, Y., and Guha, A. Tactok: semantics-aware proof synthesis. Proc. ACM Program. Lang., 4 (OOPSLA), Nov 2020. doi: 10.1145/3428299. URL https://doi.org/10.1145/3428299. — [doi:10.1145/3428299](https://doi.org/10.1145/3428299) ↗
  7. Chakraborty, S., Ebner, G., Bhat, S., Fakhoury, S., Fatima, S., Lahiri, S., and Swamy, N. Towards neural synthesis for smt-assisted proof-oriented programming. https://arxiv.org/abs/2405.01787, 2024. ↗
  8. First, E., Rabe, M., Ringer, T., and Brun, Y. Baldur: Whole-proof generation and repair with large language models. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2023, pp. 1229–1241, New York, NY, USA,…
  9. Chen, M., Tworek, J., Jun, H., Yuan, Q., de Oliveira Pinto, H. P., Kaplan, J., Edwards, H., Burda, Y., Joseph, N., Brockman, G., Ray, A., Puri, R., Krueger, G., Petrov, M., Khlaaf, H., Sastry, G., Mishkin, P., Chan, B., Gray, S., Ryder, N., Pavlov, M., Power, A., Kaiser, L., Bavarian, M., Winter, C.… — CRITIC: Large Language Models Can Self-Correct with Tool-Interactive Critiquing
  10. Hendler, J. Understanding the limits of AI coding. Science, 379(6632):548–548, 2023. find
  11. Hosseini, A., Yuan, X., Malkin, N., Courville, A., Sordoni, A., and Agarwal, R. V-star: Training verifiers for self-taught reasoners, 2024. URL https://arxiv.org/ abs/2402.06457. ↗
  12. Isabelle. de/. Isabelle. https://isabelle.in.tum. Jesse, K., Ahmed, T., Devanbu, P., and Morgan, E. Large language models and simple, stupid bugs. 2023 IEEE/ACM 20th International Conference on Mining Software Repositories (MSR), pp. 563–575, 2023. URL https://api.semanticscholar. org/CorpusID:25763… ↗
  13. Jimenez, C. E., Yang, J., Wettig, A., Yao, S., Pei, K., Press, O., and Narasimhan, K. Swe-bench: Can language models resolve real-world GitHub issues? ArXiv, abs/2310.06770, 2023. URL https://api.semanticscholar.org/CorpusID: 263829697. ↗
  14. Li, R., Allal, L. B., Zi, Y., Muennighoff, N., Kocetkov, D., Mou, C., Marone, M., Akiki, C., Li, J., Chim, J., Liu, Q., Zheltonozhskii, E., Zhuo, T. Y., Wang, T., Dehaene, O., Davaadorj, M., Lamy-Poirier, J., Monteiro, J., Shliazhko, O., Gontier, N., Meade, N., Zebaze, A., Yee, M.-H., Umapathi, L. K… find
  15. Li, Y., Choi, D., Chung, J., Kushman, N., Schrittwieser, J., Leblond, R., Eccles, T., Keeling, J., Gimeno, F., Lago, A. D., Hubert, T., Choy, P., de Masson d’Autume, C., Babuschkin, I., Chen, X., Huang, P.-S., Welbl, J., Gowal, S., Cherepanov, A., Molloy, J., Mankowitz, D. J., Robson, E. S., Kohli,… — Competition-Level Code Generation with AlphaCode
  16. Kaliszyk, C., Urban, J., Michalewski, H., and Olšák, M. Reinforcement learning of theorem proving. In Proceedings of the 32nd International Conference on Neural Information Processing Systems, NIPS’18, pp. 8836–8847, Red Hook, NY, USA, 2018. Curran Associates Inc.
  17. Kamoi, R., Zhang, Y., Zhang, N., Han, J., and Zhang, R. When can LLMs actually correct their own mistakes? A critical survey of self-correction of LLMs. Transactions of the Association for Computational Linguistics, 12:1417–1440, 2024. doi: 10.1162/tacl a 00713. URL https://aclanthology.org/ 2024.ta… ↗
  18. Li, Y., Choi, D., Chung, J., Kushman, N., Schrittwieser, J., Leblond, R., Tom, Eccles, Keeling, J., Gimeno, F., Lago, A. D., Hubert, T., Choy, P., de, C., d’Autume, M., Babuschkin, I., Chen, X., Huang, P.-S., Welbl, J., Gowal, S., Alexey, Cherepanov, Molloy, J., Mankowitz, D. J., Robson, E. S., Kohl… — Competition-Level Code Generation with AlphaCode
  19. Langley, P. Crafting papers on machine learning. In Langley, P. (ed.), Proceedings of the 17th International Conference on Machine Learning (ICML 2000), pp. 1207–1216, Stanford, CA, 2000. Morgan Kaufmann. find
  20. Lattuada, A., Hance, T., Cho, C., Brun, M., Subasinghe, I., Zhou, Y., Howell, J., Parno, B., and Hawblitzel, C. Verus: Verifying Rust programs using linear ghost types. Proc. ACM Program. Lang., 7(OOPSLA1), April 2023. doi: 10.1145/3586037. URL https://doi.org/10. 1145/3586037. — [doi:10.1145/3586037](https://doi.org/10.1145/3586037) find
  21. Li, Z., Sun, J., Murphy, L., Su, Q., Li, Z., Zhang, X., Yang, K., and Si, X. A survey on deep learning for theorem proving. In First Conference on Language Modeling, 2024. URL https://openreview.net/forum? id=zlw6AHwukB. https:// ↗
  22. Lin, H., Sun, Z., Yang, Y., and Welleck, S. Lean-star: Learning to interleave thinking and proving. https://arxiv.org/abs/2407.10040, 2024. ↗
  23. Leino, K. R. M. Dafny: An automatic program verifier for functional correctness. In Proceedings of the Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), 2010. find
  24. Liu, J., Xia, C. S., Wang, Y., and Zhang, L. Is your code generated by chatGPT really correct? rigorous evaluation of large language models for code generation. In Thirty-seventh Conference on Neural Lean FRO. Lean theorem prover. leanprover.github.io/.
  25. Information Processing Systems, 2023. URL https://openreview.net/forum?id=1qvx610Cu7. ↗
  26. Lohn, E. and Welleck, S. minicodeprops: a minimal benchmark for proving code properties. https://arxiv.org/abs/2406.11915, 2024. — [arXiv:2406.11915](https://arxiv.org/abs/2406.11915) ↗
  27. Loughridge, C., Sun, Q., Ahrenbach, S., Cassano, F., Sun, C., Sheng, Y., Mudide, A., Misu, M. R. H., Amin, N., and Tegmark, M. Dafnybench: A benchmark for formal software verification, 2024. URL https://arxiv.org/abs/2406.08467. ↗
  28. Perry, N., Srivastava, M., Kumar, D., and Boneh, D. Do users write more insecure code with ai assistants? In Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security, CCS ’23. find
  29. ACM, November 2023. doi: 10.1145/3576915.3623157. URL http://dx.doi.org/10.1145/3576915. 3623157. — [doi:10.1145/3576915.3623157](https://doi.org/10.1145/3576915.3623157) ↗
  30. Polu, S. and Sutskever, I. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020.
  31. Polu, S., Han, J. M., Zheng, K., Baksys, M., Babuschkin, I., and Sutskever, I. Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344, 2022.
  32. Lu, P., Qiu, L., Yu, W., Welleck, S., and Chang, K.-W. A survey of deep learning for mathematical reasoning. In Rogers, A., Boyd-Graber, J., and Okazaki, N. (eds.), Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pp. 14605–14631, Toron… find
  33. Redmon, J. and Sanchez-Stern, A. Proverbot 9000 : Neural networks for proof assistance, 2016. URL https://api.semanticscholar.org/CorpusID: 11622595. ↗
  34. Rozière, B., Gehring, J., Gloeckle, F., Sootla, S., Gat, I., Tan, X. E., Adi, Y., Liu, J., Sauvestre, R., Remez, T., Rapin, J., Kozhevnikov, A., Evtimov, I., Bitton, J., Bhatt, M., Ferrer, C. C., Grattafiori, A., Xiong, W., Défossez, A., Copet, J., Azhar, F., Touvron, H., Martin, L., Usunier, N.,… — Code Llama: Open Foundation Models for Code
  35. Madaan, A., Tandon, N., Gupta, P., Hallinan, S., Gao, L., Wiegreffe, S., Alon, U., Dziri, N., Prabhumoye, S., Yang, Y., Gupta, S., Majumder, B. P., Hermann, K., Welleck, S., Yazdanbakhsh, A., and Clark, P. Self-refine: Iterative refinement with self-feedback. In Thirty-seventh Conference on Neural I… find
  36. Misu, M. R. H., Lopes, C. V., Ma, I., and Noble, J. Towards ai-assisted synthesis of verified dafny methods. Proceedings of the ACM on Software Engineering, 1 (FSE):812–835, July 2024. ISSN 2994-970X. doi: 10.1145/3643763. URL http://dx.doi.org/10. 1145/3643763.
  37. Pan, A., Bhatia, K., and Steinhardt, J. The effects of reward misspecification: Mapping and mitigating misaligned models. In International Conference on Learning Representations, 2022. URL https://openreview.net/forum?id=JYtwGwIL7ye. ↗
  38. Schick, T., Dwivedi-Yu, J., Dessı̀, R., Raileanu, R., Lomeli, M., Zettlemoyer, L., Cancedda, N., and Scialom, T. Toolformer: Language models can teach themselves to use tools, 2023. URL https://arxiv.org/abs/ 2302.04761. ↗
  39. Snell, C., Lee, J., Xu, K., and Kumar, A. Scaling llm test-time compute optimally can be more effective than scaling model parameters, 2024. URL https://arxiv.org/abs/2408.03314. ↗
  40. Sun, C., Sheng, Y., Padon, O., and Barrett, C. Clover: Closed-loop verifiable code generation. https://arxiv.org/abs/2310.17807, 2023. ↗
  41. Pearce, H. A., Ahmad, B., Tan, B., Dolan-Gavitt, B., and Karri, R. Asleep at the keyboard? Assessing the security of GitHub Copilot’s code contributions. 2022 IEEE Symposium on Security and Privacy (SP), pp. 754–768, 2021. URL https://api.semanticscholar.org/CorpusID:245220588. ↗
  42. Sun, Z., Yu, L., Shen, Y., Liu, W., Yang, Y., Welleck, S., and Gan, C. Easy-to-hard generalization: Scalable alignment beyond human supervision. In The Thirty-eighth Annual Conference on Neural Information Processing Systems, 2024. URL https://openreview.net/forum? id=qwgfh2fTtN. ↗
  43. Peng, B., Galley, M., He, P., Cheng, H., Xie, Y., Hu, Y., Huang, Q., Liden, L., Yu, Z., Chen, W., et al. Check your facts and try again: Improving large language models with external knowledge and automated feedback. arXiv preprint arXiv:2302.12813, 2023.
  44. Swamy, N., Hriţcu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P.-Y., Kohlweiss, M., Zinzindohoué, J.-K., and Zanella-Béguelin, S. Dependent types and multi-monadic effects in F*. 2016. ISBN 978-1-4503-3549-2. find
  45. Team, Q. Qwen2.5: A party of foundation models. https://qwenlm.github.io/blog/qwen2.5/, September 2024. ↗
  46. Yuan, Z., Yuan, H., Li, C., Dong, G., Lu, K., Tan, C., Zhou, C., and Zhou, J. Scaling relationship on learning mathematical reasoning with large language models, 2023. URL https://arxiv.org/abs/2308.01825. ↗
  47. The HumanEval-Verus Contributors. Humaneval-verus: Hand-written examples of verified verus code derived from humaneval, 2024. URL https://github.com/secure-foundations/ human-eval-verus.git. ↗
  48. Zelikman, E., Wu, Y., Mu, J., and Goodman, N. D. Star: Bootstrapping reasoning with reasoning, 2022. URL https://arxiv.org/abs/2203.14465. ↗
  49. Zhang, K., Li, Z., Li, J., Li, G., and Jin, Z. Self-edit: Fault-aware code editor for code generation. arXiv preprint arXiv:2305.04087, 2023.
  50. Wang, T., Kulikov, I., Golovneva, O., Yu, P., Yuan, W., Dwivedi-Yu, J., Pang, R. Y., Fazel-Zarandi, M., Weston, J., and Li, X. Self-taught evaluators, 2024. URL https://arxiv.org/abs/2408.02666. ↗
  51. Zheng, L., Yin, L., Xie, Z., Sun, C., Huang, J., Yu, C. H., Cao, S., Kozyrakis, C., Stoica, I., Gonzalez, J. E., Barrett, C., and Sheng, Y. Sglang: Efficient execution of structured language model programs, 2024. URL https://arxiv.org/abs/2312.07104. ↗
  52. Wang, X., Wei, J., Schuurmans, D., Le, Q., Chi, E., Narang, S., Chowdhery, A., and Zhou, D. Self-consistency improves chain of thought reasoning in language models. arXiv preprint arXiv:2203.11171, 2022.
  53. Zhong, L. and Wang, Z. Can llm replace stack overflow? a study on robustness and reliability of large language model code generation. In AAAI Conference on Artificial Intelligence, 2023. URL https://api.semanticscholar.org/CorpusID: 261048682. ↗
  54. Welleck, S., Lu, X., West, P., Brahman, F., Shen, T., Khashabi, D., and Choi, Y. Generating sequences by learning to self-correct. In The Eleventh International Conference on Learning Representations, 2023. URL https://openreview.net/forum? id=hH36JeQZDaO. ↗
  55. Welleck, S., Bertsch, A., Finlayson, M., Schoelkopf, H., Xie, A., Neubig, G., Kulikov, I., and Harchaoui, Z. From decoding to meta-generation: Inference-time algorithms for large language models. Transactions on Machine Learning Research, 2024. ISSN 2835-8856. URL https://openreview.net/forum? id=es… ↗
  56. Wu, Y., Sun, Z., Li, S., Welleck, S., and Yang, Y. An empirical analysis of compute-optimal inference for problem-solving with language models. https://arxiv.org/abs/2408.00724, 2024a. ↗
  57. Wu, Y., Sun, Z., Li, S., Welleck, S., and Yang, Y. Inference scaling laws: An empirical analysis of compute-optimal inference for problem-solving with language models. arXiv preprint arXiv:2408.00724, 2024b.
  58. Yang, C., Li, X., Misu, M. R. H., Yao, J., Cui, W., Gong, Y., Hawblitzel, C., Lahiri, S., Lorch, J. R., Lu, S., Yang, F., Zhou, Z., and Lu, S. AutoVerus: Automated proof generation for Rust code, 2024. URL https://arxiv.org/abs/2409.13082. ↗
  59. Yao, S., Yu, D., Zhao, J., Shafran, I., Griffiths, T. L., Cao, Y., and Narasimhan, K. Tree of thoughts: deliberate problem solving with large language models. In Proceedings of the 37th International Conference on Neural Information Processing Systems, NIPS ’23, Red Hook, NY, USA, 2024. Curran Assoc… find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/aggarwal-2024-alphaverus-bootstrapping-formally-verified-code/