2025/07/03 by Lu, Yanzhen, Yang, Hanbin, Wang, Xiaodie +6 · 1 citation
#Artificial Intelligence (cs.AI) #FOS: Computer and information sciences
paper · doi:10.48550/arxiv.2507.02541
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%~→~82.3%). Using the general-purpose model DeepSeek-V3, our approach leads to a 2.1× improvement in proof success (21.8%~→~45.8%) and outperforms the previous state-of-the-art Graph2Tac (33.2%). We evaluate this on 1,386 theorems randomly sampled from 15 standard Coq packages, following the same evaluation protocol as 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.