FVSpec：现实世界中基于财产的测试是精益的挑战

随着人工智能系统生成的世界代码份额不断增长，形式验证提供了一种原则性的方法来确保代码正确，而人工智能本身可能能够承担大部分验证负担。然而，我们对当今的模型和代理在从现实世界软件中提取的验证任务上的执行情况缺乏清晰的了解，因为现有的基准在很大程度上依赖于策划或综合问题，或者专注于数学而不是程序验证。为了缩小这一差距，我们提出了一个在现实世界的正式软件验证任务上评估人工智能的基准。我们首先从现实世界的 Python 存储库中抓取 7,413 个不同的基于属性的测试 (PBT)，然后自动将其中 2,623 个 (35%) 转换为 9,415 个带有令人遗憾的占位符的精益 4 规范（3.5 形式化/PBT）。将 PBT 转换为精益规范具有挑战性：它需要在精益中对 Python 进行建模、推断 PBT 中编码的属性并处理副作用。我们描述了将 PBT 转化为精益的代理管道，评估覆盖范围和质量指标，并使用多种方法提供证明生成的基线。所有代码（抓取器和代理）和数据（PBT 和精益规范）都是开源的。