PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Karel Chvalovský, Martin Suda, Josef Urban

arXiv:2609.16228v1cs.LO

TL;DR

Neural clause guidance had improved Vampire on TPTP, but its generalization across ITP-derived benchmarks and interaction with strategy portfolios remained uncertain. This study evaluates those settings and finds consistent within-domain gains but poor cross-dataset transfer; combined portfolios still yield a practical TPTP improvement.

  • Problem

    It was unclear whether neural clause-selection gains on TPTP generalize across distinct ITP-derived benchmark families and improve portfolios of complementary proving strategies.

    Source: §1 · p. 1

  • Method

    The study evaluates neural clause guidance across TPTP, Mizar40, Isabelle/Sledgehammer, and CoqHammer, including transfer between datasets, optimized strategies, and portfolio construction.

    Source: §1 · p. 2

  • Results

    Guidance consistently improves performance within datasets but its learned advantage disappears when the target dataset changes; combined TPTP portfolios show 12.2 % improvement at a practically relevant time limit.

    Source: §9 · p. 14

  • Takeaways & Limitations

    Neural guidance remains useful for individual strategies and combined portfolios, but its marginal value diminishes as portfolio strategic complementarity captures more of the feasible-to-claim search space.

    Source: §1 · p. 2, §9 · p. 14

    The experiments rely on only fractions of the hammer-derived benchmarks, leaving larger datasets and alternative architectures as future directions.

    Source: §9 · p. 14

Abstract

from arXiv · show

A neural clause-selection guidance approach in the Vampire theorem prover was recently shown to substantially improve the success rate of the prover's default strategy on the TPTP benchmark. We experimentally study the impact of the approach across several ITP-derived benchmark sets and its interaction with theorem proving strategies. We find that while the neural guidance consistently improves performance within individual benchmark domains, cross-benchmark application of guiding models underperforms the plain default strategy. This can be remedied by training a single model on all datasets at once. Such a model, although more expensive to obtain, helps Vampire almost catch up in performance across all datasets. The picture when considering combined strategies is less clear-cut, indicating persisting value of neural guidance but under diminishing returns.

1 Introduction

This study tests neural clause guidance on ITP-derived benchmarks and across proving strategies, finding strong within-domain gains but weak cross-domain transfer and diminishing portfolio returns. It also evaluates combined portfolios, where neural and standard strategies improve TPTP performance at a practical time limit.

1 Introduction

  • The study asks whether gains observed on TPTP carry over to ITP-derived benchmarks, whether models transfer across benchmark families, and how neural guidance interacts with strategy diversity.These questions matter because ATPs are increasingly used as hammers for ITPs, whose problem distributions differ substantially from classical ATP benchmarks.Source: §1 · pp. 1–2
  • Across TPTP, Mizar40, Isabelle/Sledgehammer, and CoqHammer, the experiments examine per-dataset gains, cross-dataset transfer, locally optimized strategies, and portfolio construction.The approach builds on an RL-inspired system that replaces handcrafted clause-ranking heuristics with a neural model trained iteratively on proof traces.Source: §1 · pp. 1–2
  • Neural guidance consistently improves performance within individual domains, but models trained on one dataset typically transfer poorly and can underperform the unguided default.A single model trained on all datasets can remedy the transfer problem, at increased computational cost.Source: §1 · p. 2
  • Neural boosting substantially improves individual strategies, but its marginal benefit shrinks in larger portfolios where strategic complementarity already captures much of the feasible-to-claim search space.The study also finds that one neural model can guide more than one strategy.Source: §1 · p. 2
  • Neural guidance can lift unordered resolution with plain paramodulation above the unguided default strategy, which uses superposition and a simplification ordering.This result shows that guidance can compensate for inefficiencies in the weakened strategy.Source: §1 · p. 2
  • 12.2 % improvement on TPTP at a practically relevant ∼10 s time limit came from a portfolio combining standard and neurally guided strategies.The combined portfolio covered 4.1 % more problems overall; this was the first portfolio-scale evaluation of neural clause selection.Source: §1 · p. 2

2 Background: Neural Clause Guidance in Vampire

Vampire ranks clauses using neural scores learned from successful proof traces. Its model combines representations of input clauses, derivation histories, and term structure, and is trained iteratively using proof-search traces.

2 Background: Neural Clause Guidance in Vampire

  • The neural model scores clauses using input-problem, derivation-history, and term-structure representations, together with simple clause features.A graph neural network embeds input clauses and signature symbols; two recursive networks represent derived clauses and terms, and a fully connected network produces each score.Source: §2 · p. 3
  • The graph network runs once after CNF preprocessing, while the two recursive networks update during saturation as new clauses are derived.The model's clause scores therefore draw on representations computed as proof search proceeds.Source: §2 · p. 3
  • Training alternates evaluation and trace collection on successfully solved problems with network updates based on a loss that ranks proof clauses above other candidates.The collected traces reconstruct the candidate clauses at each selection decision and identify which later appear in the proof.Source: §2 · p. 3
  • The first training iteration uses Vampire's built-in clause-selection heuristic because the randomly initialized network is not yet useful for guidance.Prover evaluation and network updates are computationally expensive but can be parallelized.Source: §2 · p. 3

3 Four Datasets

The experiments use four TPTP-format benchmark families: TPTP, Mizar40, Isabelle/Sledgehammer exports, and CoqHammer problems.

3 Four Datasets

  • TPTP contains 15 500 CNF, FOF, and TF0 problems from library version 9.1.0 after excluding non-theorems and problems containing arithmetic.The paper notes that its library-solved percentages are incompatible with those from prior work using TPTP v9.0.0, though percentage improvements remain comparable modulo the library version.Source: §3 · p. 4
  • Mizar40 comprises 57 880 “bushy” problems from the TPTP export of the Mizar Mathematical Library.Each conjecture is paired only with previously occurring lemmas and theorems needed according to the library's human-supplied proof.Source: §3 · p. 4
  • The Isabelle dataset contains 276 363 Isabelle Sledgehammer problems extracted with Mirabelle, using the many-sorted first-order encoding.The authors selected the TFF encoding from the two available encodings.Source: §3 · p. 4
  • The CoqHammer dataset contains 82 366 TPTP problems in the first-order-logic fragment, obtained using the same package set as prior work.The paper frames CoqHammer as analogous to Sledgehammer for Coq/Rocq.Source: §3 · p. 4

4 Experimental Setup

Experiments generally limit Vampire to 32 billion CPU instructions per problem, roughly 12 seconds on the study servers. Training and evaluation use distinct shuffling and trace-collection procedures.

4 Experimental Setup

  • The default per-problem limit is 32 billion CPU instructions, roughly 12 s on the study servers, and instruction limits are chosen for robustness under memory contention.The servers have AMD EPYC 7513 processors and 500 GB RAM; experiments use 120 of 128 cores.Source: §4 · p. 4
  • Training enables input and internal shuffling and reuses the same random seed for trace-collection reruns, while final model evaluation runs without shuffling.Each successful run requires a trace-collecting rerun with increased time and instruction limits because trace collection is more expensive than proof search alone.Source: §4 · p. 4
  • Model training uses 64 cores so computation graphs fit in memory, with non-sequential model updates that act as a form of regularization.Prover evaluation and training alternate for 25 iterations; a typical TPTP iteration takes around 90 minutes, for about 1.5 days of tuning.Source: §4 · p. 4
  • Table 1 reports solved-problem counts as default → boosted / total for the corresponding train or test set.The study focuses on low time limits associated with hammer settings.Source: §4 · p. 4, Table 1 · p. 5

5 Per-Dataset Neural Boosting and Transfer Learning

The section tests default-strategy neural guidance within and across four benchmark families, then assesses mixed-dataset training. Individual-domain gains coexist with poor transfer; a pooled model nearly matches dedicated models.

5 Per-Dataset Neural Boosting and Transfer Learning

  • Per-dataset models used Vampire’s fixed default strategy and dataset-specific training sets; all had held-out testing except TPTP.CoqHammer used 30,000 training problems because the default strategy solved few there; its test problems came from separate packages to avoid related train/test theorems.Source: §5 · p. 5, §5.1 · p. 5

5.1 Boostability

  • Test-set gains were substantial but smaller than training gains; CoqHammer’s train boost was +248.3% and its unseen-test boost was +93.5%.Isabelle was the hardest dataset on which to record an improvement.Source: §5.1 · p. 5

5.2 Knowledge Transfer

  • Cross-domain transfer generally fell below the default strategy; TPTP’s apparent Mizar40 exception vanished after removing 1,840 Mizar-exported problems.The authors consider encoding differences a plausible explanation, but their problem-level analysis found no single dominant cause.Source: §5.2 · pp. 6–7

5.3 Overfitting To Training Data

  • Mizar40 test performance improved through 25 iterations, while Isabelle plateaued from iteration 5 and peaked at iteration 10; CoqHammer peaked at iteration 20.The authors describe the Isabelle pattern as pointing toward overfitting; TPTP’s plotted performance is training performance.Source: §5.3 · p. 7

5.4 Training on All Four Datasets at Once

  • 100.0%, 99.4%, 101.4%, and 95.3% of dedicated-model test performance were reached by one all-dataset model trained for 17 days.The values correspond respectively to TPTP, Mizar40, Isabelle, and CoqHammer; the authors suggest model capacity was not the main limitation at these scales.Source: §5.4 · pp. 7–8

6 Strategy Boosting

The section tests neural guidance alongside optimized strategies and portfolio search, finding that guidance improves individual strategies while its benefits diminish in combined portfolios. It also shows that boosting can make an unordered calculus outperform the unguided default, and that combined schedules improve coverage at the standard cutoff.

6.1 Portfolio Construction via Greedy Cover and Local Search

  • Using greedy cover with local hill climbing, researchers selected strategies; the first uses Twee’s goal transformation and, with other non-default settings, solves 9265 versus 8574 problems for Vampire’s default strategy.The search used an instruction limit of 8000 Gi and a random TPTP subset of 7680 problems.Source: §6.1 · p. 9

6.2 Boosting the Baseline Strategies Individually

  • The five complementary strategies differ substantially from Vampire’s default, and neural guidance delegates clause selection to the model, reducing the strategies’ clause-selection complementarity.Strategy 4/4′ is the only one in the sequence enabling SInE premise selection, which is identified as a likely reason it adds problems after boosting.Source: §6.1 · p. 9, §6.2 · p. 10
  • Each of five strategies gains 24.0% on average from individual boosting, but boosting raises the five-strategy portfolio’s performance by 13.9%.The champion strategy’s added coverage from companions falls from 15.7% in the plain portfolio to 8.4% in the boosted one.Source: §6.2 · pp. 9–10

6.3 Boosting All Baseline Strategies Jointly

  • A single model trained jointly on traces from all five strategies achieves a 23.8% average strategy boost and 12,195 combined-coverage problems.Training slows correspondingly, but the model is almost as good as the five individually trained models.Source: §6.3 · p. 10

6.4 Making Vampire Smart Again

  • Boosting raises the unordered strategy S0 from 40.4% to 61.3% of TPTP, above the unguided default’s 55.3% but below the boosted default’s 70.3%.The experiment tests whether learned clause selection can compensate for the prolific but inefficient unconstrained calculus.Source: §6.4 · p. 10

6.6 Greedy Portfolio Construction

  • At 32,000 Mi, the combined schedule covers 76.1% versus 67.8% for the plain schedule, a 12.2% improvement, though ultimate coverage is only 4.1% higher.The combined schedule needs 3.7 Ti, compared with 4.7 Ti for the plain schedule.Source: Figure 3 · p. 11, §6.6 · p. 12

6.5 Spider-style Strategy Search

  • After 20 days, plain search produced 569 strategies covering 12,720 problems, while neural search produced 244 covering 13,195; together they covered 13,247 distinct problems.The search can continue to find coverage gains beyond 20 days, but with diminishing returns.Source: §6.5 · pp. 11–12

7 Strategies versus Neural Boosting

The section compares locally optimized champion strategies and their neurally boosted versions across four datasets. Local champion boosting gives the highest performance on each dataset, but champion transfer varies by dataset and the reasons for those differences are not fully clear.

7 Strategies versus Neural Boosting

  • Across all four datasets, boosting a local champion yields the highest performance, although the relative benefit varies by dataset.The figure compares dataset champions and their boosted versions with the default and its local boost.Source: §7 · p. 12, Figure 4 · p. 13
  • TPTP and Mizar40 champions improve on the default for both datasets, while CoqHammer and Isabelle champions are worse on the opposite pair; even the Isabelle champion is slightly worse than default on CoqHammer.Twee’s goal transformation is shared by the TPTP and Mizar40 champions; CoqHammer and Isabelle champions both turn off function-definition elimination and favor higher age-weight ratios.Source: §7 · pp. 12–13
  • The reasons for champion similarities and differences are not immediately clear, though the Mizar40 dataset shows the greatest potential improvement between its weakest and strongest strategies.The reported performance spread may change as models are trained on larger portions of the comparatively large hammer-derived datasets.Source: §7 · pp. 13–14

8 Related Work

Related work situates neural clause selection in a history of learning from proofs, including ENIGMA and other neural guidance systems. It also contrasts this study’s transfer setting with prior systems whose transfer evaluations were narrower or used smaller benchmark subsets.

8 Related Work

  • Early work discussed learning clause selection from successful proofs, while ENIGMA revived the approach for E and later incorporated recursive NNs, GNNs, and layered architectures.Convolutional NNs were also explored for E, and these systems were trained mainly on Mizar and later Isabelle/HOL.Source: §8 · p. 14
  • A large-scale ENIGMA-related evaluation reported about 60% success on Mizar40 in chainy mode and 75% in bushy mode under a resource-bounded setting comparable to the 2013 results.The passage notes technical differences from the present study, including that ENIGMA had not used dynamic data collection.Source: §8 · p. 14
  • Graph2Tac recommends Coq tactics directly using a GNN, whereas CoqHammer translates Coq theories to TPTP for an external solver and proof reconstruction.Graph2Tac uses precomputed embeddings for previously known symbols, unlike the described method.Source: §8 · p. 14
  • NIAGRA reported transfer across MPTP, M2k, and TPTP, but MPTP and M2k are both Mizar-based, and its TPTP subset contained fewer than 1,000 problems.The subset selection criterion was not specified.Source: §8 · p. 14

9 Conclusion

Neural guidance helps fixed-dataset proving strategies, but its added value diminishes in portfolios; the conclusion also identifies limited benchmark coverage and future research directions. The appendix describes changes to trace retention, training, and Vampire setup.

9 Conclusion

  • Guidance improves fixed-dataset strategies, but portfolio gains diminish; combined standard and neural strategies still yield 12.2% improvement on TPTP.The improvement is described as occurring within a practically relevant time budget.Source: §9 · p. 14
  • The experiments use only fractions of the hammer-derived benchmarks; future work could examine larger datasets, transformers, and learned representations.The authors suggest comparing clause and symbol representations and the peculiarities of dataset encodings.Source: §9 · p. 14

A Technical Differences to Previously Described Setup

  • After the first two iterations, training advances by exactly five epochs using all traces, avoiding later-iteration time spent on early stopping.The earlier setup often stopped after five epochs when validation loss worsened, despite continued training improvement.Source: A Technical Differences to Previously… · p. 20
  • Early stopping uses dist_to_good in the first two iterations, measuring how far future proof clauses rank from selection under current scores.The metric replaces differentiable loss as the early-stopping criterion in those iterations.Source: A Technical Differences to Previously… · p. 20
  • The GNN uses k = 5 message-passing rounds instead of k = 8, and training decays the learning rate by factor 0.933.The stated learning rate is α = 0.0002.Source: A Technical Differences to Previously… · p. 20
  • Training retains each problem’s trace for up to five consecutive iterations, even when newer models no longer solve that problem.At most one trace is kept per problem, with preference for the least recently discovered trace.Source: A Technical Differences to Previously… · p. 20
  • Neural guidance still degrades the limited-resource saturation loop into an Otter loop, while the integration was merged with Vampire 5.0.Vampire 5.0 introduced new defaults that should make its default strategy stronger, at least on TPTP, than the previous Vampire 4.9 basis.Source: A Technical Differences to Previously… · p. 20

D Comparing Models Trained on Different Datasets

The examples compare models trained on different datasets by examining their clause scores and, more importantly, the rankings those scores induce on the passive set. In the CSR217+1 run, the shadow model ranks some proof clauses poorly.

D Comparing Models Trained on Different Datasets

  • The authors commonly see transfer failures involving many incorrectly evaluated proof clauses rather than only a few necessary clauses.Source: D Comparing Models Trained on… · p. 21
  • Scores on the CSR217+1 run compare TPTP neural and CoqHammer shadow models; shadow-model scores for selected proof clauses are much lower.The figure also plots negated clause weight and age on a separate axis for comparison.Source: D Comparing Models Trained on… · pp. 21, 23, Figure 5 · p. 22
  • For the guided TPTP model, the run takes roughly 160 selection steps and the worst proof-clause rank is about 50; one clause ranks around 8000 under CoqHammer.A clause reaching rank 0 is selected immediately; the paper emphasizes induced rankings because model scores are not directly comparable.Source: Figure 6 · p. 22, D Comparing Models Trained on… · p. 23

D.1 Transfer Between Models Trained on Mizar

The Mizar40 model does not guide the SEU392+2 proof effectively, but it does guide a proof on bushy SEU392+1 despite scoring a heavy clause poorly. On SEU392+1, that guided run uses fewer activations than the TPTP-guided run, while TPTP-noMizar requires more.

D.1 Transfer Between Models Trained on Mizar

  • On SEU392+2, TPTP guidance ranks proof clauses well, but Mizar40-based rank reevaluation reveals high passive-set placements and its guided attempt fails.The authors suggest the Mizar40 model’s training on “bushy” problems as a possible explanation.Source: §D.1 · pp. 23–24, Figure 8 · p. 24
  • 338 activations with Mizar40 guidance versus 389 with TPTP guidance on SEU392+1; TPTP-noMizar required 2034 activations.Figure 10 compares proof-clause ranks on the passive set at each selection step.Source: Figure 10 · p. 25, §D.1 · p. 25
  • On bushy SEU392+1, absent from Mizar40’s training set, Mizar40-guided search proves the problem despite scoring a weight-51 clause poorly.The proofs select different weight-51 clauses, which the Mizar40 model scores roughly −50 versus −23.Source: §D.1 · pp. 24–25, Figure 9 · p. 24

Related papers

Loading 2609.16228v1…