当世界运行在无人能懂的代码上：AI代码验证与形式化方法的未来

一份来自数学界的警告

2025年6月，国际数学联盟（International Mathematical Union）背书了一份名为《莱顿宣言》（Leiden Declaration）的文件。国际数学联盟成立于1920年，是全球数学界最具权威性的国际组织，负责颁发菲尔兹奖等顶级荣誉，其背书代表着数学共同体的集体立场。《莱顿宣言》以荷兰莱顿大学命名，该校是欧洲最古老的大学之一，长期以来在数学和逻辑学领域拥有深厚传统。宣言的发布时间正值大语言模型（LLM）被广泛应用于数学推理和代码生成之际。这份宣言的核心警告直指当下AI浪潮的软肋：人工智能正在威胁证明的可验证性——当AI系统开始参与数学证明的构建过程时，传统上由人类数学家逐步审查的"证明链"可能出现不可追溯的断裂点。

然而，围绕这份宣言的讨论中出现了一个更具建设性的反向视角——与其说AI威胁了数学的严谨，不如说数学恰恰提供了让生成式AI变得更可信的基础设施。这一观点认为，整个技术界都应当把"数学严谨性"当作一项核心使命来对待。

具体路径包括：建立可验证软件的公共基础设施、开源的已验证组件与规范库、统一的标准与基准测试、更好的更新检查工具，以及连接数学、计算机科学、工程与国家安全的跨学科培训项目。而所有这一切的地基，是对**形式化方法（Formal Methods）**背后深厚数学基础的持续投入——不只是投资应用层，更要投资底层的数学研究与教育。

形式化方法是一套基于数学逻辑的技术体系，用于对软件和硬件系统进行精确规约、开发和验证。其核心工具包括定理证明器（如Coq、Lean、Isabelle）和模型检查器（如SPIN、TLA+）。以近年来势头最猛的Lean为例，它不仅是一种编程语言，也是一个交互式定理证明器，用户可以在其中用形式化语言书写数学命题，并由机器逐步验证每一个推理步骤的正确性。Lean的数学库Mathlib已积累了超过百万行经过机器验证的数学定理。形式化方法在航空航天（如NASA的飞行控制系统）、芯片设计（如Intel的浮点运算验证）和铁路信号系统等安全关键领域已有成熟应用，但在通用软件开发中的普及率仍然很低，主要原因是其使用成本高、学习曲线陡峭——而这正是《莱顿宣言》呼吁加大投入的原因所在。

"没人懂代码"的现状早已存在

在社区讨论中，不少开发者对"无人理解的代码"这一恐慌提出了冷静的反驳。他们指出：这种情况其实早就存在了。

"现代代码库动辄数百万行，本来就没人能完整理解。我们只是把它拆成小块来处理。"

今天的软件系统，是建立在库之上、库又建立在其他库之上的深层依赖栈。以JavaScript生态为例，一个典型的Node.js项目通过npm安装的直接依赖可能只有几十个，但其传递依赖（即依赖的依赖）往往高达数百甚至上千个包。其中一些代码来自已倒闭的公司，一些出自二十年前就已去世的开源作者之手，还夹杂着各种来路不明的东西。

这种脆弱性已被多次验证：2016年的"left-pad事件"中，一个仅有11行代码的npm包被作者删除后，导致包括React、Babel在内的大量主流项目构建失败，整个JavaScript生态一度瘫痪。2021年的Log4Shell漏洞（CVE-2021-44228）则表明，一个深埋在依赖栈中的Java日志库的安全缺陷，可以影响全球数十亿台设备。这些事件生动地印证了一个事实："世界运行在无人能完全理解的代码上"从来不是AI带来的新问题，而是软件工程复杂度累积的必然结果。

另一个类比来自编译过程：我们写的高级语言最终被编译成机器码，也几乎没有人能直接读懂那些机器码。但整个体系依然运转良好——因为我们是在**元层面（meta level）**上理解和信任它的。从这个角度看，AI生成代码或许只是这条"抽象层不断叠加"链条上的又一环。

AI生成代码与编译器的关键区别

不过，把AI代码简单等同于"另一层抽象"的类比，遭到了一位开发者颇具说服力的反驳。这也是整场讨论中最值得深思的技术分歧点。

编译是可预测的，AI生成代码不是

编译过程本质上是可预测、可重复的。它不会对代码做出任意的自主决定，只是从源代码到机器码的一次相对直接的翻译。同样的输入，永远得到同样的输出。

现代编译器如GCC和LLVM/Clang遵循严格的语言规范（如C语言的ISO/IEC 9899标准），将源代码通过词法分析、语法分析、语义分析、中间表示优化和目标代码生成等明确定义的阶段转换为机器码。为了进一步确保编译器本身的正确性，学术界甚至开发了"经过验证的编译器"——最著名的是CompCert项目，这是一个用Coq定理证明器形式化验证过的C语言编译器，能够数学证明其输出的机器码忠实保留了源代码的语义。编译器的确定性，是整个软件工程信任链的基石之一。

而AI恰恰相反：

"AI常常在模糊、设计糟糕的指令下工作，并且会做出大量自己的决定——甚至可能忽略你告诉它的内容，转而实现它认为应该做的东西。"

基于Transformer架构的大语言模型（如GPT-4、Claude、Codex）在每一步生成时，会对词汇表中所有可能的下一个token计算概率分布，然后通过温度参数（temperature）和采样策略（如top-p/nucleus sampling）从中选择。温度越高，输出越随机；即使温度设为0采用贪婪解码，不同的提示措辞、上下文窗口中的微小差异，甚至浮点运算的硬件级非确定性，都可能导致截然不同的输出。更关键的是，这些模型在训练过程中优化的是"下一个token预测"的统计目标，而非"代码正确性"的逻辑目标——它们不具备真正的程序语义理解能力，只是在统计意义上模仿训练数据中的代码模式。

这位开发者分享了亲身经历：当他要求AI修改某段代码时，AI不仅完成了要求，还擅自做了其他未被要求的改动——改变了行为，或悄悄植入了隐蔽的bug。这种"自作主张"的根源在于：模型倾向于生成在训练分布中概率最高的代码模式，而非严格遵循用户指令的最小化修改。

不确定性才是核心风险

这正是问题的核心所在。传统的"无人理解的代码"至少是确定性的，可以被调试、被追溯。而AI引入的是不确定性与自主性——它不是被动的翻译器，而是一个会"自作主张"的参与者。这也解释了为什么《莱顿宣言》会强调形式化验证的重要性：只有可数学证明的约束，才能为不可预测的生成过程套上可信的缰绳。

AI代码的未来：恐慌会平息还是走向更深困境？

对于AI代码引发的普遍焦虑，社区里存在两种截然不同的历史观。

乐观派：技术成熟的必经阵痛

一部分人持历史循环的乐观态度：

"AI之所以是当下的热门话题，是因为它新、强大且不可靠。现在的一切都是实验性的，未来不可预测。但历史告诉我们，随着系统成熟、变得熟悉，恐慌与末日宣言都会平息。现在就像电力、飞机刚出现的时代。有一天你会说：我当时就在场。"

这种观点把AI视为又一次典型的技术革命——初期伴随恐惧与混乱，最终归于日常。

悲观派：编程知识失传与权力失控

另一些声音则要黑暗得多。有人担忧编程知识本身会随着可视化编辑器的普及而逐渐失传——就像工厂工作从高薪高地位岗位逐步被自动化取代、沦为最低工资的岗位一样，ICT行业也可能走上同样的路径。当越来越多的人依赖"翻译成真实代码"的可视化工具，原始编程能力（raw coding）正在悄悄流失。

这一担忧与劳动经济学中的"去技能化"（deskilling）理论高度吻合。这一概念最早由社会学家哈里·布雷弗曼（Harry Braverman）在1974年的著作《劳动与垄断资本》中系统阐述：技术进步往往将复杂的手工技艺分解为简单的标准化步骤，使原本需要高度专业知识的工作变得可由低技能劳动者完成。在软件行业，这一趋势已有迹可循——从汇编到高级语言、从手写SQL到ORM框架、从手动部署到一键CI/CD，每一层抽象都降低了入门门槛，同时也让开发者距离底层运作更远。低代码/无代码平台（如Salesforce、OutSystems）的兴起更是将这一趋势推向极致。AI代码生成可能代表这条去技能化链条上最激进的一步：当自然语言成为主要的编程接口时，理解程序执行语义的需求可能急剧下降。

更极端的设想认为，在遥远的未来，编程甚至可能因其"改变一切的力量"而被视为危险的"巫术"、被立法禁止——因为在一个高度依赖网络、甚至脑机接口的赛博世界里，掌握代码的人拥有过于集中的权力。

而最令人不安的一句话，来自讨论的结尾：

"或者更糟：当最后一个试图理解机器所造之物的人类老死，再也没有人能读懂它们时，会发生什么？"

结语：数学作为信任的地基

这场讨论从一份数学宣言出发，最终触及了一个远超技术本身的命题：在一个我们越来越无法完整理解的系统里，我们该如何维持信任？

答案或许并不在于要求每个人都读懂每一行代码——那从来就没实现过。真正的出路，正如《莱顿宣言》相关讨论所指向的，是建立可验证的基础设施：用形式化方法和数学证明，为不可预测的AI输出提供可信的边界。

我们不需要理解代码的每个细节，但我们需要能够证明它不会做我们不希望它做的事。当世界运行在无人能懂的代码上时，唯一能救我们的，可能不是更多的理解，而是更严格的验证。这也正是形式化方法从小众学术领域走向产业必需品的历史性时刻——从Lean数学库的蓬勃发展，到AWS使用TLA+验证分布式系统设计，再到微软将形式化验证融入Windows内核开发，种种迹象表明，"数学作为信任的地基"正从理念走向现实。