mlsanityData to 7 Oct 2026

Proving the Coding Interview: A Benchmark for Formally Verified Code Generation

arXiv 2502.05714 ↗First posted 8 Feb 2025cs.SE cs.AI cs.LGcited by 18

Not on the map. Why?

Abstract (arXiv)

We introduce the Formally Verified Automated Programming Progress Standards, or FVAPPS, a benchmark of 4715 samples for writing programs and proving their correctness, the largest formal verification benchmark, including 1083 curated and quality controlled samples. Previously, APPS provided a benchmark and dataset for programming puzzles to be completed in Python and checked against unit tests, of the kind seen in technical assessments in the software engineering industry. Building upon recent approaches for benchmarks in interactive theorem proving, we generalize the unit tests to Lean 4 theorems given without proof (i.e., using Lean's "sorry" keyword). On the 406 theorems of 100 randomly selected samples, Sonnet correctly proves 30% and Gemini correctly proves 18%. We challenge the machine learning and program synthesis communities to solve both each general purpose programming problem and its associated correctness specifications. The benchmark is available at https://huggingface.co/datasets/quinn-dougherty/fvapps.

Key facts. Cited by 18 papers in the map (data through 7 Oct 2026). Builds on 22 of its 35 references that are in the map. First posted on arXiv 8 Feb 2025.

Builds on

22 of 35 references.

References · 22

  1. 2024The Llama 3 Herd of Modelscited by 14,192
  2. 2021Evaluating Large Language Models Trained on Codecited by 8,053
  3. 2021Program Synthesis with Large Language Modelscited by 3,509
  4. 2023SWE-bench: Can Language Models Resolve Real-World GitHub Issues?cited by 3,193
  5. 2023Code Llama: Open Foundation Models for Codecited by 2,105
  6. 2024LiveCodeBench: Holistic and Contamination Free Evaluation of Large Language Models for Codecited by 1,906
  7. 2024Chatbot Arena: An Open Platform for Evaluating LLMs by Human Preferencecited by 1,151
  8. 2024DeepSeek-V2: A Strong, Economical, and Efficient Mixture-of-Experts Language Modelcited by 1,093
  9. 2024OpenHands: An Open Platform for AI Software Developers as Generalist Agentscited by 956
  10. 2021Measuring Coding Challenge Competence With APPScited by 879
  11. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  12. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 225
10 more
  1. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 189
  2. 2020DreamCoder: Growing generalizable, interpretable knowledge with wake-sleep Bayesian program learningcited by 159
  3. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
  4. 2019Learning to Prove Theorems via Interacting with Proof Assistantscited by 107
  5. 2021NaturalProofs: Mathematical Theorem Proving in Natural Languagecited by 80
  6. 2023Clover: Closed-Loop Verifiable Code Generationcited by 62
  7. 2024Towards AI-Assisted Synthesis of Verified Dafny Methodscited by 58
  8. 2024DafnyBench: A Benchmark for Formal Software Verificationcited by 54
  9. 2024AutoVerus: Automated Proof Generation for Rust Codecited by 46
  10. 2023CodeFusion: A Pre-trained Diffusion Model for Code Generationcited by 31

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2025: 9; 2026: 9.

18 papers.

Sort:

By area:

  1. 2025VERINA: Benchmarking Verifiable Code Generationcited by 30
  2. 2025CLEVER: A Curated Benchmark for Formally Verified Code Generationcited by 27
  3. 2025A benchmark for vericoding: formally verified program synthesiscited by 16
  4. 2025From Code Foundation Models to Agents and Applications: A Comprehensive Survey and Practical Guide to Code Intelligencecited by 13
  5. 2025VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Codecited by 7
  6. 2025Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verificationcited by 6
  7. 2026VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Leancited by 6
  8. 2026Neural Theorem Proving for Verification Conditions: A Real-World Benchmarkcited by 4
  9. 2025Benchmarking AI Models in Software Engineering: A Review, Search Tool, and Unified Approach for Elevating Benchmark Qualitycited by 3
  10. 2025A Case Study on the Effectiveness of LLMs in Verification with Proof Assistantscited by 3
  11. 2026VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generationcited by 1
  12. 2026Unlocking LLM Code Correction with Iterative Feedback Loopscited by 1
6 more
  1. 2026P3: Joint Program-and-Proof Planning for Verified Code Generationcited by 1
  2. 2026Vero: Can AI Agents Build Formally Verified Software Repositories?cited by 1
  3. 2025Holistic Evaluation of State-of-the-Art LLMs for Code Generationcited by 0
  4. 2026VeriScale: Adversarial Test-Suite Scaling for Verifiable Code Generationcited by 0
  5. 2026FVSpec: Real-World Property-Based Tests as Lean Challengescited by 0
  6. 2026Self-Spec Verifiable Code Generationcited by 0