arXiv cs.AI· Mowafak Allaham, Aditya Vempaty, Ashish Jagmohan, Prasenjit Dey, Ravi Kokku·· 12 小时前AI 评分24
交互式澄清何时能提升 LLM 生成的 Lean 规约？研究揭示同模型与跨模型配置差异
Eliciting Specifications: When Does Interactive Clarification Help?
AI 导读
研究让启发式智能体在形式化前向模拟开发者提问澄清，在 189 个 Verina Lean 4 规约生成任务上对比单次生成与 k=3、k=10 提问预算的效果。同模型 Claude Sonnet 4.6 流程在两种预算下严格 pass@1 估计均为负，而 Sonnet 4.6 到 GPT-5.6 的跨模型流程最高达 65.6%，提升 6.3 个百分点（+12 个任务）。
正文 · 原文
Abstract:LLMs can generate Lean specifications from task descriptions, but those descriptions are often underspecified or ambiguous and may omit verifier-relevant edge cases, yielding 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, we compare single-shot 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 estimates at both budgets, showing elicitation is not a uniform accuracy booster. In contrast, the Sonnet 4.6-to-GPT-5.6 and Sonnet 4.6-to-Gemini 3.8 Flash pipelines have positive strict estimates. The largest 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 estimates, with a maximum cross-model difference of +4.9 points among compiling outputs. Treatment estimates also differ across the basic and advanced 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 largest source of degradation. These findings suggest 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.
| Comments: | Accepted to NeurIPs 2026 Workshop on AI for Verifiable Coding |
| Subjects: | Software Engineering (cs.SE); Artificial Intelligence (cs.AI); Computation and Language (cs.CL) |
| Cite as: | arXiv:2610.22382 [cs.SE] |
| (or arXiv:2610.22382v1 [cs.SE] for this version) | |
| https://doi.org/10.48550/arXiv.2610.22382 arXiv-issued DOI via DataCite |
Submission history
From: Mowafak Allaham [view email]
[v1]
Mon, 5 Oct 2026 16:49:27 UTC (36 KB)
来源：arXiv cs.AI · arxiv.org