**FVSpec：真实世界性质测试驱动的 Lean 形式验证基准**

_FVSpec: Real-World Property-Based Tests as Lean Challenges_

> 该工作从 Python 仓库抓取 11,039 个基于性质的测试，自动翻译其中 2,772 个为 9,415 个 Lean 4 规范占位证明，提出三智能体 LLM 流水线完成转换，并构建基准以推动 AI 辅助的真实软件形式验证研究。

**来源信息**
- **来源**：HuggingFace Daily Papers（社区热门论文）
- **分类**：论文
- **发布时间**：2026-06-15 08:00（北京时间）
- **原文**：[打开原文](https://huggingface.co/papers/2606.01008)