Research map / Learning theory and algorithms / Combinatorial and search optimization
Graph2Tac: Online Representation Learning of Formal Math Concepts
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.
Proposes Graph2Tac, a GNN with a definition-embedding task that builds hierarchical representations of new Coq definitions online, and benchmarks it against an online k-NN solver and other Coq provers in Tactician.
Problem
Neural theorem provers for Coq struggle to use definitions and lemmas introduced in new packages unseen during training; offline models cannot incorporate online information from new definitions and proofs.
Approach
Exploit locality of formal libraries: a graph neural network encodes Coq's global knowledge as a mono-graph and computes hierarchical embeddings for new definitions via a co-trained definition embedding task, while an online k-NN learns from recent proofs.
Key results
- Online k-NN proves 25.8% of test theorems vs 15.0% for offline k-NN (1.72x).
- Graph2Tac with definition task reaches 26.1% vs 17.4% for the frozen-embedding baseline (1.5x).
- Combined G2T-Anon-Update + k-NN-online reaches 33.2% pass rate, beating CoqHammer combined (17.4%) and transformers (10.5%-14.8%).
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Add online learning from recent proofs instead of searching the offline training proofs | k-NN solver · Coq test theorems, 10-minute evaluation | pass rate: 15.0% to 25.8% (1.72x) | Helped |
| Add the definition task to compute embeddings for new definitions (ablation) | Graph2Tac · Coq test theorems, 10-minute evaluation | pass rate: 17.4% vs 26.1% | Helped |
| Add definition name embeddings (ablation) | G2T-Anon-Update · Coq test theorems, 10-minute evaluation | pass rate: 0.261 -> 0.241 | Hurt |
| Combine online definition learning with online learning from recent proofs | G2T-Anon-Update and kNN-online · Coq test theorems, 10-minute evaluation | pass rate: 1.27× | Helped |
Surprising findings
- Graph2Tac trained with named definitions (G2T-Named-Update) performed slightly worse than anonymous version, suggesting names make the definition task too easy.
Limitations
- Results are sensitive to the package-based split; excluding hott and tlc heavily influences results, and tlc was solved via an inconsistency.
- Graph2Tac only predicts local hypotheses or global definitions as arguments and uses a fixed set of base tactics, so it cannot predict arbitrary term arguments.
- Transformer baseline is trained from scratch and smaller than pretrained transformer provers, so comparison is approximate.
Experimental setup
Datasets: Coq dataset of 120 Opam packages (Tactician graph dataset)
Benchmarks: randomly sampled 2000 test theorems from Coq packages held out by package split
Metrics: fraction of theorems proved pass rate over time pass rate over model calls
Baselines: k-NN offline CoqHammer Transformer-CPU Transformer-GPU firstorder auto with * G2T-NoDef-Frozen
Builds on: Tactician CoqHammer GPT-2
Closest papers by meaning
- REFACTOR: Learning to Extract Theorems from Proofs (ICLR 2024 · similarity 0.86)
- Subgoal-based Demonstration Learning for Formal Theorem Proving (ICML 2024 · similarity 0.86)
- miniCTX: Neural Theorem Proving with (Long-)Contexts (ICLR 2025 · similarity 0.86)
- ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis (ICML 2025 · similarity 0.86)
- PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition (NeurIPS 2024 · similarity 0.86)
- ImProver: Agent-Based Automated Proof Optimization (ICLR 2025 · similarity 0.85)
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.