PaperlayerView exact revision on arXiv

Source-linked AI summary

VERINA: Benchmarking Verifiable Code Generation

Zhe Ye, Zhengxu Yan, Jingxuan He, Timothe Kasriel, Kaiyu Yang, Dawn Song

arXiv:2505.23135v3cs.LGcs.AIcs.LOcs.PLcs.SE

TL;DR

Existing benchmarks often assess only individual parts of verifiable code generation, leaving a gap in holistic evaluation. VERINA provides a modular Lean benchmark for code, specification, and proof generation and their combinations; evaluation finds proof generation especially difficult for current models.

  • Problem

    Existing benchmarks often focus on individual components rather than comprehensively evaluating code, specification, and proof generation and their combinations.

    Source: §1 · pp. 1–2

  • Method

    VERINA is a manually curated benchmark of 189 Lean tasks with descriptions, reference code, specifications, and test suites, supporting modular evaluation of individual tasks and combinations.

    Source: §1 · p. 2, §4.2 · p. 8

  • Results

    Proof generation is the most challenging task across models; OpenAI o3 achieved 4.9% successful proof in one trial.

    Source: §1 · p. 2, §5 · p. 8

  • Takeaways & Limitations

    VERINA provides a rigorous evaluation framework and directions toward more reliable, formally verified automated programming systems.

    Source: §6 · p. 10

    VERINA’s 189 examples are modest in size and emphasize simple standalone problems that do not fully represent complex real-world verification projects.

    Source: §6 · p. 10

Abstract

from arXiv · show

Large language models (LLMs) are increasingly integrated in software development, but ensuring correctness in LLM-generated code remains challenging and often requires costly manual review. Verifiable code generation -- jointly generating code, specifications, and proofs of code-specification alignment -- offers a promising path to address this limitation and further unleash LLMs' benefits in coding. Yet, there exists a significant gap in evaluation: current benchmarks often focus on only individual components rather than providing a holistic evaluation framework of all tasks. In this paper, we introduce VERINA (Verifiable Code Generation Arena), a high-quality benchmark enabling a comprehensive and modular evaluation of code, specification, and proof generation as well as their compositions. VERINA consists of 189 manually curated coding tasks in Lean, with detailed problem descriptions, reference implementations, formal specifications, and extensive test suites. Our extensive evaluation of state-of-the-art LLMs reveals significant challenges in verifiable code generation, especially in proof generation, underscoring the need for improving LLM-based theorem provers in verification domains. The best model, OpenAI o3, achieves a 72.6\% code correctness rate, 52.3\% for specification soundness and completeness, and a mere 4.9\% proof success rate (based on one trial per task). We hope VERINA will catalyze progress in verifiable code generation by providing a rigorous and comprehensive benchmark. We release our dataset on https://huggingface.co/datasets/sunblaze-ucb/verina and our evaluation code on https://github.com/sunblaze-ucb/verina.

1 INTRODUCTION

VERINA addresses the lack of benchmarks that evaluate code, specification, and proof generation both individually and in combination. Its evaluation finds that current models, especially on proof generation, remain challenged by these tasks.

1 INTRODUCTION

  • Existing benchmarks lack comprehensive support for all three tasks, quality control, robust metrics, or modular design, despite the need to evaluate their combinations.Source: §1 · pp. 1–2
  • VERINA is a Lean benchmark of 189 programming challenges with descriptions, code, specifications, proofs, and comprehensive test suites.Source: §1 · p. 2
  • The benchmark manually inspects and revises samples, and its test suites include positive and negative cases with 100% code coverage that passes the ground-truth specification.Source: §1 · p. 2
  • VERINA evaluates code with pass@k and tests, checks proofs with the Lean compiler, and scores specification soundness and completeness through theorem proving and testing.Source: §1 · p. 2
  • OpenAI o3 achieved 72.6% correct code solutions, 52.3% sound and complete specifications, and 4.9% successful proof in one trial.The best theorem-proving model, Goedel Prover V2 32B, achieved an 11.2% proof success rate in one trial.Source: §1 · p. 2
  • Iterative refinement with Lean compiler feedback raised proof success to 20.1% after 64 steps, but significantly increased costs and still yielded a low success rate.Source: §1 · p. 3

2 BACKGROUND AND RELATED WORK

Prior benchmarks often address only parts of verifiable code generation, or lack compositional evaluation and human validation. VERINA combines all three foundational tasks in Lean with modular evaluation.

Task support for verifiable code generation

  • Many benchmarks target only code, proof, or specification generation, leaving other elements to human users; VERINA covers all three tasks in Lean.Source: §2 · pp. 3–4
  • Dafny-Synthesis and Clover cover all three tasks but use automated theorem proving and have 50 and 62 human-written samples, respectively, versus VERINA’s 189 manually validated samples.Source: §2 · p. 3

Automated and interactive theorem proving

  • Lean’s interactive proofs expose intermediate steps, enabling LLMs to diagnose errors, learn from unsuccessful steps, and iteratively refine proofs.Source: §2 · p. 3

Task compositionality

  • VERINA’s modular design evaluates individual tasks and combinations, whereas prior works such as Dafny-Synthesis and Clover combine specification and proof generation into one task.Source: §2 · p. 4

3 VERINA: DATA FORMAT, CONSTRUCTION, AND QUALITY ASSURANCE

VERINA comprises 189 standalone Lean programs with natural-language descriptions, code, specifications, optional proofs, and test cases. Its construction combines manual review and automated checks to support quality and coverage.

3.1 OVERVIEW AND DATA FORMAT

  • The 189 standalone Lean programs pair a natural-language problem description with reference code, formal specifications, and test cases.Source: §3.1 · p. 4
  • Specifications contain pre-conditions on valid inputs and post-conditions describing the desired input-output relationship; ground-truth proofs are optional for evaluation.The authors manually wrote proofs for 46 of 189 examples to support quality assurance.Source: §3.1 · p. 4
  • Test suites combine positive and negative cases, with negative cases violating either the pre-condition or post-condition.Source: §3.1 · p. 4
  • Each instance has a median of 5 positive tests and 12 negative tests; descriptions have a median length of 110 words, while code reaches 38 lines and specifications 62 lines.Source: §3.1 · p. 4, Table 2 · p. 4

3.2 BENCHMARK CONSTRUCTION AND QUALITY ASSURANCE

  • The benchmark combines 49 manually translated MBPP-DFY-50 problems, 59 CloverBench instances translated with o3-mini and manually corrected, and 81 selected student submissions.Source: §3.2 · p. 5
  • Positive tests were expanded to achieve 100% line coverage on Lean ground-truth code, and ground-truth implementations and specifications passed their respective positive tests.Source: §3.2 · p. 5
  • At least three negative tests were created per positive case, except for Boolean-output functions, and specifications were designed so they could not directly yield a trivial implementation.Source: §3.2 · p. 5
  • At least two authors manually reviewed each instance, while descriptions were expanded to clarify intent, input types, and output requirements.Source: §3.2 · p. 5

4 EVALUATING VERIFIABLE CODE GENERATION USING VERINA

VERINA evaluates code, specification, and proof generation individually and in flexible combinations. Its specification metrics combine formal reasoning with comprehensive testing to assess soundness and completeness.

4 EVALUATING VERIFIABLE CODE GENERATION USING VERINA

  • VERINA covers code, specification, and proof generation, plus combinations that support evaluation from natural-language requirements through verified code.The benchmark is designed to represent multiple development workflows through modular task combinations.Source: §4 · pp. 5–6, §4.2 · pp. 7–8

4.1 FOUNDATIONAL TASKS AND METRICS

  • CodeGen is scored with pass@k, ProofGen proofs are checked by Lean, and SpecGen evaluates soundness and completeness of generated specifications.Specification evaluation first attempts theorem proving, then tests relationships against comprehensive test suites when proof is inconclusive.Source: §4.1 · pp. 6–7

4.2 TASK COMBINATIONS

  • Combined workflows include specification-guided coding, specification inference from code, and end-to-end generation of code, specification, and proof.For end-to-end generation, the proof must verify the generated code against the ground-truth specification, preventing equivalent generated code and specifications from trivializing verification.Source: §4.2 · p. 8

5 EXPERIMENTAL EVALUATION

Across the foundational tasks, code generation performs best and proof generation is hardest; proof remains a bottleneck in end-to-end generation. Lean verifier feedback and ground-truth specifications improve selected task results.

5 EXPERIMENTAL EVALUATION

  • ProofGen has pass@1 below 4.9% for all general-purpose models, while code generation generally performs best and specification generation follows.The authors identify proof generation as a bottleneck for combined tasks involving proofs.Source: §5 · pp. 8–9, Figure 5 · p. 8
  • 41.2% is o3’s Code&Spec Score, while o4-mini and o3 achieve only 3.2% on the End-to-End Score.The End-to-End Score additionally requires a correct proof verifying generated code against the ground-truth specification.Source: §5 · p. 9, Figure 6 · p. 9
  • Goedel Prover V2 32B and DeepSeek Prover V2 7B outperform general-purpose models on proof success, and Copra improves over direct single-pass generation.Copra uses o4-mini as its backbone and allows at most 64 LLM queries per sample.Source: §5 · p. 9, Figure 7 · p. 9
  • Iterative proof refinement outperforms direct generation at matched query budgets across general-purpose and proof-specific models.In refinement, models receive Lean verifier error messages and revise their proofs.Source: §5 · p. 9, Figure 8 · p. 9
  • Ground-truth specifications consistently improve CodeGen, whereas ground-truth code yields minimal or negative improvement for SpecGen.Replacing ground-truth artifacts with LLM-generated artifacts generally degrades performance.Source: §5 · p. 10, Figure 9 · p. 10

6 CONCLUSION AND DISCUSSION

VERINA provides a curated Lean benchmark and evaluation framework for verifiable code generation. Its scope is limited by modest size, standalone problems, and reliance on Lean.

6 CONCLUSION AND DISCUSSION

  • VERINA contains 189 curated examples with task descriptions, Lean code and specifications, and extensive tests with full line coverage.The benchmark supports systematic assessment of multiple verifiable code-generation capabilities.Source: §6 · p. 10
  • The 189-example dataset is modest, and its simple standalone problems do not fully represent complex real-world verification projects.The authors note that scaling the dataset for fine-tuning may require automated annotation with LLM assistance.Source: §6 · p. 10
  • VERINA currently uses Lean; extending it to ATP-based systems such as Dafny or Verus could strengthen generalizability but requires significant effort.The authors also note a risk of data contamination because underlying task topics come from widely used sources.Source: §6 · p. 10

ETHICS STATEMENT

The authors report compliance with relevant dataset licenses and the ICLR Code of Ethics.

ETHICS STATEMENT

  • The authors state that they adhere to the ICLR Code of Ethics.They refer readers to Appendix C.1 for details.Source: ETHICS STATEMENT · p. 11
  • All data used in the work are publicly available and collected for academic research purposes.The authors state that data collection included proper citation and attribution.Source: ETHICS STATEMENT · p. 11
  • The authors report compliance with relevant dataset licenses and proper citation and attribution.License details are provided in Appendix C.1.Source: ETHICS STATEMENT · p. 11

REPRODUCIBILITY STATEMENT

VERINA’s supplementary discussion documents reproducibility materials and explains why Lean is relevant to production verification and how its evaluation challenges extend to ATP systems.

REPRODUCIBILITY STATEMENT

  • The code, benchmark dataset, and evaluation pipelines are included in supplementary materials with setup and usage instructions.The paper directs readers to Sections 3.2 and 4 and the appendix for construction, metrics, and experimental details.Source: REPRODUCIBILITY STATEMENT · p. 11

A EXTENDED DISCUSSION ON THE USE OF LEAN IN VERINA

  • Lean is used beyond mathematics in production verification, including cloud authorization, Armv8 simulation, randomized algorithms, Rust verification, and Ethereum contracts.The discussion cites AWS’s Cedar and SampCert, LNSym, Aeneas, and Clear as examples.Source: A EXTENDED DISCUSSION ON THE USE OF… · p. 16
  • The authors argue that VERINA’s code and specification tasks transfer to ATP because both paradigms require correct code and sound, complete specifications.For proof generation, they point to shared reasoning about properties such as loop invariants and LLM guidance when SMT automation fails.Source: A EXTENDED DISCUSSION ON THE USE OF… · p. 16
  • Lean’s dependent type system supports higher-order functions and specifications beyond the expressiveness of SMT-based ATP specifications.The paper presents this greater expressiveness as a reason VERINA’s insights can extend beyond Lean-specific details.Source: A EXTENDED DISCUSSION ON THE USE OF… · p. 16

B EXTENDED DISCUSSION ON DATA CONTAMINATION ANALYSIS

The authors examine direct and indirect contamination risks from algorithmic familiarity, then specify licensing and use constraints for the benchmark.

B EXTENDED DISCUSSION ON DATA CONTAMINATION ANALYSIS

  • Zero 10-gram overlaps were found between VERINA’s Lean solutions and the examined 550-million-row BigCode/The Stack dataset.The authors interpret this result as evidence against direct contamination from that public pretraining corpus.Source: B EXTENDED DISCUSSION ON DATA… · pp. 16–17
  • The authors argue that algorithmic familiarity does not transfer to specification and proof generation, limiting indirect contamination concerns.They contrast code-generation and proof-generation success rates as evidence that memorized algorithms do not imply formal reasoning about them.Source: B EXTENDED DISCUSSION ON DATA… · p. 17

C.1 LICENSE

  • VERINA’s dataset is licensed under GPL-3.0, and the authors say the collected LeetCode materials are publicly available and used for academic research only.The paper states that no model training or fine-tuning is involved.Source: §C.1 · p. 17

C.2 MODEL CONFIGURATIONS AND COMPUTE

The appendix reports model settings and prompting choices, then contrasts VERINA’s task coverage and specification evaluation with CLEVER.

C.2 MODEL CONFIGURATIONS AND COMPUTE

  • All evaluated models used temperature 1.0 and a 10,000-token output budget; three prover models ran locally on eight NVIDIA H100 80GB GPUs.Table 3 presents configurations and costs; other models were accessed through APIs, with costs reported.Source: §C.2 · p. 17, Table 3 · p. 17

C.3 PROMPTS

  • Models received consistent 2-shot prompts, with five responses per problem used to calculate pass@1; specialized prover prompts avoided instruction-following failures in two models.The two prover models produced 0% success with the standard DSPy prompts because their output formats were unparsable.Source: §C.3 · p. 18

C.4 COMPARISON WITH CLEVER

  • VERINA covers code, specification, and proof generation plus their combinations, while CLEVER omits code generation, proof generation, specification inference from code, and end-to-end verification.The comparison table summarizes which tasks each benchmark supports.Source: §C.4 · p. 23, Table 4 · p. 23
  • CLEVER’s specification evaluation assumes a sound, complete ground-truth specification; VERINA instead combines proving and testing to assess specification quality when proofs are inconclusive.The authors argue that requiring ground truth limits CLEVER’s fit to scenarios where developers already have a specification.Source: §C.4 · p. 23

C.5 IMPLEMENTATION OF EVALUATION METRICS IN LEAN

The appendix details Lean implementations of the code, specification, and proof evaluations, and reports that testing can provide useful specification assessments when LLM provers are inconclusive.

C.5 IMPLEMENTATION OF EVALUATION METRICS IN LEAN

  • Generated code is evaluated on Lean 4 #guard unit tests, while generated proofs are checked by the Lean compiler and filtered for placeholders.Figure 10 illustrates the code-evaluation harness.Source: §C.5 · p. 24, Figure 10 · p. 24
  • Specification evaluation first tries proof with LLM-based provers, then tests generated specifications on suite examples when proving is inconclusive.The Lean implementation checks decidable relationships with decide before using plausible property-based testing.Source: §C.5 · p. 24
  • The test-based checks map precondition soundness and completeness to positive and negative tests, and postcondition soundness and completeness to negative and positive tests, respectively.These mappings rely on the benchmark’s verified ground-truth preconditions and postconditions passing positive tests and failing negative tests.Source: §C.5 · p. 24
  • Below 4% proof success across all cases contrasted with more than 40% of generated specifications judged sound and complete by testing.Successful proofs always agreed with testing; manual inspection of 20 randomly selected disagreements found testing correct in each case.Source: §C.5 · p. 24, Table 5 · p. 25
  • LLM provers are unreliable as a specification-evaluation metric when inconclusive rates are high, while testing can identify sound and complete specifications in those cases.The authors note that successful proofs still provide formal guarantees, and expect stronger provers to improve the metric over time.Source: §C.5 · pp. 24–25

D ADDITIONAL EXPERIMENTAL EVALUATION RESULTS

The additional experiments expose difficulty differences across VERINA subsets and tasks, and show that refinement, code summaries, and proof-generation strategies have uneven effects. Failure analyses further identify persistent specification and Lean-proof challenges.

VERINA-A and VERINA-B

Specification generation

Code-summary ablation

Proof refinement

Refinement and COPRA

Proof length

  • Human-written proofs average 169.6 characters, whereas Gemini 2.5 Flash’s successful proofs exceed 1,200 characters after 64 refinement iterations.Figure 16 compares average proof length; inspection found models often prove intermediate goals instead of using relevant library lemmas and automation tactics.Source: D ADDITIONAL EXPERIMENTAL EVALUATION… · p. 28, Figure 16 · p. 29

Detailed performance breakdown

  • Syntax errors and nonexistent library functions are major problems, while unknown specification-evaluation cases are reported as uncertainty bounds rather than definitive failures.Preconditions tend to be simpler and have lower unknown rates than postconditions; complex postconditions produce more unknown cases.Source: D ADDITIONAL EXPERIMENTAL EVALUATION… · p. 29

Proof failure analysis

  • Across four top-performing models, incomplete proofs account for 77.55% of Gemini 2.5 Flash failures and 38.24% of GPT 4.1 failures; cheat codes account for 48.53% of Claude Sonnet 3.7 failures and 28.30% of o4-mini failures.Unknown identifiers, tactics, and constants account for 15–30% of failures across models, indicating recurring Lean syntax and library-familiarity problems.Source: D ADDITIONAL EXPERIMENTAL EVALUATION… · pp. 29–30

E CASE STUDIES OF MODEL FAILURES AND EVALUATION METRICS

Case studies show how code errors, incomplete or unsound specifications, and difficult-to-evaluate postconditions can undermine verifiable code generation. One proof example reaches a correct strategy after repeated compiler-feedback refinement; the authors also describe their limited, supervised use of LLMs.

E CASE STUDIES OF MODEL FAILURES AND EVALUATION METRICS

F USE OF LLM

  • LLMs assisted with translating 59 CloverBench Dafny instances and polishing presentation, while authors inspected, corrected, and verified translations.LLMs were not used for research ideation, experimental design, dataset selection, or analysis.Source: F USE OF LLM · p. 40
Loading 2505.23135v3…