摘要
针对 AI 编程代理输出正确性难以保证的问题，本文研究规范自动形式化，即利用 LLM 代理将非正式编程问题转化为忠实的形式化规范。作者提出了 Verus-SpecBench 基准测试及 Verus-SpecGym 代理环境。为解决评估难题，通过扩展执行机制并利用对抗性测试用例进行验证。实验表明，前沿模型虽能解决部分任务，但在输入假设省略等方面仍显脆弱，且传统 LLM 评判方法漏检率高。
AI 推荐理由
研究 Agent 将非正式问题转化为形式化规范的逻辑推理与语义对齐能力，属高阶推理任务。
研究机构
CMU
Amazon
论文信息