当世界由无人理解的代码运行时会发生什么？

# 当世界运行在无人能懂的代码上时会发生什么？ 来源：https://time.com/article/2026/08/20/what-happens-when-the-world-is-run-on-code-no-one-understands-/ 国际数学家大会上月于费城召开，这是自1986年以来首次在美国举行。雅各布·齐默曼在接受数学界最高荣誉菲尔兹奖数分钟后，便告诉记者他将离开学术界投身人工智能安全研究。"我认为世界正在改变，"他表示，并补充说数学职业可能无法维持现有形态。 两个月前，他与其他八位数学家受邀评审一个AI模型是否真正证伪了现代几何学中一个有80年历史的基石——埃尔德什单位距离猜想。齐默曼和他的同行们确认该猜想已被推翻，他们为18页证明过程撰写的评述帮助将机器论证转化为人类可理解的数学语言。 这一突破及后续报告反映了阻碍我们在数学及其他所有领域取得新发现的瓶颈正在发生怎样的转变。纵观历史，稀缺资源曾是发现本身。而在AI时代，发现源源不断，人类的验证确认反而成为了稀缺资源。 需要明确的是，我们是AI乐观主义者。我们相信AI工具将与人类智慧相辅相成，拓展我们认知与构建的能力。但现有的发现验证与认证体系是为人类研究节奏设计的，这已成为当前的制约瓶颈。解决之道在于形式化：将AI的输出转化为可自动验证正确性的精确形式。构建实现验证常规化的基础设施已成为国家级工程挑战。 机器超越人类的领域远不止数学。支撑医院、银行和电网运行的代码也面临相同情况。例如今年四月，Anthropic公司披露其Mythos模型能发现主流操作系统和浏览器的未知漏洞，并将访问权限限制给五十家竞相修补漏洞的组织。随后不久，微软工程师在一款广泛使用的产品中发现90个关键漏洞；六月，参议员马克·华纳在参议院听证会上援引国家安全局局长的话称，该工具"在数小时内而非数周内就攻破了几乎所有机密系统"。 这一切发生在本就依赖我们默认正确代码运行的世界。2024年7月，一次软件更新故障就导致全球航班停飞、医院系统瘫痪。如今开发者可以通过"氛围编程"——即使用生成式AI通过自然语言提示编写代码。这让团队得以快速构建系统，但同时也会产生大量无人能完全理解的代码。 同样能加速发现的AI系统，如果将其生成能力与数学严谨性相结合，也能解决随之而来的信息过载问题。 数十年来，国防、情报、学术界和产业界的研究人员构建了替代盲目信任的方案：形式化验证方法——一套通过数学证明确保软件完全按照设计意图运行的体系。如同软件编译器将程序转化为计算机可执行指令，形式化验证将代码、功能规范及两者间的逻辑证明相结合，只有每个逻辑步骤都通过验证才能接受程序。这使得自动验证AI输出成为可能，更广泛地为软件及其他安全保障提供严格依据。生成式AI工具让这种形式化方法得以普及，这在以往是难以想象的。 一旦证明检验成本降低，下一个瓶颈就转变为编写正确的规范。精确决定系统功能并捕捉其运行环境仍依赖人类判断。即使对错误规范进行了完美证明，也只是在回答错误的问题。形式化验证无法阻止网络钓鱼，不能杜绝复杂人文系统的所有故障，也无法认证AI模型的整体安全性——但它能消除关键软件中的整类错误。对于故障可能危及数百万人的系统，这应成为采用AI生成代码的关键步骤。 国际数学联盟六月认可的《莱顿宣言》警告AI威胁着数学证明的可验证性。我们则持相反观点：数学提供了使生成式AI更可信的基础设施。正因如此，美国应将数学严谨性视为国家使命。我们需要经过验证的软件公共基础设施：包含经过验证的组件与规范的开放库、标准与基准、改进的更新检查工具，以及连接数学、计算机科学、工程学与国家安全的跨领域培训项目——这些工作需要多部门协同而非局限于单一计划。由于形式化方法建立在深厚的数学基础之上，这要求对数学研究和教育进行持续投入，而非仅关注其应用开发。 运营关键基础设施的企业不应在可能危害公众的情况下仅依赖被动修补和漏洞悬赏。相反，应从设计之初就致力于构建审计机制和形式化保障。目标并非对程序的每一行代码进行形式化验证，而是识别关键系统的核心逻辑，明确该逻辑必须遵循与禁止的行为规范，并实现对该逻辑的数学验证。 数学曾多次化解信任危机。几何学、无穷概念、逻辑学与证明本质曾使数学界陷入根本性怀疑，而每次应对都催生了更精确的语言、更严格的标准与更完善的验证体系。正是这种严谨性使数学得以规模化发展，如今软件同样需要这种变革。当AI编写越来越多支撑世界运行的代码时，盲目信任已不再足够。关键在于美国能否引领向数学化信任体系的转型，而非坐视失败将其迫在眉睫。