# Teaching Vampire New Tricks: An Experimental Study of Neural Clause Selection

> Neural clause selection consistently boosts VAMPIRE within domains but fails to transfer across datasets, though multi-dataset training recovers most performance.

- **Source:** [arXiv](https://arxiv.org/abs/2609.16228)
- **Published:** 2026-09-19
- **Permalink:** https://picx.dev/p/bpJQgQ
- **Whiteboard:** https://picx.dev/p/bpJQgQ/image

## Summary

## 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)

| dataset | train | test |
|---------|-------|------|
| TPTP | (8511 → 10864)/15500 (+27.6%) | — |
| Mizar40 | (4733 → 10098)/15000 (+113.4%) | (1543 → 3101)/5000 (+101.0%) |
| Isabelle | (6435 → 8788)/15000 (+36.6%) | (2178 → 2715)/5000 (+24.7%) |
| CoqHammer | (2813 → 9799)/30000 (+248.3%) | (399 → 772)/5000 (+93.5%) |

### 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)

| Plain Strategy | #solved | Boost | Neural Counterpart | #solved |
|----------------|---------|-------|-------------------|---------|
| 1 | 9,265 | +21.6% | 1' | 11,264 |
| 2 | 8,395 | +29.1% | 2' | 10,839 |
| 3 | 8,999 | +18.6% | 3' | 10,675 |
| 4 | 5,936 | +19.9% | 4' | 7,118 |
| 5 | 8,078 | +30.4% | 5' | 10,533 |
| **Union:** | **10,719** | **+13.9%** | | **12,207** |

### 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)

---

_Markdown view of https://picx.dev/p/bpJQgQ, served by PicX — AI-generated visual whiteboard summaries of research papers._