Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset

Tom Reichel, R. Wesley Henderson, Andrew Touchet, Andrew Gardner, Talia Ringer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publication14th International Conference on Interactive Theorem Proving, ITP 2023
EditorsAdam Naumowicz, Rene Thiemann
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959772846
DOIs
StatePublished - Jul 2023
Event14th International Conference on Interactive Theorem Proving, ITP 2023 - Bialystok, Poland
Duration: Jul 31 2023Aug 4 2023

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume268
ISSN (Print)1868-8969

Conference

Conference14th International Conference on Interactive Theorem Proving, ITP 2023
Country/TerritoryPoland
CityBialystok
Period7/31/238/4/23

Keywords

  • benchmarks
  • datasets
  • formal proof
  • machine learning
  • proof repair

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset'. Together they form a unique fingerprint.

Cite this