Learning to Find Proofs and Theorems by Learning to Refine Search Strategies: The Case of Loop Invariant Synthesis
This addresses the problem of automated theorem proving for domains with limited training data, such as loop invariant synthesis, though it appears incremental as it builds on existing AlphaZero and neural network methods.
The paper tackles automated theorem proving by training an AlphaZero-style agent to refine a high-level expert strategy, with a teacher agent generating tasks of suitable difficulty, and applies this to loop invariant synthesis for imperative programs using neural networks.
We propose a new approach to automated theorem proving where an AlphaZero-style agent is self-training to refine a generic high-level expert strategy expressed as a nondeterministic program. An analogous teacher agent is self-training to generate tasks of suitable relevance and difficulty for the learner. This allows leveraging minimal amounts of domain knowledge to tackle problems for which training data is unavailable or hard to synthesize. As a specific illustration, we consider loop invariant synthesis for imperative programs and use neural networks to refine both the teacher and solver strategies.