REVIEW 9 cited by
Proof Artifact Co-training for Theorem Proving with Language Models
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
read the original abstract
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 P}roof {\bf A}rtifact {\bf C}o-{\bf T}raining), 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\%.
Forward citations
Cited by 9 Pith papers
-
ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
ProofAug extracts progressively coarser valid proof skeletons from failed LLM proof attempts and fills them with automated theorem provers, improving miniF2F pass rates and sample efficiency in Isabelle and Lean.
-
From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier
LLM formal provers must shift from competition solvers to research agents that handle open-ended, under-specified frontier mathematics under machine-checked rigor.
-
LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4
White-box proof search with factorized Lean 4 goals reaches 18.4% on MiniF2F with Llemma-7B, outperforming black-box generation at 9.6%.
-
ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving
ProofWala is a multilingual proof-engineering framework that demonstrates cross-lingual transfer between Lean 4 and Coq for neural theorem proving.
-
Names Don't Matter: Symbol-Invariant Transformer for Open-Vocabulary Learning
A shared-parameter per-symbol stream design makes Transformers exactly invariant to symbol renaming and lets them handle unseen symbols at test time, with large gains on propositional-logic generalization and small on...
-
Solving Formal Math Problems by Decomposition and Iterative Reflection
An agent that decomposes Lean 4 goals into subproblems and iteratively repairs proofs achieves a 95.9% pass rate on miniF2F-test using a stock Gemini model.
-
Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving
Bourbaki (7B), an MCTS-based system with self-generated subgoal rewards, solves 26/658 PutnamBench problems, beating the prior 7B best of 23 at a larger sample budget.
-
Clarifying Before Reasoning: A Coq Prover with Structural Context
Enriching LLM theorem-proving prompts with Coq's internal type representations and natural-language explanations raises proof success from 21.8% to 45.8%, surpassing Graph2Tac's 33.2%.
-
Towards Scientific Discovery with Generative AI: Progress, Opportunities, and Challenges
A position paper proposing a research agenda for AI-driven scientific discovery, centered on benchmarks, science agents, multimodal representations, and unified reasoning.
Discussion (0). Continue with ORCID to comment.