具备权威的AI：从应用到硅片
AI with Authority, from Application to Silicon
- Bell Communications Research（贝尔通信研究所）
- Cornell University（康奈尔大学）
- Caltech（加州理工学院）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
该研究提出Salt方法，借助生成式AI与机器验证，在五周内由一名研究人员指挥AI智能体完成RISC-V处理器的流片，无人工审核证明与RTL，实现高效可靠的自主机器工作。
AI中文摘要：
六十年来，机器验证一直是主要的成本 overhead，仅能为特殊的人工产物所承受。在此我们报告，生成式AI颠覆了这一关系：以AI的速度，机器验证不仅经济，而且对生产力至关重要——它是公正的裁判，让一人能够安全地大规模指挥自主机器工作。在五周内，一名使用消费级AI订阅的研究人员从应用代码出发，指挥了一小队AI智能体，经过已验证的编译器和执行器，最终完成了在社区硅片 shuttle 上 tape-out 的RISC-V处理器；没有任何证明经过人工审核，也没有任何RTL由人工编写。这种工作规范——Salt方法——依赖于一个证明内核，任何幻觉产生的证明都无法通过：数学声明以内核检查的工件形式在智能体之间传递，而人类注意力则保留给声明、设计和裁决。验证是逐环节表述的，从Lean 4内核到硅片边界的SAT检查等价性。我们发布了完整的核算：定理来源、预注册的代币计量器、有上限的人工时间，以及错误台账，其捕获编号达#256——这是2026年7月7日至2026年7月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 between agents as kernel-checked artifacts, and human attention is reserved for statements, designs, and rulings. Verification is stated link by link, from the Lean 4 kernel to SAT-checked equivalence at the silicon boundary. We publish the complete accounting: theorem provenance, a pre-registered token meter, floor-bounded human time, and an error ledger whose catch numbering runs to #256 --- a monotone counter over the mathematics campaign's append-only flags ledger, maintained 2026-07-07 to 2026-07-20 (one number, #79, was never assigned; later catches are recorded un-numbered) --- against zero incorrect proofs reaching the record.
