FVSpec: Real-World Property-Based Tests as Lean Challenges
arXiv:2606.01008v3 提出 FVSpec 基准，用于评估 AI 模型在真实世界形式软件验证任务上的表现。研究人员从 Python 仓库中抓取了 11,039 个基于属性的测试（PBTs），并自动将其中的 2,772 个（占 25%）翻译为包含 sorry 占位符的 9,415 个 Lean 4 规范。该过程涉及在 Lean 中建模 Python 语义、推断命令式 PBT 中的逻辑属性以及处理依赖类型编程的固有难度，并描述了一个三智能体 LLM 管道来完成翻译。研究还评估了覆盖率和质量指标，提供了基于多种自动化及模型方法的证明生成基线，且所有代码和数据均已开源。该基准旨在推动 AI 辅助形式化验证这一未充分探索问题的进展。