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

Probably not a substantial claim: may not pass S3 (load-bearing).

Various refinement strategies use external feedback from knowledge bases, code interpreters, tool outputs, or separately trained reward models.

“Various refinement strategies use external feedback from knowledge bases (Peng et al., 2023;Chern et al., 2023), code interpreters (Chen et al., 2023;Zhang et al., 2023), tool outputs (Gou et al., 2024;Schick et al., 2023), or separately trained reward models (Akyürek et al., 2023).”

• cites Peng et al., 2023 sourceSupported
• cites Chen et al., 2023 sourceSupported
• cites Akyürek et al., 2023 sourceDisputed

  The citation is attached to the claim about separately trained reward models. Section 3 (Background; page unavailable) says RL4F trains a separate critique generator to provide natural-language feedback while leaving the task model unchanged. The Learning via Policy Gradient section describes reward as a computed similarity metric, not feedback from a separately trained reward model. (LLM, conf=0.88)

  Checked by a reasoning model — may be wrong.

  Experimental — accuracy not yet measured

Probably not a substantial claim: may not pass S3 (load-bearing).

Existing baseline methods for proof annotations in Verus lack contamination analysis.

“Notably, existing baseline methods for proof annotations in Verus (Yang et al., 2024;Chen et al., 2024) lack such contamination analysis.”

• cites Yang et al., 2024 sourceDisputed

  The paper does not lack contamination analysis: its “General threats to validity” section explicitly considers whether the LLM had seen benchmark tasks in training data. It examines the public availability of Verus proofs and the baseline LLM’s performance on potentially leaked tutorial tasks. The analysis is qualitative, but it directly contradicts the claim that none was conducted. (LLM, conf=0.87)

  Checked by a reasoning model — may be wrong.

  Experimental — accuracy not yet measured
• cites Chen et al., 2024Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

May combine two claims.

Generating formally verified code with LLMs is hindered by the scarcity of training data and the complexity of formal proofs.

“However, generating formally verified code with LLMs is hindered by the scarcity of training data and the complexity of formal proofs.”

• cites Sun et al., 2023 sourcePartly supported

  Appendix A.4.5 attributes GPT-4’s difficulty with current Dafny syntax to likely limited training data, supporting the data-scarcity point in that specific setting. The Introduction identifies the need for human expertise in writing formal specifications as the main obstacle; it says the proof step can often be automated, so it does not support formal-proof complexity as the obstacle claimed. (LLM, conf=0.86)

  Experimental — accuracy not yet measured
• cites Lohn & Welleck, 2024Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

May combine two claims.

These methods have achieved significant success in proving complex mathematical theorems, but their application to formal verification of code is typically limited to theorems from existing projects or simple program properties rather than end-to-end verified code generation.

“While these methods have achieved significant success in proving complex mathematical theorems, their application to formal verification of code is typically limited to theorems from existing projects (e.g., First et al. (2023)) or simple program properties (Lohn & Welleck, 2024) rather than end-to-end verified code generation.”

• cites First et al. (2023) sourceSupported
• cites Lohn & Welleck, 2024Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing).

Recent studies have shown that increasing inference-time compute can improve performance in reasoning, mathematics, and code generation via meta-generation strategies such as parallel sampling, tree search, and refinement.

“Recent studies have shown that increasing inference-time compute can improve performance in reasoning, mathematics, and code generation via meta-generation strategies (Welleck et al., 2024) such as parallel sampling (Wang et al., 2022;Aggarwal et al., 2023;Sun et al., 2024), tree search (Yao et al., 2024;Wu et al., 2024a), and refinement (Welleck et al., 2023;Madaan et al., 2023;Snell et al., 2024”

• cites Welleck et al., 2024Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites Wang et al., 2022 sourceSupported
• cites Yao et al., 2024Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing).

Automated formal verification has a long-standing history in interactive theorem provers.

“Automated formal verification has a long-standing history in interactive theorem provers”

• cites Redmon & Sanchez-Stern, 2016Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites Kaliszyk et al., 2018Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites Polu & Sutskever, 2020 sourceSupported

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

SAFE++ proposes translating an existing Rust dataset to Verus and training generation and refinement models on the collected data.

“Second, the concurrent work SAFE++ (Chen et al., 2024) proposes translating an existing Rust dataset to Verus and training generation and refinement models on the collected data.”

• cites Chen et al., 2024 sourcePartly supported

  The Introduction and §4.1 say the paper translates programs from existing datasets into Verus-compatible Rust and uses the resulting data for training. Section 3.3 describes joint training for proof generation and self-debugging, rather than separate generation and refinement models. The paper calls the framework SAFE and its self-debugging variant SAFE+, not SAFE++. (LLM, conf=0.87)

  Experimental — accuracy not yet measured

Classified as probably not a substantial claim.

AutoVerus prompts GPT-4 with a pipeline of hand-engineered prompts tailored to specific errors and programs.

“First, AutoVerus (Yang et al., 2024) prompts GPT-4 with a pipeline of hand-engineered prompts tailored to specific er-rors and programs.”

• cites Yang et al., 2024 sourceSupported

Probably not a substantial claim: may not pass S3 (load-bearing).

An alternative paradigm integrates language models with languages that offload proving to automated reasoning tools (e.g., SMT), including Dafny and F*.

“An alternative paradigm integrates language models with languages that offload proving to automated reasoning tools (e.g., SMT), including Dafny (Leino, 2010;Sun et al., 2023;Loughridge et al., 2024) and F* (Swamy et al., 2016;Chakraborty et al., 2024).”

• cites Leino, 2010 sourceNot checked — no full text of the source
• cites Sun et al., 2023 sourceSupported
• cites Loughridge et al., 2024Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing).

Various algorithms aim to improve a language model using data generated by the model along with an external feedback source, termed self-improvement.

“Various algorithms aim to improve a language model using data generated by the model along with an external feedback source (Zelikman et al., 2022;Wang et al., 2024;Hosseini et al., 2024), which is colloquially termed self-improvement.”

• cites Zelikman et al., 2022 sourceSupported
• cites Wang et al., 2024Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites Hosseini et al., 2024 sourceSupported

Probably not a substantial claim: may not pass S3 (load-bearing).

Common approaches rely on variants of expert iteration or rejection finetuning, where multiple solutions are sampled, and an external signal selects positive ones for model fine-tuning.

“Common approaches rely on variants of expert iteration or rejection finetuning (Polu et al., 2022;Zelikman et al., 2022;Yuan et al., 2023;Lin et al., 2024), where multiple solutions are sampled, and an external signal selects the positive ones for model fine-tuning.”

• cites Polu et al., 2022 sourceNot checked — no full text of the source
• cites Zelikman et al., 2022 sourcePartly supported

  The Introduction (p. 1) and §3.2 (p. 4) support filtering generated rationales by whether they lead to the correct answer and fine-tuning on the retained examples. But the claim’s description of sampling multiple solutions is not how this paper presents STaR: §5 (p. 9) describes more, higher-temperature sampling as a counterproductive alternative to its rationalization step. (LLM, conf=0.88)

  Experimental — accuracy not yet measured
• cites Yuan et al., 2023 sourceSupported

May combine two claims.

On tasks requiring array manipulation, the synthesized specification may omit conditions on the array length, which results in trivial solutions such as returning an empty array.

“This includes subtle forms of mis-specification; for instance, on tasks requiring array manipulation, the synthesized specification may omit conditions on the array length, which results in trivial solutions such as returning an empty array.”

May combine two claims.

Stochastic few-shot sampling reduces the computational cost associated with fine-tuning large models and enables other models to leverage the data pool to improve their performance without any training.

“This method reduces the computational cost associated with fine-tuning large models and, as shown in our results, enables other models to leverage the data pool to improve their performance without any training.”

May combine two claims.

AlphaVerus enables a Llama-70B model to successfully generate verified solutions to 33% of Verified-HumanEval, outperforming GPT-4o-based methods.

“We show that AlphaVerus enables a Llama-70B model to successfully generate verified solutions to 33% of Verified-HumanEval (The HumanEval-Verus Contributors, 2024), outperforming GPT-4o-based methods.”

• cites The HumanEval-Verus Contributors, 2024Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

The quote only partly states this claim.

AlphaVerus generates a Rust implementation and proof annotations that pass the verifier for a function that removes duplicates from a sorted vector while maintaining sorted order.

“AlphaVerus generates a Rust implementation and proof annotations (e.g., invariant, proof, assert statements) that pass the verifier.”

• AssumptionRests on an assumption: The Verus verifier correctly determines whether a program satisfies its specification.

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

AlphaVerus enables strong annotation performance.

“AlphaVerus enables strong annotation performance.”

Probably not a substantial claim: may not pass S3 (load-bearing).

DAFNY2VERUS-COLLECTION comprises 247 translated programs, 102 error trajectories, and 579 exploit pairs.

“The generated exemplars during the translation process are collected into our DAFNY2VERUS-COLLECTION, comprising 247 translated programs, 102 error trajectories, and 579 exploit pairs.”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

AlphaVerus translations can involve multiple specifications, helper functions, and proof annotations, and individually reach up to 100 lines of Verus code.

“In particular, the translations can involve multiple specifications, helper functions, and proof annotations, and individually reach up to 100 lines of Verus code.”

May combine two claims.

The new concepts identified across iterations start with basic syntax, then basic number theory algorithms, then mutable arrays and sets.

“Figure 9 depicts the new concepts that we identified across iterations, starting with the ability to translate basic syntax, then basic number theory algorithms, then the ability to work with mutable arrays and sets.”

May combine two claims.

Exploration plateaus while tree search continues improving as the generation budget is increased.

“Notably, exploration plateaus while tree search continues improving as the generation budget is increased.”

May combine two claims.

Even more complicated cases of reward hacking occur, such as leaving small gaps in translated specifications or generating degenerate translations.

“we see even more complicated cases of reward hacking, such as leaving small gaps in translated specifications or even generating degenerate translations, as illustrated in Figure 8.”

May combine two claims.

AlphaVerus relies only on a single openly available model, without an expensive GPT-4 initialization.

“In contrast, AlphaVerus relies only on a single openly available model, without an expensive GPT-4 initialization.”

May combine two claims.

AlphaVerus incorporates a new tree-search refinement strategy that outperforms the linear strategy used in SAFE++, and a critique phase to ensure the generated specifications are high quality.

“AlphaVerus also incorporates a new tree-search refinement strategy that outperforms the linear strategy used in SAFE++, and a critique phase to ensure the generated specifications are high quality.”

May combine two claims.

AlphaVerus outperforms both SAFE and AutoVerus on proof annotation.

“As shown in Table 4, AlphaVerus outperforms both methods.”

May combine two claims.

The agent first learns to use debug statements and uses them continuously; after fixing, it learns other hacks such as generating trivial specifications or exploring rare debug statements such as allowing infinite loops.

“In particular, the agent first learns to use debug statements and uses them continuously.After fixing, it learns other hacks such as generating trivial specifications or exploring rare debug statements such as allowing infinite loops.”

May combine two claims.

LLaMA-3.1-8B shows better cost efficiency at lower compute budgets, while LLaMA-3.1-70B shows higher asymptotic performance.

“LLaMA-3.1-8Bshows better cost efficiency at lower compute budgets, while LLaMA-3.1-70Bshows higher asymptotic performance.”

May combine two claims.

Manual analysis confirms that the GPT-4-based contamination detection approach significantly outperforms traditional n-gram analysis and aligns well with human assessment of contamination.

“Manual analysis confirms this approach significantly outperforms traditional n-gram analysis and aligns well with human assessment of contamination.”

Probably not a substantial claim: may not pass S3 (load-bearing).

The graph shows incremental progress in translation capabilities as different programming concepts are mastered.

“The graph shows the incremental progress in translation capabilities as different programming concepts are mastered.”

May combine two claims.

AlphaVerus operates without human intervention, hand-engineered prompts, or extensive computational resources, yet achieves significant performance improvements on verified versions of HumanEval and MBPP benchmarks where prior methods fail.

“Our approach operates without human intervention, hand-engineered prompts, or extensive computational resources, yet achieves significant performance improvements on verified versions of the HumanEval and MBPP benchmarks where prior methods fail.”

• AssumptionRests on an assumption: HumanEval and MBPP benchmarks are appropriate for evaluating formally verified code generation.

May combine two claims.

Performance of pass@32 continues to improve, with pass@256 leveling off.

“Performance of pass@32 continues to improve, with pass@256 leveling off.”

Probably not a substantial claim: may not pass S4 (based).

It is infeasible to train a model on (yS, yI, yP) examples since such examples do not exist.

“However, doing so raises a technical challenge: it is infeasible to train a model on (y S , y I , y P ) examples since such examples do not exist.”

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

Language features in verification-aware languages can cause programs to pass the verifier, such as writing 'assume (false)', which causes any program to pass.

“The latter can occur due to language features in verification-aware languages that cause programs to pass the verifier (such as writing”

Probably not a substantial claim: may not pass S4 (based).

The specifications themselves are not verified, as they represent the developer's intended behavior.

“The specifications themselves are not verified, as they represent the developer's intended behavior.”

May combine two claims.

Synthesized specifications are the one part of the translation pipeline that lacks formal guarantees, which can result in a mismatch between the intended and actual functionality of generated programs.

“Synthesized specifications are the one part of the translation pipeline that lacks formal guarantees, which can result in a mismatch between the intended and actual functionality of generated programs.”

Probably not a substantial claim: may not pass S3 (load-bearing).

REBASE allocates an exploration budget by sampling nodes from a distribution determined by the node scores at the current depth, providing an effective balance of exploration and exploitation.

“REBASE allocates an exploration budget by sampling nodes from a distribution determined by the node scores at the current depth, providing an effective balance of exploration and exploitation.”

• cites Wu et al., 2024bNot matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

May combine two claims.

The AlphaVerus pipeline iterates, creating a self-reinforcing cycle where verified programs and refinement trajectories improve the models' capabilities, enabling translation of increasingly complex programs.

“The pipeline iterates, creating a self-reinforcing cycle where verified programs and refinement trajectories improve the models' capabilities, enabling translation of increasingly complex programs.”

Classified as probably not a substantial claim. May combine two claims.

Dafny has been in use for over a decade, resulting in a larger set of available data.

“As our initial source domain, we consider Dafny-a language that follows a similar paradigm to Verus and has been in use for over a decade, resulting in a larger set of available data.”

Probably not a substantial claim: may not pass S4 (based).

AlphaVerus's approach specifically addresses the non-local nature of error fixes.

“Our approach specifically addresses the non-local nature of error fixes.”

Classified as probably not a substantial claim.

DafnyBench is a benchmark of 562 programs of varying difficulty.

“DafnyBench (Loughridge et al., 2024)-a benchmark of 562 programs of varying difficulty.”

• cites Loughridge et al., 2024Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S4 (based).

The collected exemplars can be used to improve the verified code generation performance of any model without any finetuning.

“Finally, the collected exemplars can be used to improve the verified code generation performance of any model without any finetuning.”

Probably not a substantial claim: may not pass S3 (load-bearing).

Treefinement can be viewed as a hybrid meta-generator that combines tree search and refinement, following initial parallel sampling (exploration).

“Our Treefinement algorithm can be viewed as a hybrid meta-generator that combines tree search and refinement, following initial parallel sampling (exploration).”

May combine two claims.

The results point to the effectiveness, flexibility, and data efficiency of AlphaVerus.

“Overall, the results point to the effectiveness of AlphaVerus, along with its flexibility and data efficiency.”

May combine two claims.

AlphaVerus was not designed for the proof annotations task, while AutoVerus has correction prompts specifically engineered for the task.

“This is notable since AlphaVerus was not designed for the proof annotations task, while AutoVerus has correction prompts specifically engineered for the task.”

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing), S4 (based).

Enabling verified code generation in these research languages may have limited applicability to real-world software and workflows.

“However, enabling verified code generation in these research languages may have limited applicability to real-world software and workflows.”

Probably not a substantial claim: may not pass S3 (load-bearing).

These approaches typically generate step-by-step proof statements for a given problem, with the theorem prover providing feedback on intermediate steps.

“These approaches typically generate step-by-step proof statements for a given problem, with the theorem prover providing feedback on intermediate steps.”

Probably not a substantial claim: may not pass S3 (load-bearing).

A variety of tree search methods generate one step of a mathematical solution at a time, with a verifier guiding the search process by assigning a score to the current state.

“A variety of tree search methods generate one step of a mathematical solution at a time, with a verifier guiding the search process by assigning a score to the current state (Wu et al., 2024a).”

• cites Wu et al., 2024aNot matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

May combine two claims.

For cost-constrained scenarios, it is preferable to use the smaller model with more samples, but the larger model has better asymptotic performance.

“In other words, for cost-constrained scenarios, it is preferable to use the smaller model with more samples, but the larger model has better asymptotic performance.”

Classified as probably not a substantial claim. May combine two claims.

AutoVerus's approach allows for refining some errors but requires human expertise to support new strategies through additional prompts.

“This allows for refining some errors but requires human expertise to support new strategies through additional prompts.”

Probably not a substantial claim: may not pass S2 (checkable).

This task is significantly more complex, as the LLM must structure the code to facilitate the completion of the proof.

“This task is significantly more complex, as the LLM must structure the code to facilitate the completion of the proof.”

Probably not a substantial claim: may not pass S3 (load-bearing).

HumanEval-Verus is sourced from a concurrent open-source effort to translate existing HumanEval programs to Verus.

“HumanEval -Verus is sourced from a concurrent open-source effort (The HumanEval-Verus Contributors, 2024) to translate existing HumanEval programs to Verus.”

• cites The HumanEval-Verus Contributors, 2024Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

May combine two claims.

These innovations contribute to better results, despite AlphaVerus using open models and 100 times less data.

“These innovations contribute to better results, despite our method using open models and 100 times less data.”

Probably not a substantial claim: may not pass S3 (load-bearing).

Verus offers a verification framework for Rust, a widely adopted programming language.

“In contrast, Verus (Lattuada et al., 2023) offers a verification framework for Rust, a widely adopted programming language.”

• cites Lattuada et al., 2023Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

May combine two claims.

Treefinement addresses the non-local nature of error fixes and does not need an additional trained scoring model.

“Our strategy addresses the non-local nature of error fixes, and does not need an additional trained scoring model.”

May combine two claims.

Treefinement uses verifier feedback on the complete solution, modeling tree nodes as full programs and edges as refinement steps.

“In contrast, Treefinement uses verifier feedback on the complete solution, modeling tree nodes as full programs and edges as refinement steps.”

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

Linear refinement variants are special cases of REBASE (depth = 1 with large breadth, and temperature = infinity).

“Also note that the linear refinement variants are special cases of REBASE (depth = 1 with large breadth, and temperature = ∞).”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

These two existing works study the simplified task of proof generation, while AlphaVerus studies the more general setting of verified code generation: generating the implementation and its proofs.

“Finally, these two existing works study the simplified task of proof generation, while we study the more general setting of verified code generation: generating the implementation and its proofs.”

May combine two claims.

SAFE used over a month of GPT-4o invocations and thousands of programs, contrasting with AlphaVerus's use of 562 Dafny programs and an openly available 70B model.

“Second, SAFE used over a month of GPT-4o invocations and thousands of programs, which contrasts with our use of 562 Dafny programs and an openly available 70B model.”

• cites SAFE (Chen et al., 2024)Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S4 (based).

There is a substantial lack of data for Verus.

“However, unlike in formal theorem proving or long-standing verification languages, there is a substantial lack of data for Verus.”

Probably not a substantial claim: may not pass S3 (load-bearing).

AlphaVerus can be viewed as a meta-generation algorithm that improves over time, rather than a model trained on filtered outputs.

“Conceptually, we can view AlphaVerus as a meta-generation algorithm (i.e., a combination of parallel sampling, refinement, and tree search) that improves over time, rather than a model trained on filtered outputs.”

Probably not a substantial claim: may not pass S2 (checkable), S4 (based).

Formal verification could play a crucial role in addressing ensuring correctness and reliability of generated code.

“Furthermore, our work suggests that formal verification could play a crucial role in addressing one of the most pressing challenges in automated code generation: ensuring the correctness and reliability of generated code.”

Probably not a substantial claim: may not pass S4 (based). May combine two claims.

AlphaVerus advances the state-of-the-art in formally verified code generation and establishes a scalable pathway for improving LLMs' capabilities in generating correct code.

“AlphaVerus advances the state-of-the-art in formally verified code generation and establishes a scalable pathway for improving LLMs' capabilities in generating correct code.”

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing).

This opens up new avenues for developing trustworthy AI-assisted programming tools.

“This opens up new avenues for developing trustworthy AI-assisted programming tools that can be safely integrated into real-world software development workflows.”

May combine two claims.

Prior methods typically operate in a linear fashion, while AlphaVerus structures refinement as a tree search.

“Moreover, whereas prior methods typically operate in a linear fashion-i.e., starting with an output and repeatedly refining it-our approach structures refinement as a tree search.”

May combine two claims.

AlphaVerus additionally uses refinement and tree search to collect data, and the data is collected using multiple modules.

“Our method additionally uses refinement and tree search to collect data, and the data is collected using multiple modules (e.g., outputs from Treefinement may be used to improve exploration).”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

The authors did not tune hyperparameters and used conventional settings throughout.

“We do not tune hyperparameters and use the conventional settings throughout.”

Probably not a substantial claim: may not pass S4 (based). May combine two claims.

AlphaVerus distills inference-time computation into a meta-generator that improves over time, showing potential for inference-time scaling in verified settings.

“Intuitively, AlphaVerus distills inference-time computation into a meta-generator that improves over time, showing the potential for inference-time scaling in verified settings.”