Clarifying Before Reasoning: A Coq Prover with Structural Context

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%~$\to$~82.3%). Using the general-purpose model $\mathtt{\text{DeepSeek-V3}}$, our approach leads to a 2.1$\times$ improvement in proof success (21.8%~$\to$~45.8%) and outperforms the previous state-of-the-art $\mathtt{\text{Graph2Tac}}$ (33.2%). We evaluate this on 1,386 theorems randomly sampled from 15 standard Coq packages, following the same evaluation protocol as $\mathtt{\text{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.