Source-linked AI summary
Learning Guided Automated Reasoning: A Brief Survey
Lasse Blaauwbroek, David Cerna, Thibault Gauthier, Jan Jakubův, Cezary Kaliszyk, Martin Suda, Josef Urban
TL;DR
Automated reasoners face combinatorial explosion and many consequential heuristic choices. This survey reviews learning-based guidance and combinations of machine learning with automated and interactive theorem proving, covering premise selection, proof guidance, feedback loops, and symbolic classification.
Problem
Automated reasoning and theorem-proving systems face combinatorial explosion and many heuristic choices that affect their performance.
Source: §1 · p. 1Method
The survey reviews machine-learning methods for automated and interactive theorem proving, from premise selection to guidance at multiple levels and combinations of learning with reasoning.
Source: §1 · p. 2Results
The paper discusses early systems, mathematical knowledge characterization, premise selection, machine-learning-guided theorem provers, proving-and-learning feedback loops, and related symbolic classification problems.
Source: §9 · p. 19Takeaways & Limitations
The survey presents interleaving automated reasoning and machine learning as a way to build systems that can improve their skills and continue finding harder proofs and explanations over time.
Source: §1 · p. 2Decomposing human-oriented tactic scripts into sequences or trees of simpler commands for machine learning is a difficult preprocessing step.
Source: §7.3 · p. 18
Abstract
from arXiv · showhide
Automated theorem provers and formal proof assistants are general reasoning systems that are in theory capable of proving arbitrarily hard theorems, thus solving arbitrary problems reducible to mathematics and logical reasoning. In practice, such systems however face large combinatorial explosion, and therefore include many heuristics and choice points that considerably influence their performance. This is an opportunity for trained machine learning predictors, which can guide the work of such reasoning systems. Conversely, deductive search supported by the notion of logically valid proof allows one to train machine learning systems on large reasoning corpora. Such bodies of proof are usually correct by construction and when combined with more and more precise trained guidance they can be boostrapped into very large corpora, with increasingly long reasoning chains and possibly novel proof ideas. In this paper we provide an overview of several automated reasoning and theorem proving domains and the learning and AI methods that have been so far developed for them. These include premise selection, proof guidance in several settings, AI systems and feedback loops iterating between reasoning and learning, and symbolic classification problems.
1 Introduction
Automated reasoning and theorem-proving systems are theoretically general, but combinatorial explosion and practical choice points limit their ability to solve hard problems efficiently. The survey reviews how machine learning can guide these systems and how reasoning and learning can be combined.
1 Introduction
- Combinatorial explosion and choices about theories, lemmas, tactics, and inference steps can keep AR and ATP systems from solving hard problems in reasonable time.These choices affect efficiency and practical performance rather than the theoretical correctness and completeness of proof mechanisms.Source: §1 · pp. 1–2
- Machine learning offers data-driven methods for automating heuristic design and for interleaving learning with reasoning in feedback loops.Such systems may continue improving and find harder proofs and explanations over time.Source: §1 · p. 2
- The survey traces work from early AI and theorem-proving systems through premise selection, varied guidance architectures, learning trade-offs, and combinations of machine learning with automated reasoning.It focuses mainly on automated and interactive theorem proving and is not exhaustive of the broader automated-reasoning field.Source: §1 · p. 2
2 Early History
Early work combined symbolic and statistical learning with automated reasoning, while large formal libraries and benchmarks made premise selection a central focus. Initial premise-selection approaches improved performance in large-theory settings and opened further research questions.
2 Early History
- Early AI systems proposed concepts and conjectures, while logicist proof procedures based on transformations and calculi largely prevailed in ATP’s first decades.Examples of the heuristic direction include the Automated Mathematician, Bacon, and HR; resolution, DPLL, and paramodulation advanced the logicist direction.Source: §2 · p. 2
- In the 1990s, the Munich AR group combined ATP with statistical and symbolic learning, including tree neural networks and proof guidance from abstractions of related searches.Otter’s hints similarly used subsumption-based abstractions of lemmas from related proofs.Source: §2 · p. 3
- Large ITP libraries, including Mizar, became targets for learning; MPTP released about 30,000 Mizar ATP problems in 2003 and supported early large-scale ATP and ML experiments.Mizar Proof Advisor trained a naive Bayes predictor to select library facts, while Isabelle/Sledgehammer introduced non-learning premise-selection methods.Source: §2 · p. 3
- The MPTP Challenge and CASC LTB established large-theory benchmarks, followed by fast non-learning selectors such as SInE and meta-systems such as MaLARea.MaLARea interleaved proving with learning premise selection.Source: §2 · p. 3
- Early selectors used symbolic overlap and symbol rarity, while Mizar Proof Advisor and MaLARea learned associations between conjecture features and premise names.Later learned features included term walks and semantic features derived from finite models.Source: §2 · p. 3
- MePo, SInE, and MaLARea considerably increased the performance of underlying ATPs in large theories, prompting questions about formula representation, learning methods, guidance levels, and feedback loops.The survey presents these as topics for subsequent research rather than resolving them here.Source: §2 · pp. 3–4
3 Characterization of Mathematical Knowledge
The section examines how mathematical knowledge can be represented for machine learning, from syntactic features to semantic and neural representations. Across these approaches, the central design tension is capturing useful structure and meaning while keeping representations practical and discriminative.
3.1 Syntactic Features
- Mathematical representations matter because theorem statements and their proofs may involve seemingly distant areas, making semantic characterization important for extracting relevant notions.Early syntactic premise-selection features extended symbols with normalized subterms and type information, including variable-based normalizations.Source: §3 · p. 4, §3.1 · p. 4
- TF-IDF feature weighting considerably improved the performance of the best k-nearest-neighbor predictors using the many syntactic features.The section also describes term-graph walks as a way to capture global structure and share automatically created features.Source: §3.1 · pp. 4–5
3.2 ENIGMA Syntactic Features
- ENIGMA represents clauses as numeric vectors, initially using top-down symbol paths of length three with variables and Skolem symbols renamed to special tokens.Later versions restricted enumerated triples to those in training data, added count, horizontal, and conjecture features, and introduced feature hashing and symbol anonymization.Source: §3.2 · pp. 5–6
- Appending conjecture features made ENIGMA’s predictions goal-specific, a capability reported as essential for heterogeneous Mizar problems.The first ENIGMA recommended the same clauses independently of the conjecture.Source: §3.2 · p. 6
3.3 More Semantic Features
- Semantic features address cases where syntactic similarity poorly reflects meaning; MaLARea-SG1 dynamically searched for countermodels and reported considerable performance improvement.Other approaches used unifiability-related indexing features and latent semantic analysis embeddings based on term co-occurrence.Source: §3.3 · pp. 6–7
3.4 Characterization Using Neural Networks
- Neural approaches range from embeddings and encoder-decoder models to tree neural networks that represent the recursive structure of expressions.ENIGMA-NG composes learned symbol functions to encode terms and uses a separate recurrent model for clauses as sets.Source: §3.4 · pp. 7–8
- Name-invariant graph embeddings can improve cross-domain generalization, but may lose structure, such as encoding f(t1, t2, t1) and f(t2, t1, t2) identically.In another reported trade-off, graph-based predictions could be too confident; entropy regularization was introduced to normalize confidence and improve accuracy.Source: §3.4 · p. 8
4 Premise Selection
Premise selection narrows the facts considered by a prover, helping avoid the overload of possible deductions. The section surveys learning methods ranging from similarity-based and probabilistic selection to trees and neural models.
4 Premise Selection
- Premise selection identifies facts relevant to a conjecture, helping keep automated theorem provers from being overwhelmed by possible deductions.The section focuses on learning-based approaches, alongside non-learning heuristics such as MePo and SInE.Source: §4 · p. 9
4.1 k-Nearest Neighbors (k-NN)
- k-NN ranks facts by similarity using feature-based distances, with weights and a scaling factor added to increase precision.Relevance scores are adjusted for the number of proof dependencies, and adaptive k can vary the number of neighbors considered.Source: §4.1 · p. 9
4.2 Naive Bayes
- Naive Bayes can account for absent goal features by considering only related extended features, whose probabilities can be estimated efficiently.Implementations include SNoW and a custom system for Flyspeck and other experiments.Source: §4.2 · pp. 9–10
4.3 Decision Trees
- Decision trees and ensembles support premise selection; gradient-boosted trees require (pseudo-)negative examples, which ATPBoost generates through an interleaved proving-and-training loop.Hashing millions of sparse symbolic features into a much smaller space enabled efficient training over large libraries with practically no performance penalties.Source: §4.3 · p. 10
4.4 Neural Methods
- Neural premise selection spans graph neural networks, graph sequence models, directed graph networks, recurrent networks, and transformers.Some models also account for dependencies among premises.Source: §4.4 · pp. 10–11
- A signature-independent GNN appears strongest in a large Mizar evaluation, which also demonstrates a role for ensembles and portfolios.Some neural methods can also propose unproved intermediate conjectures that split a problem into two.Source: §4.4 · p. 11
5 Guidance of Saturation-based ATPs
Machine learning guides saturation-based provers primarily by prioritizing clauses, but guidance must balance model quality with runtime efficiency. The section surveys alternative guidance targets, ways to combine learned and original heuristics, and methods for incorporating problem and proof-state context.
Clause selection
- Clause selection is a natural target for learned guidance because even small quality improvements can greatly affect prover performance.At each proving-loop iteration, it chooses the next clause to activate; an ideal selector would choose only clauses in the yet-undiscovered proof.Source: §5 · p. 11
Learning from proofs
- Learned clause guidance trains a binary classifier on clauses in discovered proofs versus other selected clauses, then prioritizes positively classified clauses.The approach traces back at least to Schulz.Source: §5 · p. 11
Efficiency trade-offs
- Guidance must balance representation faithfulness, model capacity, and the speed of learning and retrieval; higher-quality advice may lose if it takes too long.Faster guidance can also let self-learning systems produce more training data in a fixed time.Source: §5 · p. 11
Integrating learned advice
- Models can impose a total clause order and then replace or combine with the original selection heuristic; binary predictions may be ordered using clause length, age, or logits.ENIGMA’s score combines classification with clause length, while ENIGMA-NG prioritizes positive clauses and uses generation time as a tiebreaker.Source: §5 · p. 12
- Learned advice may be combined with the original heuristic, and Deepire’s layered selection performed best while allowing lazy model evaluation.In iProver, GNN-only guidance recently outperformed combining the model with original heuristics, with learning from dynamic proof data cited as one reason.Source: §5 · p. 13
Signature dependence
- Signature-dependent clause representations can tie guidance to one domain, while Deepire classifies clauses from derivation history and remains tied to a fixed initial axiom set [144,145].Signature-independent approaches include arity abstractions and invariant neural embeddings.Source: §5 · p. 13
Context
- Conjecture context can improve guidance, while proof-progress context ranges from ENIGMAWatch’s completion-ratio vector to TRAIL’s costly multiplicative attention [49].Under practical time constraints, TRAIL did not improve over plain E prover.Source: §5 · pp. 13–14
Beyond clause selection
- Beyond clause selection, ML can suggest term orderings, symbol weights, ATP strategies, and strategy schedules, and can support iterative Split & Merge algorithms [9,10,153,133,87,64,19].These approaches also include preventing interactions between unsuitable clauses [48].Source: §5 · p. 14
6 Guidance of Tableaux and Instantiation-based ATPs
Machine learning guides both tableaux-based and instantiation-based provers, where it can prioritize inference steps or improve the production of ground instantiations. Reported results include more solved test problems for rlCoP and doubled iProver performance on Mizar.
Tableaux-based provers
- After several proving-and-learning iterations, rlCoP solved 40% more test problems than default leanCoP, though its proofs remained rather short.Its Alpha-Zero-like architecture guides connection tableaux using reinforcement-learned policy and value estimates [76].Source: §6 · p. 15
- MaLeCoP’s guidance avoided 90% of inferences, and FEMaLeCoP made extension-step selection faster with an integrated sparse naive Bayes classifier.MonteCoP instead uses Monte Carlo simulations to select promising branches.Source: §6 · p. 15
Instantiation-based and SMT systems
- Instantiation-based and SMT systems combine SAT checking of ground (un)satisfiability with methods for producing suitable ground instantiations.The approach has become more relevant with powerful CDCL-based SAT solving and other calculus improvements.Source: §6 · p. 15
- Efficient neural guidance of iProver’s Inst-Gen procedure doubled its performance on the Mizar corpus.SMT machine learning has mainly addressed portfolio and strategy optimization, with newer work exploring decision trees, manual features, and neural guidance for cvc5 [109].Source: §6 · p. 15
7 Tactic Based ITP Guidance
Tactic-based guidance predicts higher-level proof actions from existing tactical proofs, placing it between premise selection and low-level ATP guidance. The section surveys its systems, advantages, and challenges.
7 Tactic Based ITP Guidance
- Tactic-based guidance learns to recommend actions from existing tactical proofs, with recommendations made for a given proof state.Tactics can range from simple inference steps to domain-specific procedures and generic proof search.Source: §7 · p. 16
7.1 Overview
- TacticToe combines tactic prediction with Monte-Carlo tree search, proving 66% of the HOL4 library in its later versions.Other systems span Coq, HOL Light, Isabelle, Lean, and frameworks for exploring tactical proof spaces.Source: §7.1 · p. 16
7.2 Advantages of Tactic-based ITP Guidance
- Tactics offer adaptive, higher-level actions, while expert-written domain-specific tactics can support specialized mathematics and learnable new actions.Examples include Coq tactics for Iris separation logic and custom HOL tactics in CakeML.Source: §7.2 · pp. 16–17
7.3 Challenges in Tactic-based ITP Guidance
- Tactics may not form a complete set of inference rules, and overlapping functionality can leave systems with redundant actions.Tactician and Proverbot9001 decompose and normalize tactic expressions; TacticToe orthogonalizes goal-tactic pairs to prefer successful tactics with broad coverage.Source: §7.3 · p. 17
- Tactic behaviors vary in execution time, making tactic selection and resource allocation difficult; human-oriented tactic languages also require difficult decomposition into simpler commands.Simple tactics may execute quickly, while sophisticated ones can take multiple seconds.Source: §7.3 · pp. 17–18
- Graph2Tac generates representations for unseen definitions on the fly, and its richer proof-state and tactic-argument representations improve performance by 50% over baselines without that background information.This addresses the expense of adapting large neural models as new concepts and lemmas are added.Source: §7.3 · p. 18
8 Related Symbolic Classification Problems
The survey places symbolic classification both inside and alongside reasoning systems, reviewing neural-symbolic methods for logic programs, theorem proving, and inductive logic programming.
8 Related Symbolic Classification Problems
- Most work classifies symbolic expressions to guide a symbolic system’s choice of action, while some classification approaches operate without such integration.The latter approaches motivated tree-neural-network guidance for clause selection.Source: §8 · p. 18
- Neural predicates in probabilistic logic programs support training within a symbolic setting, while other work explores soft unification for neural theorem proving and adversarial prover-teacher training.DeepProbLog introduces an approach to train neural predicates in probabilistic logic programs [96].Source: §8 · p. 18
- Inductive logic programming derives explanatory hypotheses from examples and background knowledge; nFOIL models FOIL’s search and stopping conditions with Naive Bayes.nFOIL seeks to maximize the probability that a hypothesis covers the examples, stopping when its score reaches a user-defined threshold.Source: §8 · p. 19
- δILP encodes inductive logic programming as a satisfiability problem with soft inferencing, and later work interleaves the neuro-symbolic system with a symbolic solver for training feedback.Related neural SAT approaches instead use a graph neural network or formulate satisfiability as a semidefinite program.Source: §8 · p. 19
9 Conclusion
The survey reviews contemporary combinations of automated reasoning and machine learning, while noting that language-model performance in fair-resource ATP evaluations remains questionable against targeted architectures. It concludes that combining deductive, search, and symbolic methods with learning offers an open direction for AI/TP research.
9 Conclusion
- The survey covers the history, mathematical knowledge, premise selection, machine-learning-guided ATP, reasoning-learning feedback loops, and related symbolic classification problems.Source: §9 · p. 19
- Language models can generate informal mathematics, but their ATP performance beyond high-school and olympiad tasks remains questionable in fair-resource comparisons with targeted architectures such as signature-independent graph neural networks.Source: §9 · p. 19
- The survey identifies emergence and benchmark memorization as debated language-model research questions, including memorization of benchmark problems, proofs, and informal presentations available online.Source: §9 · p. 19
- The authors argue that combining deductive, search, and symbolic methods with learning may yield complex, novel AI architectures and describe AI/TP research as open.Source: §9 · p. 20