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

TL;DR

FVAPPS addresses the challenge of producing both correct code and its formal verification by pairing coding tasks with Lean 4 theorems expressed with the placeholder 'sorry'. The authors build a benchmark of $4715$ Lean 4 files (including $1083$ quality-controlled samples) derived from APPS and implement a five-stage scaffolding pipeline that allows placeholders to enable compilation while evaluating proof-amenable solutions. In baseline experiments on $406$ theorems from $100$ samples, Sonnet proved $30\%$ and Gemini $18\%$, illustrating the gap between code generation and formal proof capabilities and highlighting directions for future proof-oriented program synthesis. FVAPPS thus provides a formal verification benchmark that fosters progress toward automated, verified programming for critical software domains.

Abstract

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.

Figures (10)

• Figure 1: Benchmark generation pipeline for creating coding interview theorem statements in Lean from APPS questions and solutions.
• Figure 2: FVAPPS sample 23, derived from train sample 23 of APPS source. The def is where the solver implements the function, each theorem is a correctness specification.
• Figure 3: Our generic scaffolding loop used at various stages of our pipeline. The run element is replaced with the python, pytest, lean, or lake build executable respectively.
• Figure 4: Total number of defs and theorems across FVAPPS samples.
• Figure 5: Human baseline's solution to the definition for sample 23 of FVAPPS (helper recursor omitted for brevity, available on GitHub)