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× improvement in clarity score (44.5%~rightarrow~82.3%). Using the general-purpose model textttDeepSeek-V3, our approach leads to a 2.1× improvement in proof success (21.8%~rightarrow~45.8%) and outperforms the previous state-of-the-art textttGraph2Tac (33.2%). We evaluate this on 1,386 theorems randomly sampled from 15 standard Coq packages, following the same evaluation protocol as textttGraph2Tac. 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.