Neuro-Symbolic Proof Generation for Scaling Systems Software Verification
Talkat 20th USENIX Symposium on Operating Systems Design and Implementation (OSDI '26) · 2026-07-13..07-15·
summary
Neuro-symbolic proof search implements a best-first tree search that repeatedly queries a fine-tuned LLM for single-step tactics, executes each step in a new Isabelle REPL, repairs broken tactics and premises, prunes states via quickcheck/nitpick and duplicate signatures, and falls back to Sledgehammer; the implemented system proves up to 77.6% of seL4 theorems, solves many multi-step proofs (20%+ success past ten steps), finds 58% of proofs within ten minutes, and generalizes to unseen sessions.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 1:26Interactive theorem proving challenges
- 3:12Language model failures
- 4:35Neuro-symbolic framework core
- 5:19Generating candidate proof steps
- 7:26Proof state management
- 9:15Sledgehammer role
- 10:43Isabelle 4 evaluation
- 12:11Performance comparison
- 13:40Manual effort savings
- 14:46Ablation studies
- 15:52Summary
- 16:36Q&A
related talks
22mTowards Automated Verification of LLM-Synthesized C Programs
38mAutomatically Synthesising Programs that We Can Trust
31mMaking the most of test-time compute in LLMs
01h 22mDebate: Sparks versus embers
19mMiniF2F-Dafny: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification
30mUnfamiliar Terrain
01h 00mAI Safety through Programming?
22mA Certifying Proof Assistant for Synthetic Mathematics in Lean