一句话：将 AND–OR 图视为证明系统的部分表示，把失败证明搜索的调试转化为修改证明系统，并统一 why-not 策略。
证明搜索支撑类型系统、定理证明器策略与 Datalog 程序分析等工具，但失败证明搜索的内部 AND–OR 图庞大，调试困难。本文提出新框架：将 AND–OR 图视为底层证明系统的部分表示，把调试转化为对证明系统施加修改，并让工具持续征求修改，直至系统证明原目标；该框架统一了既有 why-not 策略并支持新策略。作者在 284 个 AND–OR 图上评估：强制 Strong Soundness 相比不可靠基线减少决策数 1.4–3.2 倍；新性质 Strong Completeness Modulo Observability 支持剪枝，再减少 1.0–2.8 倍，总体减少 2.0–3.8 倍。
Proof search powers our most advanced programming tools, from type systems, to search tactics for interactive theorem provers, to Datalog-backed program analyses. Although proof search tooling is powerful and now pervasive, debugging it is hard, even for experts. When proof search cannot prove the goal, the programmer’s best source of information is a massive AND–OR graph representing the tool’s internal state during the proof search process. The difficulty of understanding and debugging this vast trace of internal state locks programmers out of exactly the high-assurance automated reasoning tools we want them to adopt. We propose a new formulation of proof search debugging, which: (i) views AND–OR graphs as a partial representations of the underlying proof system, (ii) treats debugging as a process of applying modifications to this proof system, and (iii) uses a debugging tool to solicit these modifications until the resulting proof system proves the original goal. This approach unifies decades of ad-hoc strategies in a single general-purpose framework and is applicable to the diverse range of programming tools that use proof search. Our framework can express existing “why-not” debugging strategies as well as new strategies, and we evaluate such strategies on 284 AND–OR graphs. We find that a strategy that enforces a property called Strong Soundness reduces the number of decisions by 1.4×–3.2× compared to an unsound baseline, and a new property we call Strong Completeness Modulo Observability enables pruning to further reduce decisions by 1.0×–2.8× for an overall reduction of 2.0×–3.8×.
@article{paperbot3764,
title = {Navigating AND–OR Graph Modifications to Debug Failing Proof Search},
author = {Justin Lubin and Marlena Preigh and Max Willsey and Sarah E. Chasins},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808344}
}