Reference. Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset
We report on our efforts building a new, large proof-repair dataset and benchmark suite for the Coq proof assistant. The dataset is made up of Git commits from open-source projects with old and new versions of definitions and proofs aligned across commits. Building this dataset has been a significant undertaking, highlighting a number of challenges and gaps in existing infrastructure. We discuss these challenges and gaps, and we provide recommendations for how the proof assistant community can address them. Our hope is to make it easier to build datasets and benchmark suites so that machine-learning tools for proofs will move to target the tasks that matter most and do so equitably across proof assistants.
Cite
Cited by (1)
HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement hu-2025-hybridprover
Formal methods play a crucial role in ensuring the reliability of critical systems through rigorous mathematical verification. However, their adoption remains limited due to the labor-intensive nature of manual proof construction. Recent advances in large language models (LLMs) have opened new opportunities for automated theorem proving. Two main paradigms have emerged: stepwise tactic-based generation and whole-proof synthesis. While both approaches have complementary strengths, existing work largely treats them in isolation. In this work, we propose HybridProver, a unified framework that integrates whole-proof synthesis and tactic-based generation through proof sketches as an intermediate representation. This design enables the reuse of partially correct proof structures while effectively combining high-level planning with fine-grained reasoning. We implement HybridProver in Isabelle/HOL and post-train two 7B-scale LLMs on our optimized Isabelle datasets. Experiments on the miniF2F Isabelle benchmark achieved a 73.8% success rate and improved upon the previous state of the art (61.9%), demonstrating that lightweight models, when combined with our approach, can effectively generate Isabelle/HOL proofs without relying on very large LLMs. Ablation studies further analyze the impact of dataset quality, training configurations, and sampling strategies on proof generation.
Cites 56 works (4 here)
With notes (4)
Proof repair across type equivalences ringer-2021-proof
REPLica: REPL instrumentation for Coq analysis ringer-2020-replica
Ornaments for Proof Reuse in Coq ringer-2019-ornaments
Ornaments express relations between inductive types with the same inductive structure. We implement fully automatic proof reuse for a particular class of ornaments in a Coq plugin, and show how such a tool can give programmers the rewards of using indexed inductive types while automating away many of the costs. The plugin works directly on Coq code; it is the first ornamentation tool for a non-embedded dependently typed language. It is also the first tool to automatically identify ornaments: To lift a function or proof, the user must provide only the source type, the destination type, and the source function or proof. In taking advantage of the mathematical properties of ornaments, our approach produces faster functions and smaller terms than a more general approach to proof reuse in Coq.
Adapting proof automation to adapt proofs ringer-2018-adapting
External (52)
- Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs (2023)
- Out of the bleu: how should we assess quality of the code generation models (2023)
- 2nd MATH-AI Workshop at NeurIPS’22 (2022)
- AI for Theorem Proving (AITP), 2016-2022 (2022)
- ProofNet: A benchmark for autoformalizing and formally proving undergraduate-level mathematics problems (2022)
- Beyond Bayes: Paths Towards Universal Reasoning Systems (2022)
- A parallel corpus of natural language and isabelle artefacts (2022)
- Diversity-driven automated formal verification (2022)
- HyperTree Proof Search for Neural Theorem Proving (2022)
- Autoformalization with large language models (2022)
- minif2f: a cross-system benchmark for formal olympiad-level mathematics (2022)
- Proof artifact co-training for theorem proving with language models (2021)
- Lisa: Language models of isabelle proofs (2021)
- Towards the automatic mathematician (2021)
- Break-it-fix-it: Unsupervised learning for program repair (2021)
- The Tactician: A Seamless, Interactive Tactic Learner and Prover for Coq (2020)
- CoCoNuT: combining context-aware neural translation models using ensemble for program repair (2020)
- Generative language modeling for automated theorem proving (2020)
- Codebleu: a method for automatic evaluation of code synthesis (2020)
- QED at large: A survey of engineering of formally verified software (2020)
- Getafix: learning to fix bugs automatically (2019)
- Holist: An environment for machine learning of higher order logic theorem proving (2019)
- Metamath: A Computer Language for Mathematical Proofs (2019)
- Generating Correctness Proofs with Neural Networks (2019)
- Automatic refactoring for agda (2019)
- Learning to prove theorems via interacting with proof assistants (2019)
- Automatic software repair: A survey (2018)
- Automatic Software Repair: A Bibliography (2018)
- Front-end tooling for building and maintaining dependently-typed functional programs (2018)
- Context-aware patch generation for better automated program repair (2018)
- Variable generalization performance of a deep learning model to detect pneumonia in chest radiographs: A cross-sectional study (2018)
- SerAPI: Machine-Friendly, Data-Centric Serialization for COQ (2016)
- An analysis of patch plausibility and correctness for generate-and-validate patch generation systems (2015)
- Automatic repair of real bugs: An experience report on the defects4j dataset (2015)
- Defects4J: a database of existing faults to enable controlled testing studies for Java programs (2014)
- Encyclopedia of Distances (2014)
- Mash: Machine learning for sledgehammer (2013)
- Isabelle/jedit — a prover IDE within the PIDE framework (2012)
- Fast and robust earth mover’s distances (2009)
- Proof reuse with extended inductive types (2004)
- BLEU: a method for automatic evaluation of machine translation (2002)
- Generalization and reuse of tactic proofs (1994)
- Proof Transformations in Higher-Order Logic (1987)
- Identification of common molecular subsequences (1981)
- Algorithms for the Assignment and Transportation Problems (1957)
- Statistics - archive of formal proofs
- Proof engineering, adaptation, repair, and learning for software (pearls)
- Is there a full documentation of coq’s grammar?
- Proposal: a custom build tool for coq projects
- Query ast returns empty result
- Serapi ’classic mode’ final release notice
- Portal-to-isabelle