Guiding an automated theorem prover with neural rewriting (Q2104548)

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].