Reproduce “Proving the Coding Interview: A Benchmark for Formally Verified Code Generation” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Quinn Dougherty, Ronak Mehta
Researchers from the Beneficial AI Foundation and an independent expert introduce FVAPPS, the largest formal verification benchmark with 4715 samples (1083 quality-controlled), designed to push large language models towards generating both functional code and its mathematical proof of correctness in Lean 4. This benchmark addresses critical safety and reliability concerns of AI-generated software by providing a framework to measure progress in verified automated programming.
Key insights
- An LLM-powered iterative pipeline can efficiently generate a large-scale, high-quality formal verification benchmark by translating existing programming problems into Lean 4 specifications.
- Current large language models show nascent capabilities in proving formal correctness, performing significantly worse on theorem proving (30% for Claude 3.5 Sonnet) compared to generating function implementations.
- The inherent complexity of formal verification poses a substantial challenge for both AI and human experts, as demonstrated by a human expert's difficulty in completing proofs for a single sample.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.