Eliciting Specifications: When Does Interactive Clarification Help?

LLMs can generate Lean specifications from task descriptions, but those descriptions are often underspecified or ambiguous and may omit verifier-relevant edge cases, leading to imperfect formal specifications. We study whether an elicitation agent (EA) can improve verifier-checked Lean specifications by seeking clarification from a reference-grounded simulated developer before formalization. The agent decomposes the task, identifies unresolved decisions, asks bounded clarification questions, and uses the answers to write a refined natural-language specification that an LLM formalizer then translates into Lean. On 189 Verina Lean 4 specification-generation tasks [Ye et al., 2025], we compare single-shot Lean specification generation with elicitation under question budgets of k = 3 and k = 10, allowing at most three or ten EA questions per task, across same-model and cross model configurations. The same-model Claude Sonnet 4.6 pipeline has negative strict pass@1 point estimates at both budgets, showing that elicitation is not a uniform accuracy booster. In contrast, the complete Sonnet 4.6-to-GPT-5.6 and Sonnet 4.6-to-Gemini 3.8 Flash pipeline configurations have positive strict point estimates. The largest configuration-level strict result reaches 65.6%, a +6.3-point change (+12 tasks), in the Sonnet 4.6-to-GPT-5.6 pipeline. Six of eight conditions have positive compile-conditional point estimates, with a maximum cross model difference of +4.9 percentage points among compiling outputs. Treatment point estimates also differ across the basic and advanced benchmark splits; the largest advanced-task change occurs in the Sonnet 4.6-to-GPT-5.6 configuration at k = 10, from 42.0% to 50.6%. Failure analysis identifies postconditions as the component with the largest degradations. Together, these findings suggest that future autoformalization systems should treat elicited natural-language specifications as intermediate artifacts and optimize jointly for semantic correctness among compiling outputs and reliable translation of clarified information into Lean.