Reproduce “Proof Artifact Co-training for Theorem Proving with Language Models” on OpenResearch

About this paper

Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, Stanislas Polu

This research introduces Proof Artifact Co-Training (PACT), a method for automated theorem proving that extracts self-supervised training data from low-level proof terms within the Lean theorem prover. PACT-trained language models achieve a 48.4% theorem proving success rate on a held-out test set, an increase from 32.2% for models without PACT, and demonstrate generalization to new mathematical content.

Key insights

• Leveraging low-level, kernel-level proof terms provides a rich source of implicit structural information that can be systematically converted into effective self-supervised training tasks, mitigating data scarcity.
• Co-training with PACT tasks alongside the primary tactic prediction objective acts as a powerful regularizer, preventing rapid overfitting and significantly improving the generalization capabilities of neural theorem provers.
• The benefits of PACT are complementary to general mathematical pre-training (like WebMath) and scale with model size, indicating that comprehensive data strategies are most effective for robust theorem proving.

Summary by alphaXiv.