---
title: VNN-COMP 2026 结果出炉：α,β-CROWN 居首，首次参赛的 Vibecheck 位列第二
dek: 国际神经网络验证竞赛于 7 月 24 日公布 2026 年结果，α,β-CROWN 在两个赛道均排名第一。据石溪大学介绍，排名第二的 Vibecheck 用了大约两个月开发完成，代码由 Anthropic 的 Claude 生成。
disclosure: 调研和起草本简报的程序基于 Anthropic 的 Claude 模型构建。本简报的报道涉及一款工具，其开发者用 Claude 编写了代码。
---

2026 年 7 月 24 日，国际神经网络验证竞赛（VNN-COMP）的组织者在里斯本公布了 2026 年比赛结果。[^1]竞赛比较的是这样一类工具：它们检查神经网络是否具有某项性质。这里的性质是一项精确要求，规定网络对给定范围内的每个输入应如何表现。工具要么试图证明该性质成立，要么试图找出一个违反该性质的输入。[^3, 4]

本届共有 13 款工具参与计分。常规赛道包含 24 个基准、3,373 个实例，每个实例是一个单独的验证问题。α,β-CROWN 在这一赛道以 2,344.0 分排名第一，其后依次是 Vibecheck（2,278.6 分）和 PyRAT（1,813.6 分）。在包含六个基准的扩展赛道上，三者的名次顺序相同。各项得分和计分报告于 8 月 3 日发布在 GitHub 上。[^2]

每个正确答案得 10 分，每个错误答案扣 150 分。每个基准的得分会换算成该基准最佳工具得分的百分比，工具的总分就是这些百分比之和。[^3]

工具如果报告网络违反了该性质，就必须提交反例，即一个违反该性质的输入。组织者会运行网络来检验反例。一项诚信守则要求工具只有在证明了某项性质成立之后，才报告该性质成立。计分脚本只在另一款工具提交了有效反例时，才对这类答案扣分。[^2, 3]计分报告显示，α,β-CROWN 有一个错误结果，即一个未通过检验的反例；Vibecheck 和 PyRAT 没有错误结果。[^2]

Vibecheck 出自石溪大学 Stanley Bak 领导的团队。该校称，这款工具还获得了本届竞赛的最佳新参赛工具奖（Best Newcomer Tool）。据石溪大学介绍，团队通过向 Anthropic 的 Claude 输入提示词来生成代码。Bak 说，他大约在比赛前两个月开始动手。他把这项工作比作管理一个团队，而他并不逐行阅读团队写的代码：“我要求的是正确性的证据。”[^4]Bak 是今年的组织者之一。竞赛规则允许组织者提交工具参赛，但不允许他们赢取奖金。[^3]

:::analysis
Vibecheck 没有错误结果，意味着它提交的反例都通过了重放检验，其他参赛者也没有推翻它报告的“性质成立”结论。但这还不足以表明它的验证是可靠的（sound），也就是从不错误地报告某项性质成立。这是因为，工具错误地报告某项性质成立时，只有另一名参赛者推翻这一报告，竞赛才会发现。如果开发者没有完整阅读验证器的代码，这一缺口就更加要紧，因为 2026 年的规则并不要求提交可由独立检查器验证的证明。
:::

:::checked
我们于 2026 年 10 月 20 日阅读了 VNN-COMP 网站、2026 年竞赛规则、结果代码库中的计分表和计分脚本，以及石溪大学 9 月 28 日的文章。我们没有在 arXiv 上找到组织者的总结报告。我们没有运行任何工具。关于最佳新参赛工具奖和 Vibecheck 的开发过程，我们依据的是石溪大学的说法。
:::