Learning Theorem Proving Components
Saturation-style automated theorem provers (ATPs) based on the given clause procedure are today the strongest general reasoners for classical first-order logic. The clause selection heuristics in such systems are, however, often evaluating clauses in isolation, ignoring other clauses. This has changed recently by equipping the E/ENIGMA system with a graph neural network (GNN) that chooses the next given clause based on its evaluation in the context of previously selected clauses. In this work, we describe several algorithms and experiments with ENIGMA, advancing the idea of contextual evaluation based on learning important components of the graph of clauses.
Code (1)
Tasks
Automated Theorem ProvingGraph Neural NetworkMethods 이 논문이 사용한 방법론
Similar Papers 제목 키워드 기반
Proceedings 7th International Workshop on Theorem proving components for Educational software
The 7th International Workshop on Theorem proving components for Educational software (ThEdu'18) was held in Oxford, United Kingdom, on 18 July 2018. It was associated to the conference, Federated Logic Conference 2018 (…
Automated Theorem ProvingProceedings 6th International Workshop on Theorem proving components for Educational software
The 6th International Workshop on Theorem proving components for Educational software (ThEdu'17) was held in Gothenburg, Sweden, on 6 Aug 2017. It was associated to the conference CADE26. Topics of interest include: meth…
Automated Theorem ProvingLearning to Guide a Saturation-Based Theorem Prover
Traditional automated theorem provers have relied on manually tuned heuristics to guide how they perform proof search. Recently, however, there has been a surge of interest in the design of learning mechanisms that can b…
Automated Theorem ProvingGraph Neural Networkreinforcement-learningReinforcement Learning+1Aristotle: IMO-level Automated Theorem Proving
We introduce Aristotle, an AI system that combines formal verification with informal reasoning, achieving gold-medal-equivalent performance on the 2025 International Mathematical Olympiad problems. Aristotle integrates t…
Automated Theorem ProvingProceedings 12th International Workshop on Theorem proving components for Educational software
The ThEdu series pursues the smooth transition from an intuitive way of doing mathematics at secondary school to a more formal approach to the subject in STEM education, while favouring software support for this transiti…
Automated Theorem Proving