Navigating AND–OR Graph Modifications to Debug Failing Proof Search
summary
Provides a concrete debugging method that navigates modifications to AND–OR graphs rather than the raw graph, implemented by compiling modification constraints into a SAT check (a non-MP completion oracle via compilation to SAT). Step providers include top-down, random, an informed cut step provider, and information‑gain variants; evaluated on 284 AND–OR graphs from Rust trait errors and ESOP/lean proof searches. Enforcing Strong Soundness cuts decisions by 1.4×–3.2×; adding Strong Completeness Modulo Observability pruning yields a total 2.0×–3.8× reduction.
AI-written summary · about
chapters (13)
- 0:00Debugging failing proof search
- 1:05Proof search failures hard to debug
- 2:08AND-OR graphs in proof search
- 4:12Key insight: graph modifications
- 5:16Interactive refinement in Lean
- 7:41Programming by navigation for debugging
- 10:12Implementing step providers
- 13:00Non-topological step provider strategies
- 15:30Additional step provider techniques
- 15:51Collaborators and closing
- 16:11Q&A: first-order logic
- 16:53Q&A: step provider workloads
- 18:16Final acknowledgments
related talks
21mVerifying term graph optimizations using Isabelle/HOL
22mOptimizing Optimizations: Case Study on Detecting Specific Types of Mathematical(…)
01h 02mLogic, Optimization, and Constraint Programming: A Fruitful Collaboration
21mCut Tracing with E-Graphs for Boolean FHE Circuit Synthesis
37mA Tour of Program Optimization
14mDataflow-Based Pruning for Speeding up Superoptimization
27mAugmenting Rewrite Rule Sets via Knuth-Bendix Completion
14mLOUD: Synthesizing Strongest and Weakest Specifications