License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2023.26
URN: urn:nbn:de:0030-drops-184013
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18401/
Go to the corresponding LIPIcs Volume Portal

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

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

pdf-format:
LIPIcs-ITP-2023-26.pdf (0.7 MB)

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.

BibTeX - Entry

@InProceedings{reichel_et_al:LIPIcs.ITP.2023.26,
  author =	{Reichel, Tom and Henderson, R. Wesley and Touchet, Andrew and Gardner, Andrew and Ringer, Talia},
  title =	{{Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{26:1--26:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/18401},
  URN =		{urn:nbn:de:0030-drops-184013},
  doi =		{10.4230/LIPIcs.ITP.2023.26},
  annote =	{Keywords: proof repair, datasets, benchmarks, machine learning, formal proof}
}

Keywords: proof repair, datasets, benchmarks, machine learning, formal proof
Collection: 14th International Conference on Interactive Theorem Proving (ITP 2023)
Issue Date: 2023
Date of publication: 26.07.2023
Supplementary Material: Text (Appendix): https://dependenttyp.es/pdf/repairdataappendix.pdf
Dataset (Sample): https://doi.org/10.5281/zenodo.7935207

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI