# Clarifying Before Reasoning: A Coq Prover with Structural Context

arXiv: https://arxiv.org/abs/2507.02541 · HTML: https://mlsanity.com/paper/2507.02541/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 19 of its 39 references that are in the map.
- First posted on arXiv 3 Jul 2025.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)

## Builds on (most cited first, 19 of 19)

- [DeepSeek-V3 Technical Report](https://mlsanity.com/paper/2412.19437/) (2024)
- [Llemma: An Open Language Model For Mathematics](https://mlsanity.com/paper/2310.10631/) (2023)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [Lean-STaR: Learning to Interleave Thinking and Proving](https://mlsanity.com/paper/2407.10040/) (2024)
- [TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts](https://mlsanity.com/paper/2407.03203/) (2024)
- [Magnushammer: A Transformer-Based Approach to Premise Selection](https://mlsanity.com/paper/2303.04488/) (2023)
- [APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning](https://mlsanity.com/paper/2505.05758/) (2025)
- [InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search](https://mlsanity.com/paper/2410.15700/) (2024)
- [LLMSTEP: LLM proofstep suggestions in Lean](https://mlsanity.com/paper/2310.18457/) (2023)
- [MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving](https://mlsanity.com/paper/2503.03205/) (2025)
- [Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification](https://mlsanity.com/paper/2410.19940/) (2024)
- [Succinct Representations for Concepts](https://mlsanity.com/paper/2303.00446/) (2023)
- [Automated Discovery of Tactic Libraries for Interactive Theorem Proving](https://mlsanity.com/paper/2503.24036/) (2025)
- [Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code](https://mlsanity.com/paper/2403.12627/) (2024)

## Built on by (most cited first, 2 of 2)

- [Typed Chain-of-Thought: A Curry-Howard Framework for Verifying LLM Reasoning](https://mlsanity.com/paper/2510.01069/) (2025)
- [ProsaBuddy: Assisting Mechanized Real-Time Schedulability Analysis with LLM-based Agents](https://mlsanity.com/paper/2610.03796/) (2026)

## Abstract (arXiv)

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.