mlsanityData to 7 Oct 2026

Proof Artifact Co-training for Theorem Proving with Language Models

arXiv 2102.06203 ↗First posted 11 Feb 2021cs.AI cs.LG cs.LOcited by 130

On the map: Offline RL and imitation learning from data → Language-conditioned policies and VLAs

Abstract (arXiv)

Labeled data for imitation learning of theorem proving in large libraries of formalized mathematics is scarce as such libraries require years of concentrated effort by human specialists to be built. This is particularly challenging when applying large Transformer language models to tactic prediction, because the scaling of performance with respect to model size is quickly disrupted in the data-scarce, easily-overfitted regime. We propose PACT (bf Proof bf Artifact bf Co-bf Training), a general methodology for extracting abundant self-supervised data from kernel-level proof terms for co-training alongside the usual tactic prediction objective. We apply this methodology to Lean, an interactive proof assistant which hosts some of the most sophisticated formalized mathematics to date. We instrument Lean with a neural theorem prover driven by a Transformer language model and show that PACT improves theorem proving success rate on a held-out suite of test theorems from 32% to 48%.

Key facts. Cited by 130 papers in the map (data through 7 Oct 2026). Placed in Language-conditioned policies and VLAs, one of 13 directions in Offline RL and imitation learning from data. Builds on 58 of its 94 references that are in the map. First posted on arXiv 11 Feb 2021.

Builds on

58 of 94 references.

References · 58

  1. 2017Attention Is All You Needcited by 59,932
  2. 2018BERT: Pre-training of Deep Bidirectional Transformers for Language Understandingcited by 40,204
  3. 2020Language Models are Few-Shot Learnerscited by 32,199
  4. 2020An Image is Worth 16x16 Words: Transformers for Image Recognition at Scalecited by 29,915
  5. 2019Exploring the Limits of Transfer Learning with a Unified Text-to-Text Transformercited by 14,491
  6. 2018Representation Learning with Contrastive Predictive Codingcited by 7,662
  7. 2020Scaling Laws for Neural Language Modelscited by 6,411
  8. 2018Unsupervised Representation Learning by Predicting Image Rotationscited by 1,586
  9. 2019fairseq: A Fast, Extensible Toolkit for Sequence Modelingcited by 1,486
  10. 2016Context Encoders: Feature Learning by Inpaintingcited by 1,424
  11. 2016Unsupervised Learning of Visual Representations by Solving Jigsaw Puzzlescited by 1,379
  12. 2019Cross-lingual Language Model Pretrainingcited by 1,088
38 more
  1. 2015Unsupervised Visual Representation Learning by Context Predictioncited by 1,062
  2. 2020CURL: Contrastive Unsupervised Representations for Reinforcement Learningcited by 745
  3. 2019Unified Language Model Pre-training for Natural Language Understanding and Generationcited by 668
  4. 2019Using Self-Supervised Learning Can Improve Model Robustness and Uncertaintycited by 511
  5. 2020Scaling Laws for Autoregressive Generative Modelingcited by 510
  6. 2019Unlabeled Data Improves Adversarial Robustnesscited by 415
  7. 2016Reinforcement Learning with Unsupervised Auxiliary Taskscited by 400
  8. 2020Generative Language Modeling for Automated Theorem Provingcited by 379
  9. 2019MASS: Masked Sequence to Sequence Pre-training for Language Generationcited by 345
  10. 2019Deep Learning for Symbolic Mathematicscited by 266
  11. 2018Learning a SAT Solver from Single-Bit Supervisioncited by 198
  12. 2018An efficient framework for learning sentence representationscited by 197
  13. 2017End-to-End Differentiable Provingcited by 159
  14. 2020Adversarial Robustness: From Self-Supervised Pre-Training to Fine-Tuningcited by 152
  15. 2019The Lean mathematical librarycited by 127
  16. 2019Learning to Prove Theorems via Interacting with Proof Assistantscited by 107
  17. 2016DeepMath - Deep Sequence Models for Premise Selectioncited by 80
  18. 2018Reinforcement Learning of Theorem Provingcited by 69
  19. 2019Graph Representations for Higher-Order Logic and Theorem Provingcited by 55
  20. 2018First Experiments with Neural Translation of Informal to Formal Mathematicscited by 52
  21. 2020Teaching Temporal Logics to Neural Networkscited by 51
  22. 2018GamePad: A Learning Environment for Theorem Provingcited by 48
  23. 2021LIME: Learning Inductive Bias for Primitives of Mathematical Reasoningcited by 46
  24. 2018TacticToe: Learning to Prove with Tacticscited by 43
  25. 2020Learning to Prove Theorems by Learning to Generate Theoremscited by 43
  26. 2019Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizarcited by 40
  27. 2019Generating Correctness Proofs with Neural Networkscited by 36
  28. 2016Holophrasm: a neural Automated Theorem Prover for higher-order logiccited by 29
  29. 2018Grasp2Vec: Learning Object Representations from Self-Supervised Graspingcited by 27
  30. 2019Learning to Reason in Large Theories without Imitationcited by 27
  31. 2017ENIGMA: Efficient Learning-based Inference Guiding Machinecited by 26
  32. 2017HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Provingcited by 26
  33. 2020First Neural Conjecturing Datasets and Experimentscited by 26
  34. 2018Can Neural Networks Understand Logical Entailment?cited by 24
  35. 2013MizAR 40 for Mizar 40cited by 23
  36. 2020ProGraML: Graph-based Deep Learning for Program Optimization and Analysiscited by 23
  37. 2020The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coqcited by 23
  38. 2019Hammering Mizar by Learning Clause Guidancecited by 20

50 most cited of 58 All 58 (JSON)

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2021: 5; 2022: 14; 2023: 22; 2024: 38; 2025: 26; 2026: 25.

130 papers.

Sort:

By area:

  1. 2022Solving Quantitative Reasoning Problems with Language Modelscited by 1,359
  2. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  3. 2023Llemma: An Open Language Model For Mathematicscited by 385
  4. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  5. 2024Large Language Models for Mathematical Reasoning: Progresses and Challengescited by 283
  6. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  7. 2022Autoformalization with Large Language Modelscited by 252
  8. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 225
  9. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  10. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 180
  11. 2022Formal Mathematics Statement Curriculum Learningcited by 141
  12. 2022A Survey of Deep Learning for Mathematical Reasoningcited by 124
38 more
  1. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 118
  2. 2024InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoningcited by 117
  3. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 115
  4. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
  5. 2022Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Proverscited by 97
  6. 2025BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Provingcited by 82
  7. 2021NaturalProofs: Mathematical Theorem Proving in Natural Languagecited by 80
  8. 2023An In-Context Learning Agent for Formal Theorem-Provingcited by 78
  9. 2022NaturalProver: Grounded Mathematical Proof Generation with Language Modelscited by 72
  10. 2024Lean-STaR: Learning to Interleave Thinking and Provingcited by 64
  11. 2021Linear algebra with transformerscited by 62
  12. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  13. 2023FIMO: A Challenge Formal Dataset for Automated Theorem Provingcited by 54
  14. 2024Lean Copilot: Large Language Models as Copilots for Theorem Proving in Leancited by 52
  15. 2023Magnushammer: A Transformer-Based Approach to Premise Selectioncited by 50
  16. 2025Aristotle: IMO-level Automated Theorem Provingcited by 47
  17. 2024Process-Driven Autoformalization in Lean 4cited by 45
  18. 2024MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Datacited by 43
  19. 2024Towards Scientific Discovery with Generative AI: Progress, Opportunities, and Challengescited by 41
  20. 2021TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learningcited by 37
  21. 2023Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Provingcited by 37
  22. 2024miniCTX: Neural Theorem Proving with (Long-)Contextscited by 35
  23. 2025Solving Formal Math Problems by Decomposition and Iterative Reflectioncited by 35
  24. 2024InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Searchcited by 34
  25. 2023LLMSTEP: LLM proofstep suggestions in Leancited by 32
  26. 2024Large Language Models for Education: A Surveycited by 32
  27. 2025Prover Agent: An Agent-Based Framework for Formal Mathematical Proofscited by 28
  28. 2024Autoformalizing Euclidean Geometrycited by 27
  29. 2025Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Proverscited by 26
  30. 2024Proving Theorems Recursivelycited by 25
  31. 2024LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN provercited by 25
  32. 2024Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verificationcited by 25
  33. 2023Lyra: Orchestrating Dual Correction in Automated Theorem Provingcited by 24
  34. 2023TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Modelscited by 24
  35. 2023Mathematical Language Models: A Surveycited by 24
  36. 2024FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Provingcited by 22
  37. 2024Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchicallycited by 22
  38. 2024Machine learning and information theory concepts towards an AI Mathematiciancited by 20

50 most cited of 130 All 130 (JSON)

Similar, not cited

Close in wording, no citation either way

  1. 2025ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations
  2. 2025StepFun-Prover Preview: Let's Think and Verify Step by Step
  3. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
  4. 2025Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience
  5. 2025DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning
  6. 2026Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation
  7. 2026FormalRewardBench: A Benchmark for Formal Theorem Proving Reward Models
  8. 2025Theorem Prover as a Judge for Synthetic Data Generation