mlsanityData to 14 Oct 2026

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

arXiv 2412.06176 ↗First posted 9 Dec 2024cs.LG cs.AIcited by 35

On the map: Synthetic data and self-improvement for LLMs → Code and instruction data synthesis

Abstract (arXiv)

Automated code generation with large language models has gained significant traction, but there remains no guarantee on the correctness of generated code. We aim to use formal verification to provide mathematical guarantees that the generated code is correct. However, generating formally verified code with LLMs is hindered by the scarcity of training data and the complexity of formal proofs. To tackle this challenge, we introduce AlphaVerus, a self-improving framework that bootstraps formally verified code generation by iteratively translating programs from a higher-resource language and leveraging feedback from a verifier. AlphaVerus operates in three phases: exploration of candidate translations, Treefinement -- a novel tree search algorithm for program refinement using verifier feedback, and filtering misaligned specifications and programs to prevent reward hacking. Through this iterative process, AlphaVerus enables a LLaMA-3.1-70B model to generate verified code without human intervention or model finetuning. AlphaVerus shows an ability to generate formally verified solutions for HumanEval and MBPP, laying the groundwork for truly trustworthy code-generation agents.

Key facts. Cited by 35 papers in the map (data through 14 Oct 2026). Placed in Code and instruction data synthesis, one of 13 directions in Synthetic data and self-improvement for LLMs. Builds on 41 of its 55 references that are in the map. First posted on arXiv 9 Dec 2024.

Builds on

41 of 55 references.

References · 41

  1. 2021Evaluating Large Language Models Trained on Codecited by 8,320
  2. 2022Self-Consistency Improves Chain of Thought Reasoning in Language Modelscited by 5,708
  3. 2021Program Synthesis with Large Language Modelscited by 3,637
  4. 2023Self-Refine: Iterative Refinement with Self-Feedbackcited by 3,442
  5. 2023SWE-bench: Can Language Models Resolve Real-World GitHub Issues?cited by 3,373
  6. 2023Tree of Thoughts: Deliberate Problem Solving with Large Language Modelscited by 3,211
  7. 2024Scaling LLM Test-Time Compute Optimally can be More Effective than Scaling Model Parameterscited by 1,986
  8. 2022Competition-Level Code Generation with AlphaCodecited by 1,462
  9. 2023Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generationcited by 1,391
  10. 2023Teaching Large Language Models to Self-Debugcited by 988
  11. 2023CRITIC: Large Language Models Can Self-Correct with Tool-Interactive Critiquingcited by 783
  12. 2021Asleep at the Keyboard? Assessing the Security of GitHub Copilot's Code Contributionscited by 431
29 more
  1. 2023Scaling Relationship on Learning Mathematical Reasoning with Large Language Modelscited by 427
  2. 2020Generative Language Modeling for Automated Theorem Provingcited by 388
  3. 2023Check Your Facts and Try Again: Improving Large Language Models with External Knowledge and Automated Feedbackcited by 353
  4. 2022The Effects of Reward Misspecification: Mapping and Mitigating Misaligned Modelscited by 328
  5. 2022Generating Sequences by Learning to Self-Correctcited by 277
  6. 2023FacTool: Factuality Detection in Generative AI -- A Tool Augmented Framework for Multi-Task and Multi-Domain Scenarioscited by 251
  7. 2024When Can LLMs Actually Correct Their Own Mistakes? A Critical Survey of Self-Correction of LLMscited by 240
  8. 2022Do Users Write More Insecure Code with AI Assistants?cited by 192
  9. 2024Sycophancy to Subterfuge: Investigating Reward-Tampering in Large Language Modelscited by 178
  10. 2022Formal Mathematics Statement Curriculum Learningcited by 142
  11. 2024From Decoding to Meta-Generation: Inference-time Algorithms for Large Language Modelscited by 137
  12. 2022A Survey of Deep Learning for Mathematical Reasoningcited by 124
  13. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 119
  14. 2023Let's Sample Step by Step: Adaptive-Consistency for Efficient Reasoning and Coding with LLMscited by 115
  15. 2023Self-Edit: Fault-Aware Code Editor for Code Generationcited by 111
  16. 2023RL4F: Generating Natural Language Feedback with Reinforcement Learning for Repairing Model Outputscited by 105
  17. 2024Easy-to-Hard Generalization: Scalable Alignment Beyond Human Supervisioncited by 96
  18. 2023Can ChatGPT replace StackOverflow? A Study on Robustness and Reliability of Large Language Model Code Generationcited by 73
  19. 2018Reinforcement Learning of Theorem Provingcited by 69
  20. 2024Lean-STaR: Learning to Interleave Thinking and Provingcited by 68
  21. 2023Clover: Closed-Loop Verifiable Code Generationcited by 67
  22. 2024Towards AI-Assisted Synthesis of Verified Dafny Methodscited by 58
  23. 2024A Survey on Deep Learning for Theorem Provingcited by 57
  24. 2023Verus: Verifying Rust Programs using Linear Ghost Types (extended version)cited by 53
  25. 2024AutoVerus: Automated Proof Generation for Rust Codecited by 49
  26. 2023Large Language Models and Simple, Stupid Bugscited by 45
  27. 2024Automated Proof Generation for Rust Code via Self-Evolutioncited by 33
  28. 2024Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programmingcited by 20
  29. 2024miniCodeProps: a Minimal Benchmark for Proving Code Propertiescited by 18

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2024: 1; 2025: 16; 2026: 18.

35 papers.

Sort:

By area:

  1. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 81
  2. 2025Efficient Test-Time Scaling via Self-Calibrationcited by 75
  3. 2025VERINA: Benchmarking Verifiable Code Generationcited by 34
  4. 2026Reward Hacking in the Era of Large Models: Mechanisms, Emergent Misalignment, Challengescited by 33
  5. 2025CLEVER: A Curated Benchmark for Formally Verified Code Generationcited by 29
  6. 2025Autoformalization in the Era of Large Language Models: A Surveycited by 21
  7. 2025A benchmark for vericoding: formally verified program synthesiscited by 20
  8. 2025A Comprehensive Survey on Benchmarks and Solutions in Software Engineering of LLM-Empowered Agentic Systemcited by 15
  9. 2025VeriCoder: Enhancing LLM-Based RTL Code Generation through Functional Correctness Validationcited by 13
  10. 2025Propose, Solve, Verify: Self-Play Through Formal Verificationcited by 13
  11. 2025VeruSAGE: A Study of Agent-Based Verification for Rust Systemscited by 12
  12. 2025ProofWright: Towards Agentic Formal Verification of CUDAcited by 9
23 more
  1. 2025RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generationcited by 4
  2. 2025Towards Repository-Level Program Verification with Large Language Modelscited by 4
  3. 2026Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systemscited by 4
  4. 2025Can LLMs Enable Verification in Mainstream Programming?cited by 3
  5. 2025Robust Heuristic Algorithm Design with LLMscited by 3
  6. 2026Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalizationcited by 3
  7. 2026Intent-aligned Formal Specification Synthesis via Traceable Refinementcited by 2
  8. 2026Certified Program Synthesis with a Multi-Modal Verifiercited by 2
  9. 2026Verifier-Guided Code Translation via Meta-Step Decodingcited by 2
  10. 2026Provably Complete Generalized Planning with LLMscited by 1
  11. 2025LLM-Based Config Synthesis requires Disambiguationcited by 0
  12. 2025SoK: Understanding (New) Security Issues Across AI4Code Use Casescited by 0
  13. 2026Can LLMs Reason Like Automated Theorem Provers for Rust Verification? VCoT-Bench: Evaluating via Verification Chain of Thoughtcited by 0
  14. 2026ANCORA: Learning to Question via Manifold-Anchored Self-Play for Verifiable Reasoningcited by 0
  15. 2026The Prover Is the Judge: Verified Security Software from AI Coding Agents in Ada/SPARKcited by 0
  16. 2026An AI Approach to Verified Production Cryptographic Librariescited by 0
  17. 2026Assurance Envelopes for Autonomous Coding Agents: Minimum-Cost Evidence for Software Changecited by 0
  18. 2026Djinnlang: Higher-Level Programming by Unambiguous Specification with an LLM in the Compilercited by 0
  19. 2026OSFoundry: Building and Evolving Operating Systems with Specification-Guided Agentscited by 0
  20. 2026From Verification Failures to Reusable Guidance for Coding Agentscited by 0
  21. 2026Self-Spec Verifiable Code Generationcited by 0
  22. 2026TLA-Verus: Generating and Solving Temporal Proof Obligations with LLM Agentscited by 0
  23. 2026claimcheck: Measuring and Improving Specification Faithfulnesscited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2026P3: Joint Program-and-Proof Planning for Verified Code Generation
  2. 2026WybeCoder: Verified Imperative Code Generation
  3. 2026SWE-Proof: Can Language Models Resolve Real-World Issues with Machine-Checked Proofs?
  4. 2026Automating Formal Verification with Agent-Guided Tree Search
  5. 2026AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms
  6. 2026AxDafny: Agentic Verified Code Generation in Dafny
  7. 2025VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code
  8. 2026Consistency Meets Verification: Enhancing Test Generation Quality in Large Language Models Without Ground-Truth Solutions