精选理由
形式验证是 AI 生成代码质量保障的关键，做 AI 安全或软件验证的开发者可以直接用这个基准测试自己的模型，看看能否补全 Lean 证明。
FVSpec 是一个新基准，用于评估 AI 模型和智能体在真实软件形式验证任务上的能力。研究团队从真实 Python 仓库中抓取 11,039 个属性测试（PBT），并自动将其中 2,772 个（25%）翻译成 9,415 个 Lean 4 规范（含占位符）。翻译过程需模拟 Python 语义、推断逻辑属性并处理依赖类型编程的复杂性。团队设计了一个三智能体 LLM 流水线完成翻译，并提供了多种自动化与基于模型的证明生成基线。所有代码和数据已开源，旨在推动 AI 辅助真实软件形式验证这一未充分探索的领域。
AI 翻译 · 中文
FVSpec 是一个新基准，用于评估 AI 模型和智能体在真实软件形式验证任务上的能力。研究团队从真实 Python 仓库中抓取 11,039 个属性测试（PBT），并自动将其中 2,772 个（25%）翻译成 9,415 个 Lean 4 规范（含占位符）。翻译过程需模拟 Python 语义、推断逻辑属性并处理依赖类型编程的复杂性。团队设计了一个三智能体 LLM 流水线完成翻译，并提供了多种自动化与基于模型的证明生成基线。所有代码和数据已开源，旨在推动 AI 辅助真实软件形式验证这一未充分探索的领域。
We present a benchmark for evaluating AI models and agents on real-world formal software verification tasks. We first scrape 11,039 property-based tests (PBTs) from real-world Python repositories, then automatically tran…