Opus 4.8 一次跑出带证明的算法:形式化验证正在变成模型的硬基准

概述

一名开发者(GitHub 用户 schildep)公开了一份多边形求交算法,自称是”据我所知第一个被形式化验证的多边形求交实现”。真正值得记的不是这个算法,而是它的生产方式:他给 Opus 4.8 一行形式化规格,模型自主跑了约八小时,产出了实现加一份在 Lean 4 里通过检查的正确性证明,而他之前用旧模型做同一件事时反复卡住。

这件事的信号价值在于它的判据很硬:形式化证明要么被 Lean 检查器接受,要么不被接受,中间没有”看起来对”的灰带。它不像跑分那样可以靠记忆题库或对齐评测口味来虚高。所以”Opus 4.8 一次跑通、此前模型失败”是一个干净的能力信号。但要把话说准:这是一个能用一行规格精确描述的问题上的一个案例,不是”模型学会形式化验证了”这种普遍结论。下面正面回答三件事:这个结果到底证明了模型什么、形式化验证为什么是个好基准、哪些解读是过度的。

发生了什么

作者要做的是多边形求交:给定两个多边形(可以带洞、自交、边重叠),构造出一个新多边形,它的内部正好是两者内部的交集。这类计算几何算法出名地难用普通测试验证,因为大量复杂性都藏在罕见的特殊配置里(边正好重叠、顶点正好重合、洞大小恰好处在临界点上,导致边界分组方式不唯一)。配置有无穷多种,经典测试无法穷举。

他没有靠测试,而是用 Lean 4 证明助手把”求交”这件事形式化成一条规格:结果的内部等于两个输入内部的交集,然后让 agent 产出满足这条规格的实现加证明。整套设计刻意压缩了人要审的东西:人只需读三个文件、共 87 行简单的 Lean 规格(主要是多边形的基础几何定义和算法接口),再跑一遍 Lean 检查器。带证明的实现部分(那些 ...Proofs.lean、...Impl.lean 文件)由 agent 自主写成,作者自己说从没读过,也不需要读,因为信任来自检查器而非模型。他还专门检查了证明只依赖三条公认可信的公理(propext、Classical.choice、Quot.sound),以防 agent 偷偷塞进一条假设把证明蒙混过关。

模型间的差距是这个项目最有信息量的部分,因为是同一个人、同一个目标的纵向对比。按作者的记录:年初他用 Opus 4.5、4.6 起步,4.5 是第一个能处理非平凡 Lean 证明的模型,但只有当他先把一份严格的证明草图写出来,它才能翻成 Lean,比如”内部定义与射线方向无关”这个引理就得拆成很多小步喂给它,之后他卡在这里直到 4.7 发布。4.7 能迈更大的步子,能证明”任意两个多边形的交存在”,但仍要他给出用 Eulerian 回路的思路、并分步提示怎么处理棘手的特殊情况。4.8 发布次日他在 ultracode 模式下并行开了两个会话:一个在隔离容器里从零、无提示重证主定理(几乎是此前全部工作),一个去扩展处理 4.7 反复失败的边重叠特殊情况。两个都在几小时自主工作后成功了。他观察到 4.8 的一个具体变化:面对一个可能本身就错的中间引理时,旧模型会一头扎进去耗时间,4.8 会”起疑”并主动转向另一条策略,有一次还自己起了并行子 agent 去试多条路。

作者也诚实记下了代价:强迫 agent 形式化验证,往往产出更慢、忽略规格没捕捉到的实际工程考量的代码。他猜这既来自验证难度本身在逼简单代码,也来自训练数据里几乎没有”已形式化验证的实用软件”。

为何重要

形式化验证作为模型基准,稀缺价值在于它诚实。今天大多数前沿模型的能力宣称都建立在跑分上,而跑分有结构性弱点:题库可能进了训练集,评测可能被对齐到迎合某种答题风格,分数高一两个点很难说清是真本事还是过拟合。形式化证明没有这个灰带。Lean 检查器是个确定性系统,它接受或拒绝一份证明,跟模型说得多自信、过程多漂亮都无关。一个模型要么交出了通过检查的证明,要么没交出。这种判据上的硬度,正是它比刷分更适合衡量”模型能不能真的把一长串严密推理走到底”的原因。

它还顺带解决了 agent 编码里最难的一个信任问题。平时让 agent 写代码,你要么逐行审,要么写一堆单元测试再祈祷边界都覆盖到了,两者都既贵又不彻底。这个项目把信任的锚点从”读 agent 写的几百行实现”挪到了”读 87 行规格 + 信一个确定性检查器”。agent 写的实现和证明可以当黑箱,不用人看也能判定正确。这是一种和”审代码”根本不同的协作形态:人只负责把问题说对(写规格),正确性由机器保证,中间那段重活外包给模型且无需信任它。对任何在乎正确性强保证的领域(作者引的 NASA 例子是算自动驾驶禁区),这条路径比”让 AI 多写测试”有意义得多。

成本曲线是这件事真正可能改变判断的地方。作者引的 NASA 2021 年工作,验证的是另一个多边形算法(合并而非求交),那是 2021 年、还没有能干的大模型,论文里提到他们人手写了 700 条引理才完成证明。形式化验证历来只对极关键软件值得,就是因为这种人力成本。如果 agent 能把”写引理、补证明”这段自动化掉,门槛会往下移。但要clear:目前现实的前提是问题能用一行规格精确描述,多边形求交满足,大量真实软件不满足。

对建设者的影响

如果你在用 agent 写代码,这里真正可借鉴的不是”用 Opus 4.8”,而是这套把信任锚点搬走的工作流。在你的问题里找出那一小块能被精确规约、且正确性代价高的核心(几何、并发、状态机转换、协议、权限判定这类),把它从一堆”看起来能跑”的代码里隔出来,只对它写形式化规格,让 agent 去填实现和证明,你只审规格、跑检查器。作者那个”人只读 87 行、其余当黑箱”的结构是可以复用的设计:实现可以增长、可以被后续模型优化,要人审的规格不变大。

但别急着把它套到一切上。这套路只在”目标能写成一行规格”时成立,而大多数业务逻辑的正确性根本无法这么干净地形式化(把”算对钱”写成规格本身就是开放难题)。作者也记下了实际代价:被逼着出证明的代码往往更慢、忽略工程考量,他下一步第一件事就是回去改性能。所以现实的用法是挑核心组件做,不是指望 agent 给整个系统配证明。在能用上的地方,它把”逐行审 agent 代码 + 堆单元测试祈祷覆盖到边界”换成了”审一小段规格 + 信确定性检查器”,这是实打实的省事。

对研究者的影响

如果你在设计模型评测,这个案例提示了一类被低估的基准:让模型在 Lean、Rocq 这类证明助手里产出通过检查的证明。它的好处不只是难,而是判据客观、且天然抗污染:一份新的、没进过任何训练集的形式化规格,模型要么证出来要么证不出来,没法靠背题蒙混。比起又一个会被刷爆、被怀疑数据泄漏的编码 benchmark,这类任务更能区分”真的会做长链严密推理”和”模式匹配得好”。作者无意中给出了一个纵向数据点:同一难题上,4.5 只能翻译人写的草图,4.7 能在有思路时迈大步,4.8 能自主提出并执行整套策略并在歧路上自我纠偏。这种”能自主走多长一段证明而不需要人接管”的指标,可能比单点通过率更能刻画推理能力的进展。

要警惕的研究陷阱是把单点当曲线。这是 n=1 的观察,出自一个对 Lean 很熟、知道怎么搭好脚手架(把规格和实现/证明分离、用主定理当检查点)的作者之手。换个不会写规格、不懂 Lean 的人,同一个模型大概率跑不出同样结果。模型能力是这个结果的必要条件,不是充分条件;脚手架和提问者的专业度同样在起作用。

该忽略什么

忽略”模型会形式化验证了”这种概括。准确的说法是:在一个能用一行规格精确描述、且作者搭好了脚手架的问题上,Opus 4.8 自主产出了一份通过 Lean 检查的证明。这跟”模型能对任意软件做形式化验证”差着十万八千里。绝大多数真实系统根本写不出那样干净的规格——你想验证一个交易系统”永远不会算错钱”,光是把”算对钱”形式化下来就是个开放难题。一行规格能精确刻画目标,本身就是这个问题被选中的原因,不是模型搞定了的普遍能力。

也别把”八小时自主跑通”读成”高效”或”便宜”。作者明说 4.8 跑了约八小时,且形式化验证倾向于产出更慢、更不实用的代码;他的”下一步”清单里第一条就是测量并改进性能、简化绕远路的证明。这是一个能力到了、但工程效率和成本还远谈不上成熟的状态。它说明”做得到”了,没说明”划算”。

最后,别因为这事登上 HN(93 赞)就把热度当成重要性的证据。值得记的是那个硬判据——证明通过了确定性检查器,以及同一作者跨四代模型的纵向对比;赞数只是说有人觉得有意思。HN 上真正有价值的讨论也不在点赞,而在追问细节:有人指出验证核心用的是精确有理数而非浮点数(浮点的形式化验证要难得多),编译成 WebAssembly 的是 Lean 核心、外层 JS 界面并未验证。这些细节恰恰提醒:这个结果的含金量,要落到”验证了什么、在什么假设下”才说得清,而不是一句”AI 证明了一个算法”。

来源

1. 已形式化验证的多边形求交(项目自述,作者称用 Opus 4.8 一次跑通) / blog
2. Show HN:已形式化验证的多边形求交,Opus 4.8 一次过、此前模型失败(Hacker News,93 赞) / hn

无官方一手源；本文基于可靠二手报道（具名媒体、交叉印证）写成。