构建真实软件验证的测试基准，用大模型自动转译Python测试为形式化规范。
FVSpec: Real-World Property-Based Tests as Lean Challenges
- 三阶段LLM流水线将Python属性测试转为Lean 4形式化规范。
- 从1.1万份测试中生成9415条规范，平均每条测试对应3个形式化版本。
- 开源数据与代码，助力AI辅助形式化验证研究。
我们提出一个用于评估人工智能模型和智能体在真实世界形式化软件验证任务上的基准。首先从真实世界的Python仓库中爬取11,039个属性测试（PBTs），然后将其中2,772个（占25%）自动转换为9,415条包含sorry占位符的Lean 4规范（平均每条测试对应约3个形式化版本；当多个尝试无明显优劣时全部保留）。将PBT转为Lean规范极具挑战：需在Lean中建模Python语义、推断指令式测试中的逻辑性质，并应对依赖类型编程在冷门语言中的复杂性。我们设计了一个三代理LLM流水线完成转译，评估了覆盖度与质量指标，并为证明生成提供了多种自动化与基于模型的基线方法。所有代码（爬虫与代理）及数据（PBTs与Lean规范）均开源。该基准旨在推动对人工智能辅助真实软件形式化验证这一尚未充分探索问题的研究进展，而此问题随着人工智能编写越来越多代码正日益重要。
原文摘要 · Abstract (English)
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 translate 2,772 of them (25%) into 9,415 Lean 4 specifications with sorry placeholders (about 3 formalizations/PBT; we retain multiple attempts when none dominates on quality metrics). Translating PBTs into Lean specifications is challenging: it requires modeling Python semantics in Lean, inferring the logical property encoded in an imperative PBT, and handling the inherent difficulties of dependently-typed programming in a seldom-used language. We describe a three-agent LLM pipeline for transpiling PBTs into Lean specifications, evaluate coverage and quality metrics, and provide baselines for proof generation using several automated and model based approaches. All code (scraper and agents) and data (PBTs and Lean specifications) are open source. Our benchmark aims to drive progress on the underexplored problem of AI-assisted formal verification of real-world software, which is of increasing interest as AI produces more and more of the world's code.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。