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

• URL: http://arxiv.org/abs/2502.05714v1
• Date: Sat, 08 Feb 2025 22:54:58 GMT
• Title: Proving the Coding Interview: A Benchmark for Formally Verified Code Generation
• Authors: Quinn Dougherty, Ronak Mehta,
• Abstract summary: We introduce the Formally Verified Automated Programming Progress Standards, or FVAPPS, a benchmark of 4715 samples for writing programs and proving their correctness. We challenge the machine learning and program synthesis communities to solve both each general purpose programming problem and its associated correctness specifications.
• Score: 3.5319285228327417
• License:
• 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.

Related papers

• EquiBench: Benchmarking Code Reasoning Capabilities of Large Language Models via Equivalence Checking [54.354203142828084]
  We present the task of equivalence checking as a new way to evaluate the code reasoning abilities of large language models. We introduce EquiBench, a dataset of 2400 program pairs spanning four programming languages and six equivalence categories. Our evaluation of 17 state-of-the-art LLMs shows that OpenAI o3-mini achieves the highest overall accuracy of 78.0%.
  arXiv  Detail & Related papers  (2025-02-18T02:54:25Z)
• CLOVER: A Test Case Generation Benchmark with Coverage, Long-Context, and Verification [71.34070740261072]
  This paper presents a benchmark, CLOVER, to evaluate models' capabilities in generating and completing test cases. The benchmark is containerized for code execution across tasks, and we will release the code, data, and construction methodologies.
  arXiv  Detail & Related papers  (2025-02-12T21:42:56Z)
• How Should We Build A Benchmark? Revisiting 274 Code-Related Benchmarks For LLMs [60.25940747590386]
  We propose How2Bench, which is comprised of a 55-criteria checklist as a set of guidelines to govern the development of code-related benchmarks comprehensively. We profiled 274 benchmarks released within the past decade and found concerning issues. Nearly 70% of the benchmarks did not take measures for data quality assurance; over 10% did not even open source or only partially open source.
  arXiv  Detail & Related papers  (2025-01-18T09:51:57Z)
• Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification [11.115201117143929]
  We present Rango, a fully automated synthesis proof tool for Coq. Rango identifies relevant premises and also similar proofs from the current project and uses them during synthesis. Our evaluation shows that Rango adding relevant to its context leads to a 47% increase in the number of theorems proven.
  arXiv  Detail & Related papers  (2024-12-18T17:08:42Z)
• TestGenEval: A Real World Unit Test Generation and Test Completion Benchmark [24.14654309612826]
  TestGenEval comprises 68,647 tests from 1,210 code and test file pairs across 11 well-maintained Python repositories. It covers initial tests authoring, test suite completion, and code coverage improvements. We evaluate several popular models, with sizes ranging from 7B to 405B parameters.
  arXiv  Detail & Related papers  (2024-10-01T14:47:05Z)
• Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming [8.34623776815378]
  We curate a dataset of 600K lines of open-source F* programs and proofs. This dataset includes software used in production systems ranging from Windows and Linux to Python and Firefox. We investigate the use of AI to synthesize programs and their proofs in F*, with promising results.
  arXiv  Detail & Related papers  (2024-05-03T00:14:33Z)
• Can Language Models Solve Olympiad Programming? [40.54366634332231]
  This paper introduces the USACO benchmark with 307 problems from the USA Computing Olympiad. We construct and test a range of LM inference methods for competitive programming for the first time. We find GPT-4 only achieves a 8.7% pass@1 accuracy with zero-shot chain-of-thought prompting.
  arXiv  Detail & Related papers  (2024-04-16T23:27:38Z)
• CodeT: Code Generation with Generated Tests [49.622590050797236]
  We explore the use of pre-trained language models to automatically generate test cases. CodeT executes the code solutions using the generated test cases, and then chooses the best solution. We evaluate CodeT on five different pre-trained models with both HumanEval and MBPP benchmarks.
  arXiv  Detail & Related papers  (2022-07-21T10:18:37Z)
• Measuring Coding Challenge Competence With APPS [54.22600767666257]
  We introduce APPS, a benchmark for code generation. Our benchmark includes 10,000 problems, which range from having simple one-line solutions to being substantial algorithmic challenges. Recent models such as GPT-Neo can pass approximately 15% of the test cases of introductory problems.
  arXiv  Detail & Related papers  (2021-05-20T17:58:42Z)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  We propose a transformer-based model that answers binary questions over rule-bases and generates the corresponding proofs. Our model learns to predict nodes and edges corresponding to proof graphs in an efficient constrained training paradigm. We conduct experiments on synthetic, hand-authored, and human-paraphrased rule-bases to show promising results for QA and proof generation.
  arXiv  Detail & Related papers  (2020-10-06T15:47:53Z)
• Unit Test Case Generation with Transformers and Focal Context [10.220204860586582]
  AthenaTest aims to generate unit test cases by learning from real-world focal methods and developer-written test cases. We introduce Methods2Test, the largest publicly available supervised parallel corpus of unit test case methods and corresponding focal methods in Java. We evaluate AthenaTest on five defects4j projects, generating 25K passing test cases covering 43.7% of the focal methods with only 30 attempts.
  arXiv  Detail & Related papers  (2020-09-11T18:57:36Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.