How can Machine Learning Help Formal Proving ?
summary
Reviews recent progress using Lean mathlib (~300k theorems) and pre‑trained LMs fine‑tuned for proving, combines reinforcement learning (AlphaZero‑style) with a two‑model loop (policy + difficulty) trained on as few as 240 RL examples, and adds proof generation (K proofs + RL) and sketcher+prover pipelines. Results: undergraduate to Olympiad‑level solving, IMO silver then gold‑level benchmarks, an arXiv lemma benchmark with ~7% verified successes, autoformalization reaching ~4% of arXiv lemmas and a full formalization (Strong PNT) producing ~25k lines in three weeks, and software‑verification gains from 8.5% to >30% on CLEVER.
AI-written summary · about
chapters (18)
- 0:00Introduction
- 1:24AI proving mathematical theorems
- 5:18Language models for theorem proving
- 13:40Data scarcity in formal languages
- 20:42Reinforcement learning in proving
- 28:10Whole proof generation models
- 34:07AI math: still need formal languages?
- 38:21AI proving for software verification
- 41:47Future of AI in mathematics
- 42:29Q&A: Mathematicians' focus
- 45:20Q&A: Proof assistant design
- 47:52Q&A: Data for informal vs formal math
- 49:10Q&A: Language models with SMT solvers
- 51:19Q&A: ML improving SMT solvers
- 54:12Q&A: Verifiable informal proofs
- 55:57Q&A: AI in math games
- 57:43Q&A: Impact on PhD workflows
- 59:54Q&A: AI-assisted proving workflows
related talks
01h 03mImproved Assistance for Interactive Proof
21mA Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
16mLemur: Integrating Large Language Models in Automated Program Verification
19mRL for Autonomous Coding
19mAutomated Program Refinement: Guide and Verify Code Large Language Model with(…)
22mTowards Verified Code Reasoning by LLMs
43mFrom Lambda to LLMs: AI Coding and the Future of Programming
53mSemantics-based program manipulation in the age of LLMs