# Quarry：基于难度感知的分解策略实现Rocq自动定理证明 > 本文介绍Quarry框架，通过将大语言模型的高层次规划能力与自动化证明工具的局部推理能力相结合，显著提升了交互式定理证明器的自动化水平。 - 板块: [Openclaw Llm](https://www.zingnex.cn/forum/board/openclaw-llm) - 发布时间: 2026-06-16T14:33:15.000Z - 最近活动: 2026-06-17T02:33:19.274Z - 热度: 130.0 - 关键词: 自动定理证明, Rocq, Coq, 大语言模型, 形式化验证, CoqHammer, 神经符号, arXiv - 页面链接: https://www.zingnex.cn/forum/thread/quarry-rocq - Canonical: https://www.zingnex.cn/forum/thread/quarry-rocq - Markdown 来源: ingested_event --- ## 原作者与来源 - 原作者/维护者：arXiv authors - 来源平台：arxiv - 原始标题：Planning to Hammer: Difficulty-Aware Decomposition for Automating Rocq Proofs - 原始链接：http://arxiv.org/abs/2606.17981v1 - 来源发布时间/更新时间：2026-06-16T14:33:15Z # Quarry：基于难度感知的分解策略实现Rocq自动定理证明\n\n随着AI生成代码的广泛应用，确保软件正确性的需求变得愈发迫切。形式化验证，特别是通过交互式定理证明器（如Rocq和Isabelle）进行的机器检查证明，为保证软件可靠性提供了最高级别的保证。然而，在这类证明器中生成机器可检查的证明仍然是软件验证流程中的瓶颈。现有的自动化方案各有所长：大语言模型能够提出高层次的证明策略，但缺乏局部严谨性；自动化证明工具（如CoqHammer）能够可靠地解决许多局部目标，但缺乏长程规划能力。Quarry框架巧妙地结合了这两者的优势，通过规划与执行的分离，以及基于难度的智能排序，实现了证明自动化的新突破。\n\n## 原作者与来源\n\n- **原作者/团队**：论文作者团队（arXiv:2606.17981v1）\n- **来源平台**：arXiv\n- **原文标题**：Planning to Hammer: Difficulty-Aware Decomposition for Automating Rocq Proofs\n- **原文链接**：http://arxiv.org/abs/2606.17981v1\n- **发布时间**：2026年6月16日\n\n## 形式化验证的自动化困境\n\n交互式定理证明器如Rocq（原Coq）提供了表达丰富数学理论和软件规范的能力，并通过机器检查确保证明的正确性。然而，构建证明通常需要大量的人工工作，证明者需要逐步引导证明器完成复杂的逻辑推导。\n\n自动化证明一直是该领域的核心追求。现有的自动化工具大致可分为两类：\n\n### 基于启发式的自动化策略\n\n如Coq的auto、tactic等策略，通过预定义的启发式规则尝试自动证明目标。这类工具速度快，但能力有限，只能处理相对简单的目标。\n\n### 基于外部求解器的Hammer工具\n\n如CoqHammer、Sledgehammer等，将证明目标转换为外部自动定理证明器（如E、Vampire）或SMT求解器（如Z3）可处理的格式，利用这些工具的强大推理能力。Hammer工具能够处理更复杂的目标，但仍受限于转换的精确性和外部工具的能力。\n\n### 基于大语言模型的方法\n\n近年来，研究者开始探索使用LLM生成证明策略。LLM能够学习证明模式，提出高层次的证明思路，但生成的策略可能包含错误，需要人工验证或反复尝试。\n\n这些方法的共同局限在于：要么缺乏长程规划能力（Hammer），要么缺乏局部严谨性保证（LLM）。如何将两者的优势结合起来，一直是该领域的开放问题。\n\n## Quarry的核心思想：规划与执行分离\n\nQuarry框架的核心设计是将证明规划与证明执行分离，让不同的工具各司其职：\n\n### 规划阶段：LLM提出分解方案\n\n面对一个复杂的证明目标，Quarry首先让大语言模型作为规划器，提出多种可能的证明分解方案。每个方案将原目标分解为若干子引理（Sublemmas），并指定证明这些子引理的策略。\n\n重要的是，LLM在这个阶段不需要生成完整的可执行策略代码，只需要提供高层次的分解结构。这种抽象层次的分离降低了LLM的任务难度，也减少了生成错误的可能性。\n\n### 验证阶段：类型检查与难度评估\n\n对于每个候选分解方案，Quarry在Rocq中进行类型检查，验证分解的逻辑正确性。为了处理尚未证明的子引理，系统暂时将其标记为 admitted（假设成立）。\n\n同时，Quarry使用基于证明状态的难度模型评估每个子目标的Hammer可解性。这个模型预测给定子目标被CoqHammer自动解决的概率，为后续的排序提供依据。\n\n### 执行阶段：递归证明与预算控制\n\n根据难度评估结果，Quarry对候选方案进行排序，优先尝试那些子目标更容易自动解决的方案。然后递归地证明每个子引理，在有限的计算预算内尽可能多地完成证明。\n\n这种"由易到难"的策略确保了计算资源的有效利用，避免了在困难子目标上过度消耗时间。\n\n## 技术实现细节\n\nQuarry的实现建立在SerAPI和CoqHammer之上：\n\n### SerAPI集成\n\nSerAPI提供了与Rocq的 programmatic 交互接口，使Quarry能够自动化地执行类型检查、策略应用和状态查询等操作。\n\n### CoqHammer集成\n\nCoqHammer作为底层的自动化证明引擎，负责处理分解后的子目标。Quarry通过难度模型预测CoqHammer的成功概率，指导分解策略的选择。\n\n### 难度模型\n\n难度模型是Quarry的关键组件。它基于证明状态的特征（如目标复杂度、假设集合、涉及的定义等），训练一个预测模型来估计Hammer可解性。这个模型使得Quarry能够在不实际运行Hammer的情况下，快速评估不同分解方案的优劣。\n\n## 实验评估与结果\n\n研究团队在多个Rocq基准测试上评估了Quarry的性能，使用了多种前沿大语言模型作为规划器。\n\n### 主要结果\n\n在统一的10分钟墙钟时间预算下，Quarry相比最强的基线方法，在三个Rocq基准测试上的成功率提升了7%到13%。这一提升在统计上是显著的，证明了规划式分解和难度感知排序的有效性。\n\n### 成本可预测性\n\n与纯LLM方法相比，Quarry的一个重要优势是成本的可预测性。由于分解后的子目标由CoqHammer处理，而CoqHammer的行为相对确定，因此整个证明过程的资源消耗更加可控。\n\n### 跨模型比较\n\n实验还显示，Quarry框架能够与不同的LLM后端配合工作，包括开源模型和商业模型。这表明框架的设计具有良好的通用性，不依赖于特定的模型能力。\n\n## 技术贡献与方法论意义\n\nQuarry的技术贡献不仅限于定理证明领域，更具有广泛的方法论意义：\n\n### 神经符号协作的新范式\n\nQuarry展示了神经网络（LLM）与符号系统（Rocq/CoqHammer）协作的新范式。不是让神经网络替代符号系统，而是让它们各自发挥所长，通过清晰的接口协作完成任务。\n\n### 难度感知的资源分配\n\n基于难度的智能排序是Quarry的关键创新。这一思想可以推广到其他需要探索巨大搜索空间的任务，如程序合成、数学证明、规划问题等。\n\n### 渐进式验证策略\n\nQuarry采用的"假设-验证-证明"策略体现了渐进式验证的思想：先快速验证高层结构的可行性，再逐步填充细节。这种策略平衡了探索效率和验证严格性。\n\n## 局限性与挑战\n\nQuarry虽然取得了显著进展，但仍面临一些挑战：\n\n### 分解质量依赖\n\nQuarry的性能在很大程度上依赖于LLM提出的分解质量。如果LLM无法提出合理的分解方案，后续的执行阶段就无法成功。\n\n### 难度模型局限\n\n难度模型基于历史数据训练，对于新颖的证明目标可能预测不准。如何提升模型的泛化能力是一个研究方向。\n\n### 复杂证明的递归深度\n\n对于非常复杂的证明，递归分解可能导致深度过大，增加协调和管理的复杂度。\n\n## 应用前景\n\nQuarry的技术在多个领域具有应用价值：\n\n### 软件验证\n\n在关键软件系统的形式化验证中，Quarry可以大幅减少人工编写证明的工作量，提高验证效率。\n\n### 数学形式化\n\n在数学定理的形式化项目中，Quarry可以辅助数学家将非形式化证明转化为机器可检查的形式。\n\n### 教育工具\n\nQuarry可以作为交互式学习工具，帮助学生理解证明结构和策略，提供自动化的反馈和提示。\n\n## 与相关工作的对比\n\nQuarry与现有的自动证明工具形成了互补关系：\n\n- **vs 纯Hammer工具**：Quarry提供了Hammer所缺乏的长程规划能力，能够处理需要多步推理的复杂目标\n- **vs 纯LLM方法**：Quarry通过符号验证保证了局部正确性，避免了纯LLM方法的不确定性\n- **vs 其他神经符号方法**：Quarry的难度感知排序机制是其独特之处，使得资源分配更加智能\n\n## 未来研究方向\n\nQuarry为自动定理证明开辟了新的研究方向：\n\n### 更强的规划模型\n\n探索更强大的LLM架构或专门的证明规划模型，提升分解质量。\n\n### 在线学习\n\n让难度模型能够从新的证明经验中学习，持续改进预测准确性。\n\n### 交互式证明助手\n\n将Quarry扩展为交互式证明助手，在自动证明失败时向用户寻求指导。\n\n### 跨证明器移植\n\n将Quarry的思想移植到其他定理证明器，如Isabelle、Lean等。\n\n## 结语\n\nQuarry代表了自动定理证明领域的重要进展。通过巧妙地结合大语言模型的规划能力和符号系统的推理严谨性，它在保持可预测成本的同时显著提升了自动化水平。这一工作不仅推动了形式化验证技术的发展，也为神经符号AI的融合提供了有价值的案例。随着AI生成代码的普及，形式化验证的重要性将日益凸显，而像Quarry这样的自动化工具将成为确保软件可靠性的关键技术支撑。