09:41
官方账号arXiv cs.AI@Quinn Dougherty, Max von Hippel, Hazel Shackleton, Mike Dodds
推荐理由：形式验证是 AI 生成代码质量保障的关键，做 AI 安全或软件验证的开发者可以直接用这个基准测试自己的模型，看看能否补全 Lean 证明。
属性测试
共 1 条相关 AI 资讯
6月2日
09:41
FVSpec 是一个新基准，用于评估 AI 模型和智能体在真实软件形式验证任务上的能力。研究团队从真实 Python 仓库中抓取 11,039 个属性测试（PBT），并自动将其中 2,772 个（25%）翻译成 9,415 个 Lean 4 规范（含占位符）。翻译过程需模拟 Python 语义、推断逻辑属性并处理依赖类型编程的复杂性。团队设计了一个三智能体 LLM 流水线完成翻译，并提供了多种自动化与基于模型的证明生成基线。所有代码和数据已开源，旨在推动 AI 辅助真实软件形式验证这一未充分探索的领域。