规划锤击：用于自动化 Rocq 证明的难度感知分解

随着人工智能生成的代码激增，形式验证，尤其是通过 Rocq 和 Isabelle 等交互式定理证明者进行的形式验证，对于确保软件的正确性变得越来越重要。然而，在此类证明器中生成机器检查的证明仍然是一个瓶颈。现有的解决方案为证明自动化带来了互补的优势：大语言模型 (LLM) 可以提出高级证明策略，但缺乏局部严谨性，而 CoqHammer 等自动化策略可以可靠地实现许多局部目标，但缺乏长期规划能力。为了结合两个领域的优点，我们推出了 Quarry，一个基于规划的证明综合框架，它将证明规划与证明执行分开。具体来说，Quarry 要求 LLM 主动提出具有任意子引理的多重证明分解，在 Rocq 中在临时承认的子引理下对它们进行类型检查，并使用基于证明状态的难度模型来估计锤子可解性，对候选者进行排名。然后，它在有限的预算内递归地证明次引理，有效地将长证明转化为锤子可解决的义务序列。我们在 SerAPI 和 CoqHammer 之上实现 Quarry，并使用跨多个基准的多个前沿 LLM 对其进行评估。实验结果表明，基于规划的分解和可解性感知排序极大地提高了自动化程度，同时保持了可预测的成本。在统一的 10 分钟挂钟预算下，Quarry 在三个 Rocq 基准测试中的成功率比最强基线提高了 7% 到 13%。这些结果表明，通过协调神经规划与符号执行而不是取代其中任何一个，可以实现可靠的证明自动化。