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]
来源
核查或更正本页
- 更正
- 提交更正请求 · 在 GitHub 编辑源文件 · 更正政策
.jpg){kind=link}