Anthropic 10 月 22 日发了一篇文章讲他们和 Theorem 合作用 Claude 给 100 多个开源库做形式化验证先把“什么绝对不能发生”写成规则让 AI 去写证明再交给机器逐条检查。我第一遍读完确实没太看懂。Rocq、RISC-V、OSS-Fuzz、ASan一个术语接一个术语。读到最后我也说不清它跟我有什么关系。后来实在头疼就偷懒让 AI 帮我看完全文再总结又跟 AI 聊了几轮我才知道这篇文章对我们大多数人有价值的点是它的做法我们给 AI 定规矩让 AI 按规矩去做再让 AI 去找出违反规矩的反例。跟 AI 协作我越来越觉得关键问题是规则该怎么找。它到底做了什么平时写单元测试像是抽查几道题输入 A应该得到 B。模糊测试更进一步让机器随机出海量的题去撞 bug。但题是出不完的撞得再久也不能说“没有了”。形式化验证换了个思路先把“什么算对”写清楚这叫规格再给出一份证明说明所有输入都满足它。证明卡在哪里就顺着那里去找 bug。以前很少有人这么做。证明比代码本身大得多只有极少数专家写得了。这次他们让 Claude 来写。起点是 Google 的 OSS-Fuzz 平台上开源项目开发者已经写好的模糊测试。他们把每个测试的规格定成一句话任何小于 64 MB 的输入都不会让程序崩溃不出现内存错误也不出现断言失败。注意这句话的写法。他们没有写正面的要求没有去描述程序应该做对什么他们写的是反面的要求什么绝对不能发生。换成我们跟 AI 说话的方式这是一条负面提示词。Claude 负责写证明一个叫 Rocq 的证明检查器负责逐条验收。证明写出来非常长但人不用读。按原文的说法人只需要信三样东西机器和操作系统的数学模型、定理本身是怎么写的、检查器本身。Claude 自己说“我证完了”不算数检查器说了才算。这跟我上一篇写的是同一件事干活的那个不能自己给自己判卷。检查器只管程序满不满足规格。规格写得对不对还得人来看。附录里有两个数字我印象很深。第一个在一类证明任务里Claude 几乎都会先自己写一份简短的规格再去证明。规格的中位数大约 110 行对应的程序中位数大约 86 KB 代码。第二个来自另一个实验。研究者让 Claude 用 Rust 写一个能运行 Python 程序的解释器覆盖 Python 的很大一部分语法一边写一边证明它的行为和一篇论文里定义的 Python 规则一致。为了比一比测试和证明各能抓到多少问题研究者在这个解释器的早期版本里故意埋了 7 个 bug。先用随机生成的测试去跑7 个 bug 里只发现了 2 个另外 5 个没被发现程序照样通过了测试。再用证明去查7 个 bug每一个都让证明过不去全被发现了。测试只能发现它碰巧撞上的问题。证明要求所有情况都符合规则哪一处不符合都会卡住。证明的过程中Claude 也找到了一些模糊测试很难碰到的 bug。比如一个解压程序里有个计数器会减过头导致往内存里不该写的地方写数据。它只在大约 20 MB、结构很特别的输入上才会触发而模糊测试一般只喂 1 MB 以内的小输入。看着很好是吧好像 bug 很容易就能找出来。但实际上一个证明要花几亿 token作者也说成本是眼下最大的门槛。审规则不审实现AI 写的代码越来越多人一行行审肯定审不过来。这篇文章给了一个很清楚的分工规格只有一百来行人审得过来几十 KB 的代码交给 AI 去证明检查器负责判卷。这也是我一直以来的看法人不用亲手写每一行也不用逐行读懂每一行但什么算对得由人来定义。规则写成“不能发生什么”AI 才有东西可撞。你跟 AI 说“把这个函数写好”它不知道该往哪里找反例。你说“任何输入都不能让它崩”它就有了明确的目标去找那个能让它崩的输入。找到了那是 bug找不到而且能证明找不到这份证明就成立了。原文有一段把这层关系讲得很直白很多模糊测试本来就在检查更高层的规律比如压缩再解压结果必须和原来一模一样。规律一旦不成立程序就会崩。所以证明它“永远不崩”等于证明了这条规律本身。还有一个细节我很喜欢。为了不让 Claude 每遇到一个 bug 就停下来等人他们允许它在证明途中自己修 bug。但这就留了一个口子Claude 完全可以把程序改成一个什么都不做、所以永远不会崩的程序定理就轻松证完了。所以他们又加了一条规矩任何改动都扣分能证明这次改动影响了哪些输入、而且影响得很少才额外加分所有改动都要记录、审计。规矩会被钻空子所以规矩还得管住“怎么满足规矩”。人不用读懂每一行实现但“什么绝对不能发生”必须由人说了算。今天就能上手8 条单测全过一条规则 0.14 秒找到 bug形式化证明我们跑不动但它的“抽查版”谁都能跑叫属性测试property-based testing。普通单测写的是例子“输入 A得到 B”。属性测试写的是规律“对所有输入这件事都必须成立”。工具会自动生成大量输入去撞撞到反例后还会把它缩到最小。Python 里有 HypothesisJS/TS 里有 fast-check。Anthropic 今年 1 月也发过一篇思路相近的文章让 Claude 读代码、猜规律、写 Hypothesis 测试在 NumPy、SciPy、Pandas 里找到了 bug。我拿一个分和元互转的小函数试了一下把以“分”为单位的整数转成“¥1,234.56”这样的字符串再解析回来。defformat_yuan(fen:int)-str:yuan,centsdivmod(fen,100)returnf¥{yuan:,}.{cents:02d}看起来没毛病吧先写 8 条普通单测0、5 分、整元、千分位、百万级、解析带不带角分最后一条是几个手挑的往返例子。结果8 passed。再换成属性测试。不写任何具体例子只写一条规矩任何整数格式化以后再解析都不能变。given(st.integers())deftest_roundtrip(fen):assertparse_yuan(format_yuan(fen))fen跑一次0.14 秒失败。Hypothesis 给出的最小反例是这样的E AssertionError: assert -199 -1 E where -199 parse_yuan(¥-1.99) E where ¥-1.99 format_yuan(-1) E Failing test case: test_roundtrip( E fen-1, E )退款 1 分钱显示成了 ¥-1.99解析回去变成了 -199 分。原因是 Python 的divmod对负数向下取整divmod(-1, 100)得到的是(-1, 99)。8 条单测为什么全过因为里面全是 0 和正数一个负数都没有。测的都是写测试的人想到的情况bug 恰好藏在没想到的地方。我又换了 50 个随机种子各跑一次。50 次都失败每次都缩到同一个最小反例fen-1。修复只要两三行先取符号再对绝对值做divmod。修完以后属性测试和原来的 8 条单测一起跑9 passed。单元测试属性测试形式化证明写的是什么几个例子对所有输入都成立的规律规律加一份证明能说明什么这几个例子是对的抽查没找到反例所有输入都满足规律今天谁能用所有人所有人极少数项目负面提示词为什么好用拿我自己来说我给 AI 写的要求越来越多是这种形状“不要编数据”“不要改已经确认的部分”“不要自己放宽验收标准”。这比“请认真写”“请保证质量”管用。原因在于一句“绝不能”天然是一句对所有情况都成立的话。“不能编数据”意味着文章里每一个数字都得有出处。它是一条规格一个不变量。AI 可以拿着它一条一条去对去找反例。“写得专业一点”呢它只是一种感觉。AI 只能猜你想要什么样你也没法拿它去检查到底哪一句违反了它。单测和属性测试的区别也是这样。“输入 123456得到 ¥1,234.56”是一个正面的例子“任何整数转过去再转回来都不能变”是一条规矩。前者只覆盖你想到的情况后者逼着工具、逼着 AI 去找你没想到的情况。所以我会认为负面约束好用是因为它把一个模糊的期望变成了一条可以被撞、可以被检查的规则。那么跟 AI 协作的时候规则该怎么找结合这篇文章和这个 demo我整理了五条可以直接用的做法。第一先问“对所有输入什么必须成立”让 AI 写代码、写测试之前先让它回答这个问题而不是先列几个例子。答案写出来人只审这几行。第二从几种常见的规律里找原文列过模糊测试常检查的几类规律下面这四种最好上手往返编码再解码、格式化再解析必须拿回原样。demo 里抓到 bug 的正是这一条。幂等同一个操作做两次和做一次的结果一样。不变量比如排序前后元素个数不变。对照新实现和旧实现、和参考实现给同样的输入结果必须一致。第三写一份“绝不能出现”清单Anthropic 的规格本身是一条“绝不能”任何输入都不能让程序崩。放到自己的项目里可以是“金额转一圈不能变”“已经确认的结论不能被改掉”“引用不能没有出处”。每一条都要具体到能检查出是不是被违反了。第四规矩要连“怎么满足”一起管AI 也会走捷径。只写“测试必须通过”它就有动机去改测试只写“不能崩”它就有动机把程序改成什么都不做。所以要像 Anthropic 那样再补一条每次改动都要说明改了什么、影响了哪些输入并且留下记录。第五人定规则AI 去撞机器判卷定规则是人的活找反例是 AI 的活判卷交给机器测试框架、类型检查、证明检查器。别让写代码的那个 AI自己给自己判卷。规则写成“不能发生什么”AI 才知道该去哪里找反例。别人怎么看这篇文章出来以后也有不少冷静的声音。Hacker News 的讨论里有一类常见的质疑你怎么知道 AI 证明的正是你想要的规格和你真正的意图之间隔着一段距离。这恰好说明了人该站在哪。证明可以交给 AI判卷可以交给检查器“这条规格是不是我想要的”只能人来回答。threatline 的分析更直接文章里唯一能独立核对的 libexpat 漏洞四个月前就已经作为 CVE 公开了。他们的结论是应该把这次看作“验证吞吐量的跃升”而不是“这些库都安全了”的保证。Dragonfly 的 Haseeb Qureshi 说得也中肯它不是万能药但比凭感觉测过强得多。审不过来靠什么验收上一篇我写 Lauren Tan 一个月 2000 个 PR结论是靠人一行行审审不过来但独立验收这一环不能消失。这篇文章让我看到了验收的另一种做法人不去追着几十 KB 的实现看而是把一百来行“什么绝对不能发生”写清楚让 AI 去找反例让机器判卷。AI 写代码的速度已经上来了跟不上的是验证。上一篇最后我说能放手多少取决于验收靠不靠得住。现在我多了一个答案验收靠不靠得住先看规则有没有写清楚。本文读的原文Anthropic《LLMs are making formal software verification feasible at a much larger scale》https://www.anthropic.com/research/formal-verification原文附录https://www-cdn.anthropic.com/files/4zrzovbb/website/6867eadf760258fa8b42a504600cd3c036d16358.pdf公开的证明仓库https://github.com/theorem-labs/oss-verify-proofsAnthropic 的属性测试文章https://www.anthropic.com/research/property-based-testingHypothesishttps://hypothesis.readthedocs.io/ fast-checkhttps://fast-check.dev/Hacker News 讨论汇总daily.devhttps://daily.dev/posts/llms-are-making-formal-software-verification-feasible-at-a-much-larger-scale-oarwz7ikuthreatline 的分析https://agentblog.threatline.io/posts/claude-formal-verification-123-libraries/Haseeb Qureshi 的评价转引自 WebProNewshttps://www.webpronews.com/anthropic-theorem-claude-formal-verification-oss-fuzz/
实战指南与优化策略)
