Learning to Guide a Saturation-Based Theorem Prover

Area of Science:

• Artificial Intelligence
• Automated Reasoning
• Machine Learning

Background:

• Traditional automated theorem provers depend on manual heuristics for proof search.
• Recent advancements focus on integrating machine learning for automated performance improvement.

Purpose of the Study:

• To introduce TRAIL (Trial Reasoner for AI that Learns), a deep learning-based theorem prover.
• To enhance automated theorem proving through a neural framework for saturation-based methods.

Main Methods:

• Utilizing a graph neural network for logical formula representation.
• Developing a novel neural representation for theorem prover states and actions.
• Implementing an attention-based policy for inference selection.

Main Results:

• TRAIL significantly outperforms previous reinforcement learning-based theorem provers (up to 36% improvement).
• TRAIL surpasses state-of-the-art traditional theorem provers on a benchmark (up to 17% improvement).

Conclusions:

• TRAIL demonstrates the efficacy of deep learning in automated theorem proving.
• This approach offers a powerful alternative to traditional heuristic-based methods.