AlphaVerus
A model translates programs into Verus, tree search repairs them with verifier feedback, and a filter keeps trustworthy results as examples.
The loop
- Proposes
Verus translations of programs (from Dafny) and repaired versions, from a Llama 3.1 70B model
- Judged by
The Verus verifier, plus a filter that rejects translations whose specification or program is misaligned
- Steers
Treefinement tree search fixes errors from verifier feedback; verified, filtered programs become prompt examples
Headline result
With Llama 3.1 70B and no model fine-tuning, verified-code generation reaches 32.9% on HumanEval-Verus and 65.7% on MBPP-verified (pass@256), versus 27.1% and 35.9% for GPT-4o and 11.8% and 26.9% for Llama 3.1 70B.
What this does not prove
HumanEval-Verus and MBPP-verified are small, hand-adapted benchmarks, and the task is generating code plus proofs from specifications. Verification proves code matches the specification, so the misalignment filter matters.
How it generalizes the harness
- A domain authority judges
- Search over a population
- The output outlives the model
- An infallible formal kernel
Verus judges validity, a tree of candidate repairs is searched, and a built-in filter guards against the model gaming the verifier.
Classification
| What it proposes | Program |
|---|---|
| Generative model | Llama 3.1 70B (frozen, no fine-tuning) |
| Algorithmic authority | Verus verifier with a misalignment filter |
| Feedback | Verifier errors |
| What gets updated | Prompt context and search tree |
| When it runs | At inference time |
| Validity | Formal (machine-checked) |
| Evidence | Experiments reported |
| Lineage | Original system |