LLM 能根据任务描述生成 Lean 规范，但这些描述往往不完整或含糊，可能遗漏 verifier 关注的边界情况，导致形式化规格不完备。
本文探讨一种引导式澄清代理（Elicitation Agent，EA）是否能够通过向参考开发者提出澄清问题，提升 verifier 检查后的 Lean 规范质量。
EA 的工作流程包括：将任务拆解为子任务，标记尚未决定的要点，限制提问次数（k=3 或 k=10），收集答案后撰写更精炼的自然语言规格，随后交给 LLM 正式化器转化为 Lean 代码。
实验在 189 条 Verina Lean 4 规格生成任务上进行，比较单轮生成与有澄清的两种提问预算。使用同模型 Claude Sonnet 4.6 管线以及跨模型 Claude → GPT‑5.6、Claude → Gemini 3.8 Flash 管线。评估指标包括严格的 pass@1、编译条件通过率（compile‑conditional）以及任务层面的 treatment 通过率。
结果显示，同模型管线在两种预算下的 strict pass@1 为负，说明澄清并非普适的准确性提升手段。跨模型管线则表现为正向提升，最高达到 65.6%（提升 6.3 点），在 Claude → GPT‑5.6、k=10 时从 42.0% 提升至 50.6%。六个条件的 compile‑conditional 为正，最大跨模型差值为 4.9 点。错误分析表明，后置条件是导致规格退化的主要因素。
这些发现表明，未来的自动形式化系统应将澄清后的自然语言规格视为中间产物，联合优化编译通过率以及将澄清信息可靠翻译为 Lean 的语义正确性。
点评