Hardening the Hammer: More Integration of Automatic and Interactive Theorem Provers

• Applicant: Professor Tobias Nipkow, Ph.D.
• Subject Area: Theoretical Computer Science
• Term: from 2012 to 2016
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 226154341

• Final Report Year: 2019

Final Report Abstract

Proof assistants—also called interactive theorem provers—are increasingly used to verify hardware and software and to formalize mathematics. However, despite the success stories, including a verified microkernel, formal theorem proving remains laborious and requires specialized experts. Today it takes novices months or years to become proficient. As one user quipped, “There’s no learning curve—it’s a series of cliffs.” The situation has improved in the past decade with the integration of first-order automatic theorem provers in proof assistant. Sledgehammer is a tool that integrates automatic theorem provers in Isabelle/HOL, a popular proof assistant developed primarily at TU München in the principal investigator’s research group. The primary goal of the Hardening the Hammer project was to increase Sledgehammer’s success rate. During the course of the project, the success rate on a representative set of benchmarks has gone up from 64% to 77%, thanks to various innovations: • the use of machine learning to select potentially relevant lemmas from the available libraries; • the use of lightweight (yet correct) encodings to translate Isabelle’s rich logic to the automatic theorem provers’ less expressive logics; • improvements in the underlying automatic theorem provers, in collaboration with researchers in automated reasoning; • the translation of detailed machine-generated proofs into Isabelle proofs to increase the success rate of proof reconstruction; • the integration of higher-order provers.

Publications

• Extending Sledgehammer with SMT solvers. Journal of Automated Reasoning 51(1), pp. 109–128, 2013
  Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson
  (See online at https://doi.org/10.1007/s10817-013-9278-5)
• A learning-based fact selector for Isabelle/HOL. Journal of Automated Reasoning 57(3), pp. 219–244, 2016
  Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef Urban
  (See online at https://doi.org/10.1007/s10817-016-9362-8)
• Encoding monomorphic and polymorphic types. Logical Methods in Computer Science 12(4:13), 2016, pp. 1–52
  Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, and Nicholas Smallbone
  (See online at https://doi.org/10.1007/978-3-642-36742-7_34)
• Hammering towards QED. Journal of Formalized Reasoning 9(1), pp. 101–148, 2016
  Jasmin C. Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban
  (See online at https://doi.org/10.6092/issn.1972-5787/4593)
• Semi-intelligible Isar proofs from machine-generated proofs. Journal of Automated Reasoning 56(2), pp. 155–200, 2016
  Jasmin Christian Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, and Albert Steckermeier
  (See online at https://doi.org/10.1007/s10817-015-9335-3)
• Superposition: Types and Induction. PhD thesis, Universität des Saarlandes
  Daniel Wand