Report
Teaser, summary, work performed and final results
Periodic Reporting for period 1 - Matryoshka (Fast Interactive Verification through Strong Higher-Order Automation)
Teaser
Proof assistants are increasingly used to verify hardware and software and to formalize mathematics. However, despite the success stories, they remain very laborious to use. The situation has improved with the integration of first-order automatic theorem...
Summary
Proof assistants are increasingly used to verify hardware and software and to formalize mathematics. However, despite the success stories, they remain very laborious to use. The situation has improved with the integration of first-order automatic theorem provers—superposition provers and SMT (satisfiability modulo theories) solvers—through middleware such as Sledgehammer for Isabelle/HOL and HOLyHammer for HOL Light and HOL4; but this research has now reached the point of diminishing returns. Only so much can be done when viewing automatic provers as black boxes.
To make interactive verification more cost-effective, we propose to deliver very high levels of automation to users of proof assistants by fusing and extending two lines of research: automatic and interactive theorem proving. This is our grand challenge. Our starting point is that first-order (FO) automatic provers are the best tools available for performing most of the logical work. Our approach will be to enrich superposition and SMT with higher-order (HO) reasoning in a careful manner, to preserve their desirable properties. We will design proof rules and strategies, guided by representative benchmarks from interactive verification.
With higher-order superposition and higher-order SMT in place, we will develop highly automatic provers building on modern superposition provers and SMT solvers, following a novel stratified architecture. To reach end users, these new provers will be integrated in proof assistants and will be available as backends to more specialized verification tools. The users of proof assistants and similar tools stand to experience substantial productivity gains: From 2010 to 2016, the success rate of automatic provers on interactive proof obligations from a representative benchmark suite called Judgment Day has risen from 47% to 77%; with this project, we aim at 90%–95% proof automation.
Work performed
Superposition and SMT are currently the most successful proof calculi for reasoning about classical first-order logic. Despite some convergence, they remain very different technologies, with complementary strengths and weaknesses.
Our first larger contribution so far has been to extend superposition and SMT to handle some higher-order constructs. These are constructs that are present in nearly all proof assistants (Coq, Isabelle, ...) and hence are needed to do actual reasoning in practice. Our contribution is a first step towards full support for higher-order logic. These techniques are implemented in the SMT solver veriT and the superposition provers Zipperposition and E 2.3.
We have also made some contributions to the formal mathematical library of the Lean proof assistant, partly related to Task 4.
Final results
We now have a new generation of provers (namely, veriT, Zipperposition, and E) that support a richer logic, and hence are more easily and efficiently applicable to be used in proof assistants. This will make proof assistants more automatic and hence easier to use, to verify hardware or software or to formalize mathematics. The expected result is provers that support full higher-order logic and that are well integrated in major proof assistants.
Website & more info
More info: http://matryoshka.gforge.inria.fr.