Clarifying Before Reasoning: A Coq Prover with Structural Context

📄 arXiv: 2507.02541v1 📥 PDF

作者: Yanzhen Lu, Hanbin Yang, Xiaodie Wang, Ge Zhang, Biao Li, Chenxu Fu, Chao Li, Yang Yuan, Andrew Chi-Chih Yao

分类: cs.AI

发布日期: 2025-07-03

💡 一句话要点

提出基于结构化上下文的Coq定理证明器，显著提升LLM推理能力

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 定理证明 Coq 大型语言模型 结构化上下文 任务清晰度 Planner-Executor架构 形式化方法

📋 核心要点

  1. 现有LLM在Coq定理证明中面临挑战，任务理解不足导致推理能力受限。
  2. 通过引入结构化语义上下文，提升任务清晰度，从而增强LLM的推理能力。
  3. 实验表明，该方法显著提升了Coq定理证明的成功率，优于现有SOTA方法。

📝 摘要（中文）

本文研究了提升任务清晰度是否能增强大型语言模型的推理能力，重点关注Coq中的定理证明。我们引入了一个概念层面的指标来评估任务清晰度，并表明向现代LLM使用的标准输入添加结构化语义上下文，可以使清晰度得分提高1.85倍（44.5％〜82.3％）。使用通用模型DeepSeek-V3，我们的方法使证明成功率提高了2.1倍（21.8％〜45.8％），并且优于先前的最先进水平Graph2Tac（33.2％）。我们在从15个标准Coq软件包中随机抽取的1,386个定理上进行了评估，遵循与Graph2Tac相同的评估协议。此外，在我们的结构化数据上微调较小的模型可以实现更高的性能（48.6％）。我们的方法使用选择性的概念展开来丰富任务描述，并采用Planner-Executor架构。这些发现突出了结构化任务表示在弥合理解和推理之间差距的价值。

🔬 方法详解

问题定义：现有大型语言模型在Coq定理证明任务中表现不佳，主要痛点在于模型难以充分理解定理证明的任务，缺乏对Coq语言和相关概念的深入理解，导致推理过程困难，证明成功率较低。

核心思路：论文的核心思路是通过提升任务的清晰度来增强LLM的推理能力。具体而言，通过向LLM提供结构化的语义上下文，使其能够更好地理解定理证明的目标和相关概念，从而提高证明的成功率。这种结构化上下文包括选择性地展开相关概念，提供更丰富的任务描述。

技术框架：论文采用Planner-Executor架构。Planner负责分析当前证明目标，并选择性地展开相关的概念，生成包含结构化语义上下文的任务描述。Executor则利用LLM，基于Planner提供的任务描述进行推理，生成Coq证明代码。整个流程旨在将复杂的证明任务分解为更易于理解和执行的子任务。

关键创新：论文的关键创新在于引入了结构化语义上下文的概念，并通过选择性概念展开来丰富任务描述。与以往直接将原始Coq代码输入LLM的方法不同，该方法更加注重任务的清晰度和可理解性，从而显著提升了LLM的推理能力。此外，论文还提出了一个概念层面的指标来评估任务清晰度。

关键设计：论文的关键设计包括：1) 选择性概念展开策略，用于确定哪些概念需要展开以提供更清晰的上下文；2) Planner-Executor架构，将任务分解为规划和执行两个阶段；3) 概念层面清晰度评估指标，用于衡量结构化上下文的有效性。具体参数设置和网络结构等细节未在摘要中详细说明。

📊 实验亮点

实验结果表明，该方法在Coq定理证明任务中取得了显著的性能提升。使用DeepSeek-V3模型，证明成功率从21.8%提高到45.8%，提升了2.1倍，超过了之前的SOTA方法Graph2Tac（33.2%）。通过在结构化数据上微调较小的模型，甚至可以达到更高的性能（48.6%）。清晰度得分也从44.5%提升到82.3%，提升了1.85倍。

🎯 应用场景

该研究成果可应用于自动化定理证明、程序验证、形式化方法等领域。通过提升LLM在形式化推理任务中的能力，可以降低人工参与的需求，提高软件开发的可靠性和安全性。未来，该方法有望推广到其他需要复杂推理的任务中，例如代码生成、知识图谱推理等。

📄 摘要（原文）

In this work, we investigate whether improving task clarity can enhance reasoning ability of large language models, focusing on theorem proving in Coq. We introduce a concept-level metric to evaluate task clarity and show that adding structured semantic context to the standard input used by modern LLMs, leads to a 1.85$\times$ improvement in clarity score (44.5\%~$\rightarrow$~82.3\%). Using the general-purpose model \texttt{DeepSeek-V3}, our approach leads to a 2.1$\times$ improvement in proof success (21.8\%~$\rightarrow$~45.8\%) and outperforms the previous state-of-the-art \texttt{Graph2Tac} (33.2\%). We evaluate this on 1,386 theorems randomly sampled from 15 standard Coq packages, following the same evaluation protocol as \texttt{Graph2Tac}. Furthermore, fine-tuning smaller models on our structured data can achieve even higher performance (48.6\%). Our method uses selective concept unfolding to enrich task descriptions, and employs a Planner--Executor architecture. These findings highlight the value of structured task representations in bridging the gap between understanding and reasoning.