Improved Assistance for Interactive Proof
summary
Classifies learning tasks for ITPs and shows concrete wins: simple premise selection (k‑NN) raises Isabelle hammer success from ~38% to ~47%, graph neural nets and logic‑aware embeddings improve further, and Monte Carlo proof search with reinforcement learning (tactic‑level exploration in TacticToe/Tactician) finds proofs with average branching ≈10 and depths ~300 that other provers miss. Builds guided ATPs (Enigma for E, guided Vampire) and a synthesis/heuristic pipeline (cus + heuristics) that disproves hundreds of hammer problems. Notes LLMs still fail on many basic propositional and proof tasks and are too brittle for direct integration.
AI-written summary · about
chapters (9)
- 0:00Improved proof assistance intro
- 1:33Talk overview
- 5:07Premise selection techniques
- 17:18Guiding proof search
- 26:53Better proof assistant interaction
- 35:52Automated disproof and counterexamples
- 44:27Premise selection advances
- 50:10Direct automation and future work
- 1:02:22Q&A
related talks
21mA Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
01h 02mHow can Machine Learning Help Formal Proving ?
11mAutomated Discovery of Tactic Libraries for Interactive Theorem Proving
26mInteractive Theorem Provers for Proof Education
01h 01mDiscussion
21mTowards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
43mAI Development Lifecycle: Learnings of What Changed with LLMs
15mCurrent Practices for Building LLM-Powered Reasoning Tools Are Ad Hoc—and We Can Do Better