Research map / Architectures and efficiency / RNNs and normalization
BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Introduces BAIT, an open-source cross-platform framework for AI interactive theorem proving, and uses it to compare embedding architectures (GNN, Transformer, Structure Aware Transformers, ensembles) across supervised premise selection benchmarks and end-to-end TacticZero proving in HOL4.
Problem
Research on AI for interactive theorem proving is fragmented across ITP systems and learning approaches, making methods hard to compare and replicate; the choice of formula embedding architecture (graph vs sequence) has not been thoroughly compared across ITP systems.
Approach
A unified, modular framework (BAIT) with Data, Model, Environment and Experiment modules that standardises supervised and end-to-end AI-ITP tasks across systems, used to benchmark state-of-the-art embedding architectures including Structure Aware Transformers (and directed SAT) against GNNs and Transformers.
Key results
- Directed Structure Aware Transformer achieves the best premise selection accuracy on MIZAR40 (74.1) and LeanStep (97.0), and top-5 on HOList (85.1), outperforming GNN and Transformer baselines.
- On HOL4 end-to-end TacticZero, the GNN encoder reaches 64.6% validation pass@1 versus 43.0% for the original TacticZero autoencoder, roughly a 31% (relative) improvement claimed in the text.
- Transformers outperform GNN-only approaches overall in supervised tasks, and ensembles almost always beat their base GNN and Transformer models.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| restrict SAT attention to ancestor or descendant nodes | SAT embeddings · HOList Tactic | accuracy: 35.2 -> 39.1 | Helped |
| restrict SAT attention to ancestor or descendant nodes | SAT embeddings · HOList top-5 | accuracy: 81.2 -> 85.1 | Helped |
| restrict SAT attention to ancestor or descendant nodes | SAT embeddings · MIZAR40 Premise Selection | accuracy: 73.6 -> 74.1 | Helped |
| restrict SAT attention to ancestor or descendant nodes | SAT embeddings · LeanStep Premise Selection | accuracy: 96.6 -> 97.0 | Helped |
| restrict SAT attention to ancestor or descendant nodes | SAT embeddings · HOL4 Premise Selection | accuracy: 91.0 -> 91.1 | No clear effect |
| replace the original seq2seq autoencoder with a GNN encoder pretrained on HOL4 premise selection | TacticZero · HOL4 TacticZero validation | pass@1: 43.0% -> 64.6% | Helped |
| replace the original seq2seq autoencoder with a Transformer encoder pretrained on HOL4 premise selection | TacticZero · HOL4 TacticZero validation | pass@1: 43.0% -> 63.3% | Helped |
| replace the original seq2seq autoencoder with a GNN encoder pretrained on HOL4 premise selection | TacticZero · HOL4 TacticZero training | cumulative goals proven: 90.7% -> 96.2% | Helped |
| replace the original seq2seq autoencoder with a Transformer encoder pretrained on HOL4 premise selection | TacticZero · HOL4 TacticZero training | cumulative goals proven: 90.7% -> 96.8% | Helped |
| combine GNN and Transformer embeddings | embedding models · HOList Tactic | accuracy | Helped |
| use a Bag of Words model instead of learned embedding architectures | supervised embedding benchmarks · HOList Relative Parameter | accuracy | No clear effect |
Surprising findings
- Directed SAT did not help on the small HOL4 premise selection dataset, where the complex SAT model is likely insufficient for learning.
- A Bag of Words (0-layer GNN) baseline performed poorly on most benchmarks, except the HOList relative parameter accuracy.
Limitations
- Could not evaluate Directed SAT on HOLStep due to expensive preprocessing.
- HOList models were not extensively evaluated end-to-end due to compute constraints (prior work used 2000 CPUs).
- Tree-LSTMs and CNNs were not evaluated.
Experimental setup
Datasets: HOList HOLStep MIZAR40 LeanStep HOL4 standard library premise selection
Benchmarks: HOList HOLStep MIZAR40 LeanStep HOL4 premise selection TacticZero HOL4 end-to-end
Metrics: accuracy relative parameter accuracy top-5 accuracy cumulative goals proven validation pass@1
Baselines: TacticZero GNN Transformer Bag of Words SAT DAG-LSTM
Builds on: TacticZero HOList INT Structure Aware Transformer ReProver
Closest papers by meaning
- Magnushammer: A Transformer-Based Approach to Premise Selection (ICLR 2024 · similarity 0.90)
- ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis (ICML 2025 · similarity 0.88)
- LEGO-Prover: Neural Theorem Proving with Growing Libraries (ICLR 2024 · similarity 0.88)
- A Minimal Agent for Automated Theorem Proving (ICML 2026 · similarity 0.88)
- Alchemy: Amplifying Theorem-Proving Capability Through Symbolic Mutation (ICLR 2025 · similarity 0.88)
- Subgoal-based Demonstration Learning for Formal Theorem Proving (ICML 2024 · similarity 0.87)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.