一句话：Quarry 将证明规划与执行分离，用 LLM 提出分解并由难度模型排序，递归调用 CoqHammer 提升 Rocq 证明自动化。
交互式定理证明器中的机器检查证明仍是软件形式验证的瓶颈：LLM 能提出高层证明策略但缺乏局部严谨性，CoqHammer 等自动策略能可靠解决局部目标却缺乏长程规划。为此，论文提出 Quarry，一个基于规划的证明合成框架，将证明规划与证明执行分离。Quarry 让 LLM 主动提出多种带任意子引理的证明分解，在 Rocq 中临时 admit 子引理并进行类型检查，再用基于证明状态的难度模型估计各候选的 hammer 可解性并排序；随后在有限预算内递归证明子引理，从而把长证明转化为一系列 hammer 可解的义务。系统实现于 SerAPI 和 CoqHammer 之上，并使用多个前沿 LLM 在多个基准上评估。在统一 10 分钟墙钟预算下，Quarry 在三个 Rocq 基准上比最强基线成功率提升 7–13 个百分点，表明神经规划与符号执行协同可实现可靠且成本可预测的证明自动化。
As AI-generated code proliferates, formal verification—particularly through interactive theorem provers such as Rocq and Isabelle—becomes increasingly important for ensuring software correctness. However, producing machine-checked proofs in such provers remains a bottleneck. Existing solutions bring complementary strengths to proof automation: large language models (LLMs) can propose high-level proof strategies but lack local rigor; automated tactics such as CoqHammer can reliably discharge many local goals, but lack long-range planning capabilities. To combine the best of both worlds, we present Quarry, a planning-based proof synthesis framework that separates proof planning from proof execution. Specifically, Quarry asks an LLM to actively propose multiple proof decompositions with arbitrary sublemmas, type-checks them in Rocq under temporarily admitted sublemmas, and ranks candidates using a proof-state-based difficulty model estimating hammer solvability. It then recursively proves sublemmas within a bounded budget, effectively turning long proofs into sequences of hammer-solvable obligations. We implement Quarry on top of SerAPI and CoqHammer and evaluate it using multiple frontier LLMs across multiple benchmarks. The experimental results show that planning-based decomposition with solvability-aware ranking substantially improves automation while maintaining predictable cost. Under a uniform 10-minute wall-clock budget, Quarry improves over the strongest baseline by 7–13 percentage points in success rate across three Rocq benchmarks. These results demonstrate that reliable proof automation can be achieved by coordinating neural planning with symbolic execution rather than replacing either.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2606-17981,
title = {Planning to Hammer: Difficulty-Aware Decomposition for Automating Rocq Proofs},
author = {Ning Zhang and Nongyu Di and Zenan Li and Yuan Yao and Xiaoxing Ma},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839497}
}