smart2

SMART

Strong Modular Proof Assistance Reasoning Across Theories



ERC Project "SMART". Starting Grant no. 714034 realized at the Computational Logic research group of the Institute of Computer Science at the University of Innsbruck. Project dates: March 2017 - February 2022. Team:

  • Cezary Kaliszyk (PI)
  • Burak Ekici (Postdoc)
  • Ping Hou (Postdoc)
  • Miroslav Olsak (Postdoc)
  • Michael Faerber (Postdoc)
  • Shawn Qingxiang Wang (PhD student)
  • Joshua Chen (PhD student)
  • Stanisław Purgał (PhD student)
  • Evan Marzion (PhD student)
  • Julian Parsert (research assistant)

Summary

Formal proof technology delivers an unparalleled level of certainty and security. Nevertheless, applying proof assistants to the verification of complex theories and designs is still extremely laborious. High profile certification projects, such as seL4, CompCert, and Flyspeck require tens of person-years. We recently demonstrated that this effort can be significantly reduced by combining reasoning and learning in so called hammer systems: 40% of the Flyspeck, HOL4, Isabelle/HOL, and Mizar top-level lemmas can be proved automatically.

Today’s early generation of hammers consists of individual systems limited to very few proof assistants. The accessible knowledge repositories are isolated, and there is no reuse of hammer components. It is possible to achieve a breakthrough in proof automation by developing new AI methods that combine reasoning knowledge and techniques into a smart hammer, that works over a very large part of today’s formalized knowledge. The main goal of the project is to develop a strong and uniform learning-reasoning system available for multiple logical foundations. To achieve this, we will develop: (a) uniform learning methods, (b) reusable ATP encoding components for different foundational aspects, (c) integration of proof reconstruction, and (d) methods for knowledge extraction, reuse and content merging. The single proof advice system will be made available for multiple proof assistants and their vast heterogeneous libraries.

The ultimate outcome is an advice system able to automatically prove half of Coq, ACL2, and Isabelle/ZF top-level theorems. Additionally we will significantly improve success rates for HOL provers and Mizar. The combined smart advice method together with the vast accumulated knowledge will result in a novel kind of tool, which allows working mathematicians to automatically find proofs of many simple conjectures, paving the way for the widespread use of formal proof in mathematics and computer science.

Activities

  • We co-organize the Conference on Artificial Intelligence and Theorem Proving (AITP)

Publications

  • TacticToe: Learning to reason with HOL4 Tactics.
    LPAR 2017. [ BibTeX | Publisher's site | PDF (preprint) ]
  • Goal-Oriented Conjecturing for Isabelle/HOL.
    CICM 2018. [ Publisher's site | Preprint (Arxiv) ]
  • First Experiments with Neural Translation of Informal to Formal Mathematics.
    CICM 2018. [ BibTeX | Publisher's site | PDF (preprint) ]
  • Concrete Semantics with Coq and CoqHammer.
    CICM 2018. [ BibTeX | Publisher's site | PDF (preprint) ]
  • Certification of Nonclausal Connection Tableaux Proofs.
    TABLEAUX 2019. [ BibTeX | Publisher's site | PDF (preprint) ]
  • Aligning Concepts across Proof Assistant Libraries.
    J. Symbolic Computation. 2019. [ BibTeX | Publisher's site | PDF (preprint) ]
  • Semantics of Mizar as an Isabelle Object Logic.
    Journal of Automated Reasoning. 2019. [ BibTeX | Publisher's site | PDF (preprint) ]
  • Towards a Unified Ordering for Superposition-Based Automated Reasoning.
    ICMS 2018. [ BibTeX | Publisher's site | PDF (preprint) ]
  • Towards Formal Foundations for Game Theory.
    ITP 2018. [ BibTeX | Publisher's site | PDF (preprint) ]
  • IMP with exceptions over decorated logic.
    Discrete Mathematics & Theoretical Computer Science, 2018. [ Publisher's site | Preprint (Arxiv) ]
  • Reinforcement Learning of Theorem Proving.
    NeurIPS 2018. [ BibTeX | Publisher's site | arXiv | PDF (preprint) ]
  • Can Neural Networks Learn Symbolic Rewriting?
    LRGSR 2019. [ Publisher's site | Preprint ]
  • HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving.
    ICLR 2017. [ BibTeX | PDF (preprint) ]
  • Monte Carlo Tableau Proof Search.
    CADE 2017. [ BibTeX | Publisher's site | PDF (preprint) ]
  • Automating Formalization by Statistical and Semantic Parsing of Mathematics.
    ITP 2017, volume 10499 of LNCS, pp. 12 – 27. 2017. [ BibTeX | Publisher's site | PDF (preprint) ]
  • Isabelle Formalization of Set Theoretic Structures and Set Comprehensions.
    MACIS 2017. [ BibTeX [ Publisher's site | PDF (preprint) ]
  • Classification of Alignments between Concepts of Formal Mathematical Systems.
    CICM 2017. [ BibTeX | Publisher's site | PDF (preprint) ]
  • Towards Mac Lane's Comparison Theorem for the (co)Kleisli Construction in Coq.
    FMM 2018. [ Publisher's site | PDF (preprint) ]
  • System Description: Statistical Parsing of Informalized Mizar Formulas.
    SYNASC 2017. [ BibTeX | Publisher's site | PDF (preprint) ]
  • Presentation and Manipulation of Mizar Properties in an Isabelle Object Logic.
    CICM 2017. [ BibTeX | Publisher's site | PDF (preprint) ]
  • Higher-order Tarski Grothendieck as a Foundation for Formal Proof.
    ITP 2019. [ BibTeX | Publisher's site | PDF (preprint) ]
  • GRUNGE: A Grand Unified ATP Challenge.
    CADE 2019. [ BibTeX | Publisher's site | PDF (preprint) ]
  • Formal Microeconomic Foundations and the First Welfare Theorem.
    CPP 2018. [ BibTeX | Publisher's site | PDF (preprint) ]
  • Deep Network Guided Proof Search.
    LPAR 2017. [ BibTeX | Publisher's site | PDF (preprint) ]
  • Hammer for Coq: Automation for Dependent Type Theory.
    JAR, 2018 [ BibTeX | Publisher's site | PDF (preprint) ]
  • Verifying Bit-vector Invertibility Conditions in Coq.
    PxTP 2019. [ PDF (arxiv) ]
  • Relaxed Weighted Path Order in Theorem Proving.
    MCS 2020. [ Publisher's site | PDF (preprint) ]
  • Property Invariant Embedding for Automated Reasoning.
    ECAI 2020. To appear. [ PDF (arxiv) ]
  • Exploration of neural machine translation in autoformalization of mathematics in Mizar.
    CPP 2020. [ BibTeX | Publisher's site | PDF (preprint) ]
  • Property Preserving Embedding of First-order Logic.
    GCAI 2020. [ BibTeX | Publisher's site | PDF (preprint) ]
  • Mac Lane’s Comparison Theorem for the Kleisli Construction Formalized in Coq.
    Mathematics in Computer Science, 2020. [ Publisher's site | PDF (preprint) ]


 erc100eu100logo-uibklogonew
Nach oben scrollen