通过结构化上下文提升任务清晰度，显著增强大模型的定理证明能力。
Clarifying Before Reasoning: A Coq Prover with Structural Context
- 用概念展开和规划-执行架构，增强输入的结构化语义信息。
- 在1386个定理上，证明成功率从21.8%提升至45.8%，提升2.1倍。
- 适合关注逻辑推理、形式化验证及提示工程优化的研究者。
本文研究提升任务清晰度是否能增强大语言模型的推理能力，聚焦于Coq定理证明。我们引入概念级度量评估任务清晰度，发现添加结构化语义上下文可使清晰度得分从44.5%提升至82.3%，提升1.85倍。基于通用模型DeepSeek-V3，该方法使证明成功率从21.8%提升至45.8%，性能优于先前最优的Graph2Tac（33.2%）。实验在1,386个来自15个标准Coq包的定理上进行，遵循与Graph2Tac一致的评估协议。此外，在结构化数据上微调小型模型可进一步达到48.6%的成功率。方法采用选择性概念展开与规划-执行架构，表明结构化任务表示对弥合理解与推理差距具有关键价值。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。