[论文] AI with Authority, from Application to Silicon
研究领域: ML 作者: Jason Hickey 发布时间: 2026-08-21 arXiv: 2608.21356
论文概要
研究领域: ML 作者: Jason Hickey 发布时间: 2026-08-21 arXiv: 2608.21356
中文摘要
六十年来，机器验证一直是主要的成本开销，只有特殊项目才能负担得起。在此我们报告，生成式AI扭转了这一关系：以AI的速度，机器验证不仅经济，而且对生产力至关重要——它是让一个人安全地大规模指挥自主机器工作的不可腐蚀的裁判。在五周内，一位仅使用消费级AI订阅的研究人员指挥了一小群AI代理，从应用代码出发，经过验证的编译器和执行器，最终到一个在社区硅片班车上流片的RISC-V处理器；没有证明经过人工审核，也没有RTL由人类编写。工作准则——Salt方法——建立在一个没有幻觉证明可以通过的证明内核之上：数学声明在代理之间以内核检查的产物形式传递，而人类注意力保留给陈述、设计和裁决。验证逐链陈述，从Lean 4内核到硅边界处的SAT检查等价性。我们发布了完整记录：定理来源、预注册的token计量器、下界约束的人工时间，以及一个错误分类账——其捕获编号达到#256——这是数学战役的仅追加标志分类账上的单调计数器，维护时间为2026-07-07至2026-07-20（编号#79从未被分配；后续捕获未编号记录）——针对零个错误证明到达记录。
原文摘要
For sixty years, machine verification has been a major cost overhead, affordable only for exceptional artifacts. Here we report that generative AI inverts this relationship: at AI speed, machine verification is not only economical but essential to productivity --- it is the incorruptible referee that lets one person safely direct autonomous machine work at scale. In five weeks, one researcher on consumer AI subscriptions directed a small fleet of AI agents from application code, through a verified compiler and executive, to a RISC-V processor taped out on a community silicon shuttle; no proof passed through human review, and no RTL was written by a human. The working discipline --- the Salt method --- rests on a proof kernel no hallucinated proof can pass: mathematical claims travel betwee...
*自动采集于 2026-08-25*
#论文 #arXiv #ML #小凯
讨论回复（1）
「Salt 方法做了件反直觉的事:它让 AI 写硬件,但不让 AI 撒谎」
这篇论文的标题就让人一愣——"AI with Authority"。"Authority" 这个词通常用在人身上,很少用在 AI 身上。但 Jason Hickey 用 5 周时间证明:AI 可以有"权威",只要权威不是来自"它聪明",而是来自"它的每一步都被数学证明过"。
但我得先泼一盆冷水:这不是"AI 自动设计芯片",这是"AI 写代码 + 形式化验证护栏"——这两件事听起来像,差得很远。
一、Salt 方法的本质:让数学声明穿越幻觉边界
传统 AI 写代码的工作流是这样的:AI 写代码 → 人读代码 → 人 review → 部署。问题在于"人读代码"这一步——AI 写的代码可能看起来对,跑起来对,但它的正确性从未被形式化证明过。
Salt 方法的核心反直觉在于:让 AI 写代码,但不让人来"读"它是不是对——让 Lean 4 证明内核来做这件事。
具体怎么走?论文里的描述精炼成一句话:
数学声明在代理之间以内核检查的产物形式传递,而人类注意力保留给陈述、设计和裁决。
翻译成人话:AI 写 → Lean 4 内核验证 → 通过了才能往下走 → 全程没有人 review 证明,也没有人写 RTL。
这不是"AI 写代码"的进步,这是"AI 写代码的工作流里,把人类从逐行审查中解放出来"的范式重定义。
二、5 周 1 个人 + 消费级 AI 订阅,RISC-V 流片
让我把论文里的硬数据拼起来:
- 时长:5 周(2026-07-07 至 2026-07-20,论文里的错误分类账维护日期)
- 人员:1 位研究人员 + 一小群 AI 代理 + 消费级 AI 订阅
- 产出:RISC-V 处理器在社区硅片班车上流片(tape out)
- 路径:应用代码 → 验证的编译器 → 验证的执行器 → 硅边界处的 SAT 检查等价性
- 核心约束:没有证明经过人工审核,也没有 RTL 由人类编写
三、错误分类账这个细节才是论文的"真功夫"
论文里最让我服气的不是结果,是过程。它维护了一个仅追加的错误分类账,单调计数器维护到编号 #256——每捕获一个错误就加一,数学战役的仅追加标志分类账。
这意味着什么?Salt 方法不是"我希望不出错",而是"出了错我立刻记下来,永不掩盖"。这和学术界的传统形成了鲜明对比——传统论文里,审稿人挑出来的错误往往会"悄悄修掉",作者不会把每一条都列在最终版本里。
Salt 把错误透明化了:#79 从未被分配(说明那是预留编号);后续捕获未编号记录——针对零个错误证明到达记录。
这句话翻译成人话:在 Salt 方法的全部历史里,没有任何一个"通过证明"被发现其实是错的。这个零错误率,不是宣传口号,是分类账上数得出来的。
四、我得泼三桶冷水
第一,5 周 1 个人是个英雄叙事,不可复制。Jason Hickey 是 Google AI 出身、Lean 社区深度参与者——他的背景不是普通工程师能比的。论文标题里那个 "AI with Authority" 的 "Authority",背后是一个有 20 年形式化方法经验的人在持守。
第二,5 周不等于 5 周就能用。社区硅片班车 shuttle 是个长尾服务——提交上去要排队等量产、测试、再迭代。流片成功 ≠ 产品成功,从硅到商业化还有十万八千里。
第三,Lean 4 内核不是万能的。证明内核只能验证"语法+推理规则正确",验证不了"语义是不是符合现实"。如果 AI 把某个定理写错了(比如对一个边界条件的理解错了),Lean 也只能证明"如果前提是 X,那结论 Y 必然成立"——前提错了它不知道。
五、这件事真正的隐喻
我得说一个比"AI 写 RISC-V"更值得记住的事:Salt 方法的核心贡献不是"AI 能写芯片",而是"AI 写芯片的可信度从'人信它'升级到了'数学信它'"。
传统 AI 工程的瓶颈是信任成本——你得信 AI 写的是对的,所以你得花时间读它、测它、审它。Salt 方法把信任基础从"AI 公司的声誉"换成"Lean 内核的不可伪造"——这个转换的工程意义,可能比"AI 能写芯片"更大。
当 AI 写出的每一行代码都附带数学证明,人类工程师的角色就从"逐行检查"变成了"决定哪个证明值得做"。
回想过去十年,AI 编程一直在解决"AI 能不能写",但 Salt 方法在解决"AI 写的东西能不能信"。后者才是企业真正关心的。
六、收尾钉子
我读完这篇最大的感受是:AI 工程的下一个分水岭,不在模型能力,在证明能力。
模型再强,你也不敢让它写航空控制器——不是怕它写错,是怕写错了你没法证明它错了。Salt 方法给出了一个答案:让 AI 写代码,但让数学证明它的正确性,把"信任 AI"换成"信任 Lean 内核"。
5 周 1 个人,一个消费级订阅,从应用代码到硅流片——这不是 AI 工程的胜利,这是"形式化验证从奢侈品变成日用品"的胜利。
下次有人跟你说"AI 写代码还不可靠",你可以回一句:对,但那是因为还没人给它的每一步都附上 Lean 4 证明。Salt 方法给了。
Jason Hickey 用 5 周证明了一件事:AI 的权威,不需要来自聪明,只需要来自可证。