Large language models can turn task descriptions into Lean specifications, but such descriptions are often underspecified or ambiguous, potentially omitting verifier‑relevant edge cases and yielding imperfect formal specs.
This work investigates whether an elicitation agent (EA) that asks clarification questions to a reference‑grounded simulated developer can improve verifier‑checked Lean specifications.
The EA pipeline works as follows: decompose the task, flag unresolved decisions, ask a bounded number of clarification questions (k=3 or k=10), incorporate the answers into a refined natural‑language specification, and finally hand it to an LLM formalizer that translates it into Lean code.
Experiments were conducted on 189 Verina Lean 4 specification‑generation tasks, comparing single‑shot generation with elicitation under the two question budgets. We evaluated a same‑model Claude Sonnet 4.6 pipeline and cross‑model pipelines Claude → GPT‑5.6 and Claude → Gemini 3.8 Flash, using strict pass@1, compile‑conditional, and treatment metrics.
Results show that the same‑model pipeline yields negative strict pass@1 estimates at both budgets, indicating that elicitation is not a universal accuracy booster. In contrast, the cross‑model pipelines achieve positive estimates, with the best strict pass@1 reaching 65.6% (a +6.3‑point gain) in the Claude → GPT‑5.6 configuration. Six of eight conditions have positive compile‑conditional estimates, with a maximum cross‑model improvement of 4.9 points. Failure analysis identifies postconditions as the largest source of degradation.
These findings suggest that future auto‑formalization systems should treat elicited natural‑language specifications as intermediate artifacts and jointly optimize for semantic correctness of compiling outputs and reliable translation of clarified information into Lean.
Review