论文页面 - FVSpec：作为Lean挑战的真实世界基于属性的测试

来源：https://huggingface.co/papers/2606.01008

摘要

本文提出了一个用于AI辅助形式化验证的基准，涉及使用多智能体LLM流水线将基于属性的测试从Python转换为Lean规范。

我们提出了一个基准，用于评估AI模型和智能体在真实世界软件形式化验证任务上的表现。我们首先从真实世界的Python仓库中抓取11,039个基于属性的测试（PBT），然后自动将其中2,772个（25%）转换为9,415个Lean 4规范，并包含sorry占位符（每个PBT约3个形式化版本；当没有单一版本在质量指标上占优时，我们保留多次尝试）。将PBT转换为Lean规范具有挑战性：需要在Lean中对Python语义进行建模，推断命令式PBT中编码的逻辑属性，并处理在一种不常用语言中进行依赖类型编程的固有困难。我们描述了一个三智能体LLM流水线，用于将PBT转译成Lean规范，评估了覆盖率和质量指标，并为使用多种自动化和基于模型的方法进行证明生成提供了基线。所有代码（爬取器和智能体）和数据（PBT和Lean规范）均为开源。我们的基准旨在推动AI辅助真实世界软件形式化验证这一尚未充分探索的问题取得进展，随着AI生成越来越多的代码，这一领域正日益受到关注。

查看arXiv页面 (https://arxiv.org/abs/2606.01008)查看PDF (https://arxiv.org/pdf/2606.01008)项目页面 (https://fvspec.galois.com/)添加到收藏 (https://huggingface.co/login?next=%2Fpapers%2F2606.01008)

在您的智能体中获取此论文：

hf papers read 2606.01008

没有最新的CLI？curl -LsSf https://hf.co/cli/install.sh | bash

引用此论文的模型0

没有模型链接此论文

请在模型README.md中引用arxiv.org/abs/2606.01008以从此页面链接。

引用此论文的数据集2

GaloisInc/fvspec-pbt 查看器• 更新于约1小时前 • 21.7k • 59 (https://huggingface.co/datasets/GaloisInc/fvspec-pbt)

GaloisInc/fvspec-fv 查看器• 更新于约1小时前 • 9.42k • 55 (https://huggingface.co/datasets/GaloisInc/fvspec-fv)

引用此论文的Space0

没有Space链接此论文

请在Space README.md中引用arxiv.org/abs/2606.01008以从此页面链接。

包含此论文的收藏0

没有收藏包含此论文

请将此论文添加到收藏 (https://huggingface.co/new-collection)中以从此页面链接。