arXiv cs.AI· Mowafak Allaham, Aditya Vempaty, Ashish Jagmohan, Prasenjit Dey, Ravi Kokku·· 11 小时前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 个任务）。
正文 · AI 翻译
摘要：LLM 可以根据任务描述生成 Lean 规范，但这些描述往往不够具体或存在歧义，并且可能遗漏与验证器相关的边界情况，从而产生不完善的形式化规范。我们研究一种引导代理（EA）能否在形式化之前，通过向一个以参考为依据的模拟开发者寻求澄清，来改进经验证器检查的 Lean 规范。该代理会分解任务、识别尚未解决的决策、提出有边界的澄清问题，并利用回答撰写一份经过细化的自然语言规范，随后由 LLM 形式化器将其翻译为 Lean。在 189 个 Verina Lean 4 规范生成任务上，我们在问题预算 k=3 和 k=10（即每个任务最多允许三个或十个 EA 问题）下，比较了单次生成与引导式生成，覆盖同模型和跨模型配置。同模型的 Claude Sonnet 4.6 流水线在两个预算下均得到负的严格 pass@1 估计，表明引导并非普遍提升准确率。相比之下，Sonnet 4.6 到 GPT-5.6 以及 Sonnet 4.6 到 Gemini 3.8 Flash 的流水线得到正的严格估计。最大的严格结果达到 65.6%，即 +6.3 个百分点的变化（+12 个任务），出现在 Sonnet 4.6 到 GPT-5.6 流水线中。八种条件中有六种具有正的编译条件估计，在编译输出中最大跨模型差异为 +4.9 个百分点。处理效应在基础与高级划分之间也存在差异；高级任务的最大变化出现在 k=10 的 Sonnet 4.6 到 GPT-5.6 配置中，从 42.0% 升至 50.6%。失败分析将后置条件确定为最大的退化来源。这些发现表明，未来的自动形式化系统应将引导得到的自然语言规范视为中间产物，并联合优化编译输出中的语义正确性以及将澄清信息可靠地翻译为 Lean。
| 评论： | 已被 NeurIPs 2026 可验证编码 AI 研讨会接收 |
| 主题： | 软件工程（cs.SE）；人工智能（cs.AI）；计算与语言（cs.CL） |
| 引用为： | arXiv:2610.22382 [cs.SE] |
| （或 arXiv:2610.22382v1 [cs.SE] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.22382 由 DataCite 颁发的 arXiv DOI |
提交历史
来自：Mowafak Allaham [查看电子邮件]
[v1]
2026 年 10 月 5 日星期一 16:49:27 UTC（36 KB）
来源：arXiv cs.AI · arxiv.org