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.19
URN: urn:nbn:de:0030-drops-183942
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18394/
Go to the corresponding LIPIcs Volume Portal

Jakubův, Jan ; Chvalovský, Karel ; Goertzel, Zarathustra ; Kaliszyk, Cezary ; Olšák, Mirek ; Piotrowski, Bartosz ; Schulz, Stephan ; Suda, Martin ; Urban, Josef

MizAR 60 for Mizar 50

pdf-format:
LIPIcs-ITP-2023-19.pdf (0.9 MB)

Abstract

As a present to Mizar on its 50th anniversary, we develop an AI/TP system that automatically proves about 60% of the Mizar theorems in the hammer setting. We also automatically prove 75% of the Mizar theorems when the automated provers are helped by using only the premises used in the human-written Mizar proofs. We describe the methods and large-scale experiments leading to these results. This includes in particular the E and Vampire provers, their ENIGMA and Deepire learning modifications, a number of learning-based premise selection methods, and the incremental loop that interleaves growing a corpus of millions of ATP proofs with training increasingly strong AI/TP systems on them. We also present a selection of Mizar problems that were proved automatically.

BibTeX - Entry

@InProceedings{jakubuv_et_al:LIPIcs.ITP.2023.19,
  author =	{Jakub\r{u}v, Jan and Chvalovsk\'{y}, Karel and Goertzel, Zarathustra and Kaliszyk, Cezary and Ol\v{s}\'{a}k, Mirek and Piotrowski, Bartosz and Schulz, Stephan and Suda, Martin and Urban, Josef},
  title =	{{MizAR 60 for Mizar 50}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{19:1--19:22},
  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/18394},
  URN =		{urn:nbn:de:0030-drops-183942},
  doi =		{10.4230/LIPIcs.ITP.2023.19},
  annote =	{Keywords: Mizar, ENIGMA, Automated Reasoning, Machine Learning}
}

Keywords: Mizar, ENIGMA, Automated Reasoning, Machine Learning
Collection: 14th International Conference on Interactive Theorem Proving (ITP 2023)
Issue Date: 2023
Date of publication: 26.07.2023
Supplementary Material: Software: https://github.com/ai4reason/ATP_Proofs

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