PaperlayerView exact revision on arXiv

Source-linked AI summary

AI with Authority, from Application to Silicon

Jason Hickey

arXiv:2608.21356v2cs.SEcs.AIcs.ARcs.LO

TL;DR

长期以来，机器验证对大多数软硬件工作而言成本过高；生成式 AI 虽然降低了候选证明和设计的生成成本，却没有让它们因此变得可信。本文介绍 Salt method，并报告一项为期五周、由一人完成的演示：从应用代码到 RISC-V 流片，全程采用 kernel-checked verification。

  • 问题

    机器验证长期以来成本高昂，除非面对特殊制品，否则难以实际采用；生成式 AI 降低了证明生成成本，却没有解决如何信任其输出的问题。

  • 方法

    Salt method 使用 kernel-checked artifacts 和具名 checkers 检验各项主张，将人工审查保留给陈述、设计和裁决，而不是证明本身。

  • 结果

    一人使用消费级产品，在五周内完成了从应用到硅片流片的 verified system stack 开发，并在每一层明确规定验证方式。

  • 要点与局限

    在这一经测量的工作范围内，机器验证是 AI-scale development 的前提，而人的注意力可以集中于陈述和设计决策。

  • 要点与局限

    本研究仅涉及一名专家实践者，未估计其他研究人员、团队或领域的结果。

Abstract

from arXiv · show

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.

1. 引言——一段个人历程

Salt 方法将生成式 AI 与形式化验证结合起来，使高度自主的开发从应用代码一直到硅片流片都可审计。本文呈现一个为期五周、由一人完成的案例研究及其可测量、可重放的完整记录，同时明确不主张该配置具有最优性、典型性或可推广性。

  • Salt 方法: Salt 方法通过将 AI 生成的软件与硬件开发建立在形式化方法之上，应对验证长期以来成本高昂且难以实施的问题。生成式 AI 降低了候选证明和设计的生成成本，但所提供的材料并未声称它能独立解决可信性问题。
  • 个人历程: 作者将这项工作描述为完成一项持续数十年的使命：把 1990 年的开关网络定理与 AI 驱动的软件和硬件开发连接起来。在得出软件开发是核心瓶颈后，构建能够开发软件的 AI 这一使命于 1992 年形成。
  • 演示: 一人利用面向消费者的订阅服务，在五周内指挥一支 AI 机群，将一个已证明的 1990 年定理推进到通过社区硅片穿梭项目完成流片的网络。这项工作在晚间和周末完成，AI 机群以形式化方法为基础。
  • 基线: 该案例研究从空的代码仓库起步，建立在公开的 mathlib 之上，并以 CompCert、seL4 和 CakeML 等经过验证的技术栈为参照 。这些里程碑式系统由专家团队历经数年构建，而本演示使用面向消费者的产品，在五周内完成。
  • 范围与局限: 本文不主张该配置对其他研究者而言是最优、典型或可推广的。其文档记录主张涵盖经内核检查、可重放的数学断言，经提交验证的定理溯源、计量化的经济性以及仅追加的错误日志。
  • 贡献: 本文贡献了一个全栈演示、明确的验证等级，以及对经济性、定理溯源和已记录错误的完整记录。文中还完整陈述了参考配置及其所需不变量。

结果 · 2. Salt——方法论

Salt 方法将可信验证视为一个双向问题：除非人类能够理解并验证待证规格，否则仅对实现进行机器检查是不够的。因此，该方法结合了五类由 agent 生成的工件、经 kernel 检查的证书、对抗性控制，以及人类对规格含义和不可逆操作的明确责任。

  • 2. Salt——方法论: Salt 同时处理实现正确性和规格正确性，因为经机器检查的证明，其可信度不超过它所证明的陈述。因此，该方法将形式化规格视为需要人类理解的对象，而不仅是验证的输入。
  • 2. Salt——方法论: 在每个尺度上，英文提示都会产出实现、规格、经 kernel 检查的证明、对抗性测试和简化的形式化证书。该证书用易于理解的词汇重述规格，而其经 kernel 检查的蕴含契约则将这一重述连接到已证明的陈述。
  • 2. Salt——方法论: 证书层使陈述级审查变得可行，而主动质询让人类能够要求针对绑定变量、假设和变更后假设的经 kernel 检查证据。审查被呈现为与系统持续交流的过程，而不是一次性阅读证书。
  • 2. Salt——方法论: 测试可以提升为定理，其中每轮 kernel fixture 为该方法提供了具体机制，将常规工程检查转化为证明。该工作流保留熟悉的测试实践，同时增加了定理提升这一额外操作。
  • 2. Salt——方法论: 只有人类能够判断规格是否符合其意图，以及已证明的陈述是否表达了读者所理解的含义。Salt 将这些验证边界视为一项明确的纪律，而不是一个默认假设。
  • 2. Salt——方法论: Salt 坚持 kernel-only truth、针对 kernel 无法检查之处的结构化对立，以及对稀缺人类注意力的有意节约。该方法包括执行前的对抗性反驳、对落地结果的独立见证、与命令关联的测量，以及旨在失败的控制。
  • 2. Salt——方法论: 该方法规定六项必需不变量和六项指导性条款，其中必需层与工具无关，指导性层则采用经过测量的参考配置。其要求还规定不可逆的对外操作必须由人类执行，并要求条件目标声明其假设和处置方式。

SALT 方法

Salt 方法将机器检查作为真理的基础，用结构化对抗检验内核无法验证的内容，并将人类注意力保留为最稀缺的资源。其必需不变量定义了该方法，而建议性文章描述了本案例中的配置运行与测量结果。

  • 机器检查确立真理，结构化对抗检验内核无法验证的内容，而人类注意力被视为最稀缺的资源。
  • 必需元素是强制性的，而实际运行的配置属于建议性内容。
  • 该方法将六项必需不变量与六篇描述参考配置的建议性文章区分开来。必需项说明该方法是什么；建议项说明本案例运行并测量了什么。

3. 裁判者——其立足之地 · 4. 机群——实践中的方法论

该工作流将 Lean 4 kernel 设为数学论断的唯一裁决者，同时通过一条有意采用非均质结构的 Lean 与基于 SAT 的检查链来确立硬件正确性。在实践中，一名人类指挥五个专门化 AI 席位，其交叉检查与对抗性审查生成可审计的错误台账。

  • 3. 裁判者——其立足之地: Lean 4 kernel 针对 mathlib [26] 检查每一条数学论断，并对每个定理进行公理审计；不使用 custom axioms 或 native_decide。该工作流的信任基础是一个紧凑、独立的 kernel，以及论断本身，而不是模型或其解释。
  • 3. 裁判者——其立足之地: 硬件正确性使用三个独立检查器：规格到制品的链接由 Lean 检查，而 Verilog 与 netlist 的对应链接则使用基于 SAT 的 Yosys 等价性检查。该检查链明确采用非均质结构，因为截至 2026-08-11 尚不存在通用的 Verilog-to-Lean importer。
  • 4. 机群——实践中的方法论: 五个长期运行的 AI 席位——协调、数学、编译器、硅和证据——共享一个 repository 与 append-only 消息总线，由一名人类统一指挥。这些席位依据 kernel ground truth 所启用的书面规则运行；每次提交都由第二个席位独立见证。
  • 4. 机群——实践中的方法论: 设计在执行消耗前会接受对抗性反驳审查，活动将由此产生的事件记录为可观测的错误记录。台账的单位是事件，而不是每次提及；它在出版前冻结时正式确定。
  • 4. 机群——实践中的方法论: 数学活动的对抗性层在一份事件台账中捕获了设计错误，其单调编号延续至 #256。append-only flags ledger 维护于 2026-07-07 至 2026-07-20；#79 从未分配。
  • 4. 机群——实践中的方法论: 对于每个目标，该方法都会产出实现、规格、kernel 检查的证明、对抗性测试和 kernel 检查的证书，由人类负责审阅并质询该证书。Figure 2 描述了共享 repository、append-only 消息总线以及 kernel 构成的机群运行结构。

5. 主干——从应用到硅片流片的演示

该演示在七天内构建出一套经过验证的系统栈，处于项目五周周期之内，沿着一条从定理陈述，经编译器和执行器，直到完成流片的实物设计的完整保管链。其核心贡献是这一端到端验证案例研究，而非硬件新颖性；每个环节都明确说明验证方式，并标出信任边界。

  • 5. 主干——从应用到硅片流片的演示: 这套七日系统栈沿着一条从定理陈述，经验证编译器和执行器，直到完成流片的实物设计的完整保管链展开。论文将该主干呈现为系统栈演示，而不是硬件贡献；验证逐环节说明，并在每个环节标出信任边界。
  • 5. 主干——从应用到硅片流片的演示: 该设计包含一个将结构化语言编译为小型指令集的编译器、其组件的仿真证明、352 个由 kernel 发出的触发器，以及综合记录中的 1,468 个时序单元。在所报告的配置中，第四个岛被禁用并保持连接。
  • 5. 主干——从应用到硅片流片的演示: 1990 年的交换网络定理在 kernel 中证明了路由调度的完整旋转闭包，并驱动了所提交的交换器。论文指出该定理承载于设计之上，并指向 Fig. 3。
  • 5. 主干——从应用到硅片流片的演示: 未给出芯片级来源比例，因为尚未在已交付设计的 GDS 上重新运行结构连接。该限制具体适用于已交付运行的 GDS，并不否定逐环节验证的记录。
  • 5. 主干——从应用到硅片流片的演示: 71 个文件中的 1,884 行 Lean 证书和 22,679 行由 agent 编写的 Verilog 代码，实例化了该系统与硅片部分的栈。所报告的硅片侧统计不包括 48 个文件中由流程生成的 294,232 行网表代码。

6. 锻造场——数学基础

数学攻坚在内核检查揭示的失败中锻造出 Salt method，同时产出了大规模机器检查 Lean 语料库。其宣称的目标——孪生素数猜想——仍未得到证明，但该语料库形式化了重要的 sieve 结果，并界定了该方法的适用范围。

  • 方法形成: 该方法的规则源于实践失败，逐步积累为判例法，其中包括幻觉式结果、错误设计，以及超出适用范围引用测量值。账本记录每条规则背后的事件，而不是套用预先设计的规则集。
  • 方法形成: 孪生素数基础的选择带有偶然性：任何将快速生成与不可腐蚀的检查器相结合的领域，都可能锻造出相同的规则。作者选择孪生素数，是因为内核下的困难数学构成了严苛的 proving ground。
  • 语料库: 37 天内生成了超过 320,000 行 Lean 4，按相同 extractor 计算，相当于 mathlib 的 29.3%。论文还公布了 658,103 行的原始计数，并报告了 3,466 次提交和零个无提交日。
  • 形式化数学: 该语料库对重要 sieve 结果的证明进行了机器检查，而这些结果此前尚未由公开的 proof-assistant artifacts 建立；对于存在并行 artifacts 的情况，论文标明独立形式化，而不声称首次完成。所调查的主张包括 Siegel–Walfisz、大筛、Bombieri–Vinogradov、下界 sieve 和 Chen 定理；独立形式化包括 Vaughan 恒等式、Maynard–Tao sieve 和 Montgomery–Vaughan Hilbert 不等式。
  • 局限与适用范围: 孪生素数猜想仍未得到证明：它被表示为一个定义，而条件性结果明确列出其假设；语料库则证明了相关 Maynard 类和 parity-invariant sieve certificates 的局限。报告的内核结果包括 M_2 ≤ 2 log 2 < 2，以及满足 M_k > 2 的最小 k 为 five [25]。

7. 经济学

经济学部分仅报告有记录支持的成本与生产力指标，并明确不提出缺乏依据的每条定理美元成本和归因主张。该部分记录了在116 h 40 m时间窗口内的37 h 21 m人工参与、大量无人值守运行，以及一种以定期人工裁决而非证明审查为核心的治理模式。

  • 测量限制: 记录无法推导出每条定理的美元成本、model-hours、按账户归因，或 Lean corpus 中生成内容与人工撰写内容的划分。本节将定量主张限制在项目记录直接支持的数值上。
  • 无人值守运行: 43.0%的数学 commits 落在至少一小时的静默窗口内，其中最长的20 h 56 m窗口包含26个 commits 和12,310行新增 Lean 代码。在四小时和八小时口径下，数学部分的占比分别为14.5%和8.8%；systems repository 的交互性更强，一小时口径为24.4%，四小时口径为4.6%。
  • 人工时间: 在116 h 40 m的计量窗口内，共有37 h 21 m的人工参与；根据已发布的相关性测量工具，机器生成的击键不计入其中。该估计涵盖45个参与时段，并注明不确定性范围为4分钟。
  • 人工的角色: 20次 council sitting 产生了有记录的裁决；人工执行了7项不可逆操作，拒绝了另外5项操作，提出1项设计否决，并完成9次源代码核验。在定期裁决之间，fleet 在执行层自主运行，没有证明经过人工审查。
  • 撤回: 一次 verification-cost ratio 在三次运行中的第二次将其改变了factor of 52后被撤回，这表明该配置的价值取决于受治理的数值，而非看似亮眼但缺乏依据的数字。其中一次运行落在原主张否认的10–100×开销范围内，撤回决定也保留在ledger中。

8. 裁判者导出的内容

该案例研究发现，以 kernel 为锚定的基准真值重塑了 AI agent 的行为：agent 彼此捕获作用域错误，在源头撤回断言，并将事件转化为成文规则。

  • 8. 裁判者导出的内容: 以 kernel 为锚定的基准真值使 AI agent 能够捕获彼此自信地犯下的作用域错误，并在源头撤回这些错误。这一发现表明，kernel 的认识论向外渗透进了 agent 的工作文化。
  • 8. 裁判者导出的内容: 由于不可腐化的基准真值锚定了其文化，这些 agent 将活动中的事件转化为成文规则。
  • 8. 裁判者导出的内容: 错误台账记录了反复出现的类别，包括以定律的作用域发布测量结果，以及声称世界状态而非对其进行测量的寄存器。

讨论

讨论指出，快速、低成本且可能出错的生成过程能够逆转形式化验证的传统开发成本负担，同时强调，本研究展示的是一种特定工作机制，而非研究生产力的一般理论。文章还强调，该工作形式化了已知数学，并报告了一个单人实践案例，且明确说明了适用范围的限制。

  • 解读: 形式化验证自 Floyd 和 Hoare 的程序逻辑以来一直成本高昂 ；但当生成过程快速、低成本且可能出错时，它可能变得切实可行。论文将这一机制与形式化开发主要仅适用于编译器、微内核和里程碑式定理的情况进行对比 [9, 14, 16]。
  • 范围与局限: 本研究没有提出新的重磅数学成果：孪生素数猜想未被触及，其广受赞誉的定理只是对已知结果进行了形式化。
  • 范围与局限: 证据仅限于一名专家实践者，不对其他研究者、团队、领域或劳动力市场作出任何主张，并包含经验证硬件链中明确命名的仅 SAT 链路。优先权主张均标注日期，因为该领域正以数周为时间尺度发生变化。

方法

方法部分定义了一个由五个席位组成的 fleet 架构，固定 Lean 4/mathlib 依赖版本 [26]，审计公理，并建立工具版本可追溯的验证链。文中还预注册 token 与人工时间核算，规定调查方案，并披露在消费级订阅下使用 Claude 系列 agents。

  • 方法: fleet 方法规定了五个席位、一条总线、治理规则、公开发布的协议文档、Lean 4/mathlib 依赖版本锁定 [26]，以及公理审计方案。验证链按环节记录其工具及版本。
  • 方法: 研究预注册了 token 计量器，并定义人工时间核算标准。
  • 方法: §6 的调查方法采用五条对抗性检索路径，并为每项主张建立证据文件。
  • 方法: AI 使用披露说明，研究在遵循期刊政策的前提下，使用消费级订阅运行 Claude 系列模型。

资助

本研究未获得外部资助。

  • 作者报告称，本研究未获得外部资助。
Loading 2608.21356v2…