Guiding an automated theorem prover with neural rewriting
Kinyon and Veroff used Prover9 to search for the proof of the abelian inner mapping (AIM) conjecture, an open problem in quasigroup theory. In this paper, the authors improve its performance by using neural synthesis to suggest useful alternative formulations of the problem. They designed a method called 3SIL (stratified shortest solution imitation learning) which trains a neural predictor through a reinforcement learning loop to propose correct rewrites of the conjecture that guide the search. The authors trained 3SIL on a simpler task and demonstrated that it outperformed other reinforcement learning methods. They then trained 3SIL on the AIM benchmark and showed that the final trained network outperformed Prover9 and Waldmeister, another automated theorem prover, in solving the AIM problems. The combined system of 3SIL and Prover9 achieved a success rate of 90\%, which is 8.3\% higher than Prover9 alone in the same time. For the entire collection see [Zbl 1499.68012].
- scientific article; zbMATH DE number 1748489
- A neurally-guided, parallel theorem prover
- Deep network guided proof search
- Automated proof synthesis for the minimal propositional logic with deep neural networks
- Toward neural-network-guided program synthesis and verification
- A fully automatic theorem prover with human-style output
- The term rewriting approach to automated theorem proving
- Verifying B proof rules using deep embedding and automated theorem proving
- A New Class of Automated Theorem-Proving Algorithms
- ACER
- Automated theorem proving in quasigroup and loop theory
- Citius altius fortius: lessons learned from the theorem prover Waldmeister
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- Faster, higher, stronger: E 2.3
- Hammering towards QED
- scientific article; zbMATH DE number 1809862 (Why is no real title available?)
- Loops with abelian inner mapping groups: an application of automated deduction
- Premise selection for mathematics by corpus analysis and kernel methods
- Proof simplification and automated theorem proving
- Reinforcement learning. An introduction
- TacticToe: learning to prove with tactics
- The CADE-27 automated theorem proving system competition -- CASC-27
- The Tactician. A seamless, interactive tactic learner and prover for Coq
- Tree neural networks in HOL4
- Twee: an equational theorem prover
- Using hints to increase the effectiveness of an automated reasoning program: Case studies
- Development of neural networks for accelerating automated theorem proving: Results for the group theory
- Enhancing ENIGMA given clause guidance
- Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
- A neurally-guided, parallel theorem prover
- Deep network guided proof search
- Property invariant embedding for automated reasoning
- Automated proof synthesis for the minimal propositional logic with deep neural networks
- An Experimental Pipeline for Automated Reasoning in Natural Language (Short Paper)
- Invariant neural architecture for learning term synthesis in instantiation proving
Uses Software
This page was built for publication: Guiding an automated theorem prover with neural rewriting
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2104548)
