Summary (Overview)

• This paper presents a comprehensive experimental study of neural clause-selection guidance in the VAMPIRE automated theorem prover across four benchmark families: TPTP, Mizar40, Isabelle/Sledgehammer, and CoqHammer.
• Neural guidance consistently improves performance within individual domains (up to +248.3% on training sets), but models fail to transfer across datasets, often underperforming the unguided default strategy.
• Training a single model on all datasets simultaneously recovers most of the per-dataset performance (95.3–101.4% of dedicated models), suggesting the model capacity is sufficient but domain-specific encoding details matter.
• Neural guidance can compensate for inefficient calculi: boosting an unordered resolution/plain paramodulation strategy lifts it above the unguided default's performance.
• At portfolio scale, a combined schedule (plain + neural strategies) covers 4.1% more problems overall and achieves 12.2% improvement at the practically relevant ~10s time limit.

Introduction and Theoretical Foundation

The work builds on a previously introduced neural clause-selection guidance system for VAMPIRE, inspired by reinforcement learning (RL). The key insight is that learned clause selection can outperform handcrafted heuristics in fixed settings, but several open questions remain:

1. Broader effectiveness: Does the improvement observed on TPTP carry over to ITP-derived benchmarks with structurally different problem distributions?
2. Transfer: How well do models trained on one benchmark family generalize to others?
3. Portfolios: How does neural guidance interact with strategy diversity and optimized strategy portfolios?

The theoretical foundation rests on the idea that clause selection in saturation-based provers is a critical bottleneck. The neural approach replaces handcrafted ranking heuristics with a graph-based scoring model iteratively trained on proof traces.

Methodology

Neural Guidance Architecture

The neural network consists of four connected components:

• GNN (Graph Neural Network): Processes the input problem's CNF in several message-passing rounds, producing embeddings of input clauses and signature symbols
• RvNN (Recursive Neural Network) for derivation history: Computes embeddings of derived clauses by combining parent embeddings with derivation rule information
• Second RvNN for term structure: Computes embeddings of compound terms using GNN embeddings of signature symbols
• Fully-connected NN: Processes concatenated embeddings plus simple clause features (age, weight, number of literals) to produce a single score

Training Process

The iterative training loop repeats until performance stops improving:

1. Evaluate (plain or neurally-guided) VAMPIRE on training problems, collecting traces from successful attempts
2. Use traces to compute a loss function expressing that proof clauses should score higher than non-proof clauses
3. Update network parameters via gradient descent

Datasets

• TPTP: 15,500 problems (CNF, FOF, TF0 formats, excluding non-theorems and arithmetic)
• Mizar40: 57,880 "bushy" problems from Mizar Mathematical Library export
• Isabelle: 276,363 Sledgehammer problems (TFF encoding)
• CoqHammer: 82,366 FOL problems from Coq/Rocq

Experimental Setup

• Resource limit: 32 billion CPU instructions per problem (~12s on servers)
• Hardware: AMD EPYC 7513 (128 cores, 2.6 GHz), 500 GB RAM
• Training uses 64 cores, evaluation uses 120 cores
• 25 training iterations total; each TPTP iteration takes ~90 minutes

Empirical Validation / Results

Per-Dataset Performance (Table 1)

Key Findings

1. Knowledge Transfer: Models trained on one dataset consistently underperform the default strategy on other datasets. The only exception was TPTP→Mizar40, which was explained by TPTP containing 1,840 Mizar-exported problems.

2. Multi-Dataset Training: A single model trained on all four datasets achieved 100.0% (TPTP), 99.4% (Mizar40), 101.4% (Isabelle), and 95.3% (CoqHammer) of dedicated model performance.

3. Strategy Boosting: Five complementary strategies were boosted individually (average +24.0%), with the 5-strategy portfolio improving by 13.9% through boosting.

Strategy Portfolio Results (Table 2)

Weakened Calculus Experiment

The unconstrained strategy $S_0$ (unordered resolution, plain paramodulation) solved 40.4% of TPTP (vs. default's 55.3%), but after boosting reached 61.3%—above the unguided default.

Spider-style Strategy Search Results

• Plain search: 569 strategies covering 12,720 problems
• Neural search: 244 strategies covering 13,195 problems
• Combined: 13,247 distinct problems

Portfolio Performance

• Combined schedule: 4.1% more problems than plain
• At 32,000 Mi mark: 76.1% vs 67.8% (12.2% improvement)
• Combined schedule more efficient: 3.7 Ti vs 4.7 Ti

Theoretical and Practical Implications

1. Domain-specific learning: The lack of transfer suggests neural guidance capitalizes on encoding-specific details rather than general theorem-proving principles. The GNN likely recognizes input sub-classes (e.g., Mizar type guards vs. Isabelle type tags) rather than learning universal proof strategies.

2. Model capacity: The multi-dataset training result (95.3–101.4% of dedicated performance) indicates model capacity is not the limiting factor at current scales.

3. Portfolio integration: Neural guidance adds diminishing returns in large portfolios where strategic complementarity already captures much of the feasible search space. However, the 12.2% improvement at practical time limits is substantial.

4. Calculus compensation: Neural guidance can tame prolific but inefficient calculi, suggesting potential for exploring theoretically interesting but computationally challenging proof systems.

Conclusion

The paper demonstrates that neural clause selection guidance consistently improves VAMPIRE's performance within individual domains but exhibits poor cross-domain transfer. The main takeaways are:

1. Strengths: Substantial single-strategy improvements, effective multi-dataset training, and meaningful portfolio-level gains at practical time limits.

2. Limitations: Poor transfer across datasets, diminishing returns in large portfolios, and evidence that the network exploits encoding-specific patterns rather than general mathematical principles.

Future directions include:

• Training larger models on larger datasets (using more of the available hammer-derived benchmarks)
• Exploring transformer architectures
• Investigating learned clause/symbol representations and encoding peculiarities across datasets
• Systematic analysis of why models fail to transfer (e.g., the differences in CNF graphs processed by the GNN)