Quarry：基于难度感知的分解策略实现Rocq自动定理证明

本文介绍Quarry框架，旨在解决形式化验证中交互式定理证明器（如Rocq）的自动化瓶颈。该框架通过分离证明规划与执行，结合大语言模型（LLM）的高层次规划能力和自动化证明工具（如CoqHammer）的局部严谨推理能力，显著提升了Rocq的自动证明成功率。核心创新包括基于难度感知的分解策略，优先处理易解决的子目标，有效分配计算资源。

形式化验证是确保软件正确性的关键手段，但构建机器可检查的证明仍需大量人工。现有自动化方案各有局限：启发式策略（如Coq的auto）能力有限；Hammer工具（如CoqHammer）缺乏长程规划；LLM方法虽能提出高层思路，但局部严谨性不足。如何结合两者优势是领域开放问题。

Quarry核心是规划与执行分离：1.规划阶段：LLM提出目标分解方案（子引理+策略）；2.验证阶段：Rocq类型检查分解正确性，并用难度模型评估子目标的Hammer可解性；3.执行阶段：按难度排序递归证明子引理，控制计算预算。技术实现上集成SerAPI（与Rocq交互）、CoqHammer（自动证明引擎）及基于证明状态特征的难度预测模型。

在Rocq基准测试中，Quarry在10分钟预算下比最强基线成功率提升7%-13%；相比纯LLM方法，成本更可预测；且能适配开源/商业LLM，通用性强。

技术贡献包括神经符号协作新范式（LLM与符号系统各司其职）、难度感知资源分配、渐进式验证策略。应用前景涵盖关键软件验证（减少人工）、数学形式化（辅助定理转化）、教育工具（帮助学生理解证明）。

局限性：分解质量依赖LLM、难度模型泛化不足、复杂证明递归深度大。未来方向：更强规划模型、难度模型在线学习、交互式助手、跨证明器（如Isabelle）移植。