TacticToe: learning to reason with HOL4 tactics
From MaRDI portal
Abstract: Techniques combining machine learning with translation to automated reasoning have recently become an important component of formal proof assistants. Such "hammer" tech- niques complement traditional proof assistant automation as implemented by tactics and decision procedures. In this paper we present a unified proof assistant automation approach which attempts to automate the selection of appropriate tactics and tactic-sequences com- bined with an optimized small-scale hammering approach. We implement the technique as a tactic-level automation for HOL4: TacticToe. It implements a modified A*-algorithm directly in HOL4 that explores different tactic-level proof paths, guiding their selection by learning from a large number of previous tactic-level proofs. Unlike the existing hammer methods, TacticToe avoids translation to FOL, working directly on the HOL level. By combining tactic prediction and premise selection, TacticToe is able to re-prove 39 percent of 7902 HOL4 theorems in 5 seconds whereas the best single HOL(y)Hammer strategy solves 32 percent in the same amount of time.
Recommendations
Cited in
(21)- Hammer for Coq: automation for dependent type theory
- TacticToe: learning to prove with tactics
- Towards the automatic mathematician
- Online machine learning techniques for Coq: a comparison
- The role of entropy in guiding a connection prover
- Learning theorem proving components
- The Tactician. A seamless, interactive tactic learner and prover for Coq
- GRUNGE: a grand unified ATP challenge
- Standalone Tactics Using OpenTheory
- A learning-based fact selector for Isabelle/HOL
- Sharing HOL4 and HOL Light proof knowledge
- TacticToe
- MaSh: machine learning for Sledgehammer
- Hammering Mizar by Learning Clause Guidance (Short Paper).
- Machine Learning for Inductive Theorem Proving
- Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction
- Learning Proof Transformations and Its Applications in Interactive Theorem Proving
- Dynamic dependability analysis of shuffle-exchange networks
- Deep reinforcement learning for synthesizing functions in higher-order logic
- Learning guided automated reasoning: a brief survey
- Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
Describes a project that uses
Uses Software
This page was built for publication: TacticToe: learning to reason with HOL4 tactics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4645730)
