交互式澄清何时有助于 Lean 规格生成？
原标题：Eliciting Specifications: When Does Interactive Clarification Help?
AI 摘要
该研究在 Verina 的 189 个 Lean 4 规格生成任务上，测试了让一个 elicitation agent（EA）在形式化之前向模拟开发者提出澄清问题、再生成精炼自然语言规格的做法是否有效。结果显示，同模型 Claude Sonnet 4.6 流水线在两种提问预算下严格 pass@1 均为负向变化，而 Sonnet 4.6 到 GPT-5.6 的跨模型流水线提升最大，达到 65.6%（+6.3 个百分点，+12 个任务）。作者据此认为，澄清式提问并非普遍提升准确率，未来系统应把 elicited 规格视为中间产物，并同时优化编译输出的语义正确性与澄清信息向 Lean 的可靠转换。
正文节选
Eliciting Specifications: When Does Interactive Clarification Help? Abstract 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 tas