We introduce the Formally Verified Automated Programming Progress Standards, or FVAPPS, a benchmark of 4712 samples for writing programs and proving their correctness, the largest formal verification benchmark. 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 accomplished 30% and Gemini accomplished 18%. We challenge the machine learning and program synthesis communities to solve both each general purpose programming problem and it’s associated correctness specifications. The benchmark will be available on HuggingFace upon publication.
Jan Kels Heinrich-Heine-Universität Düsseldorf, Abdelhalim Dahou GESIS – Leibniz-Institute for the Social Sciences, Brigitte Mathiak GESIS – Leibniz-Institute for the Social Sciences
Shihao Xia The Pennsylvania State University, Mengting He The Pennsylvania State University, Linhai Song The Pennsylvania State University, Yiying Zhang University of California San Diego