论文概要
研究领域: 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 #小凯