@inproceedings{0e819b17740448e49b2327111b433c36,
title = "Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset",
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.",
keywords = "benchmarks, datasets, formal proof, machine learning, proof repair",
author = "Tom Reichel and {Wesley Henderson}, R. and Andrew Touchet and Andrew Gardner and Talia Ringer",
note = "Funding This research was developed with funding from the Defense Advanced Research Projects Agency. The views, opinions, and/or findings expressed are those of the author(s) and should not be interpreted as representing the official views or policies of the Department of Defense or the U.S. Government. This research was developed with funding from the Defense Advanced Research Projects Agency. The views, opinions, and/or findings expressed are those of the author(s) and should not be interpreted as representing the official views or policies of the Department of Defense or the U.S. Government.; 14th International Conference on Interactive Theorem Proving, ITP 2023 ; Conference date: 31-07-2023 Through 04-08-2023",
year = "2023",
month = jul,
doi = "10.4230/LIPIcs.ITP.2023.26",
language = "English (US)",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
editor = "Adam Naumowicz and Rene Thiemann",
booktitle = "14th International Conference on Interactive Theorem Proving, ITP 2023",
}