Learned Provability Likelihood for Tactical Search
Thibault Gauthier
TL;DR
This paper introduces a method to estimate the provability of formulas to enhance tactical theorem proving, demonstrated by improvements in re-proving theorems in HOL4 using TacticToe.
Contribution
It presents a novel approach to incorporate provability likelihood estimates into tactical search, improving theorem prover performance.
Findings
Increased re-proving success rate on HOL4 library
Enhanced user experience with improved framework performance
Effective integration of provability estimates into tactical search
Abstract
We present a method to estimate the provability of a mathematical formula. We adapt the tactical theorem prover TacticToe to factor in these estimations. Experiments over the HOL4 library show an increase in the number of theorems re-proven by TacticToe thanks to this additional guidance. This amelioration in performance together with concurrent updates to the TacticToe framework lead to an improved user experience.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsStatistics Education and Methodologies · Mathematics, Computing, and Information Processing · Artificial Intelligence in Games