AI智能体时代的形式化方法
LLM越来越多地被用于代码生成，而研究人员也警告说，它们的输出往往看起来正确，但遗漏了功能需求。这使得正确性、可审计性和策略合规性变得更加——而不是更少——有价值。
因为AI让代码容易生成但难以信任，我们需要验证和可证明性。
- 可证明性回答："这个系统在重要属性上是否正确？"
- 可验证性回答："其他人能否独立检查这个声明？"
- 在智能体编码中，主要风险是看似合理但错误的软件。证明、测试、模型检查、运行时监控器和审计跟踪将快速代码生成转变为可信赖的工程。
当代码变得廉价时，保证变得有价值。
1、AI时代的可证明和可验证软件
想想你每天依赖的软件——我说的不是流媒体应用崩溃或浏览器冻结。
想想当您在70英里时速猛踩刹车时，汽车防抱死系统中运行的代码。或者想想锁定持有公司全部流动性的智能合约的加密算法。或者甚至医疗设备，比如连续血糖监测仪中控制精确胰岛素微剂量的固件。
那么问题是，我们如何实际知道——毫无疑问——当生命或数十亿美元处于风险中时，这些系统不会失败？
因为你不能再依赖一个工程师团队在发布前运行几千个单位测试。我们需要绝对的数学确定性，这是一个巨大的工程障碍。
历史上，科技行业依靠测试来发现bug。你编写代码，抛出一堆边界情况场景，如果通过，就发布。这是"快速行动，打破东西"的旧口号。但测试只能证明bug的存在；它永远不能证明它们的不存在。对于高风险环境，这种范式已经完全消亡。你不能再问"这段代码在我们的测试套件中有效吗？"你必须问"你能产生可机器检查、数学上合理的证据，证明这段代码将始终执行其预期规范，无论输入如何吗？"
AI现在正在积极编写——在许多情况下运行——惊人数量的代码。我们在生态系统中引入了一个巨大的速度乘数，而速度传统上是彻底验证的敌人。
有趣的是AI在这个领域中的双重性质。
它同时是软件保证的最大威胁和实现它的最有前途的工具。这是一个完全的悖论。
2、AI作为验证目标
首先让我们看看AI作为验证目标。我们越来越多地将神经网络——比如自主系统的学习控制器——直接放入关键基础设施中。
这很可怕。传统软件程序只是一系列逻辑分支；如果A，那么B。人类可以阅读和跟踪它。但神经网络只是一个包含数十亿权重、偏差和高维矩阵乘法的黑盒子。你无法仅仅阅读代码来查看它的作用。"代码"本质上只是对概率做出反应的数学。
那么你如何证明概率是安全的？
你必须在那个高维空间中映射边界。重点完全转移到证明两件事：鲁棒性和可达性。
鲁棒性提出一个数学问题。假设你获取一个输入，比如自动驾驶汽车摄像头看到的停车标志，你以难以察觉的分数扰动像素——人类甚至不会注意到的噪音。神经网络的输出是否会急剧失败并将其分类为限速标志？如果是，它就不鲁棒。
可达性分析，另一方面，使用复杂几何来计算系统状态空间的绝对极限。它保证系统永远不会达到不安全状态，无论向矩阵中输入什么对抗性输入。
3、AI作为助手（以及供应链风险）
如果验证AI大脑本身如此紧张，那么当同一个AI实际上在编写传统代码时会发生什么？
这是悖论的第二部分。
如果大型语言模型突然比人类工程师快一百倍地生成代码，仅仅数量就会破坏我们当前的审计方法。这就像雇佣一个超快的建筑队来建造摩天大楼。他们以闪电般的速度工作，但他们偶尔试图使用彩绘纸板而不是钢梁。因为纸板在数学上看起来像钢，他们的模式匹配算法，我们的建筑检查员（我们的验证方法）需要一个全新的框架来在浇筑混凝土之前捕捉那个纸板。
这种令人难以置信的速度呈指数级放大了供应链风险。AI助手通过从互联网上快速拉取开源库、依赖项和代码片段来编写代码。受损代码的攻击面变得巨大。那个"纸板梁"可能是恶意行为者故意滑入供应链的。
这就是为什么溯源框架不再是可选的。
我们谈论的是像SLSA（软件工件的供应链级别）和SBOM（软件物料清单）这样的框架。这些不仅仅是简单的检查清单或自述文件。它们是加密签名的证明。每次编译代码时，系统都会对使用的编译器的确切版本、导入的特定库和确切的构建环境进行哈希处理。它创建了一个不间断的、加密的监管链，这样你就知道每件东西来自哪里。
监管机构和企业买家将此视为绝对最低基线。如果你无法加密证明每个字节的确切来源，没有人会开始讨论代码本身是否在数学上合理。
4、证据光谱
假设我们的加密供应链已锁定，我们仍然必须证明代码实际上做了它应该做的事情。
让我们看看我们的"建筑检查员"使用的实际工具。有一个完整的验证分类法，称为"证据光谱"，这些工具的严格程度差异很大。
最顶层是交互式定理证明和SMT（可满足性模理论）求解器——名字像Roc、Lean 4和CVC5。定理证明听起来像黑板上的数学家，但我们谈论的是数百万行代码。SMT求解器的作用是将软件简化为纯代数逻辑。想象将代码中的函数翻译成一个巨大的、高度复杂的布尔方程。这是纯数学。
然后求解器使用重型算法启发式来尝试找到单个变量赋值——单组输入——会使方程为假（表示bug或违反规范）。如果求解器穷尽地证明公式不可满足，意味着它找不到破坏它的任何方法，那么没有输入组合能够违反规范。你得到一个字面数学证明，证明你的代码在功能上是正确的。
大的问题是什么？这要求你首先编写一个完美严格的数学规范。你必须将人类意图翻译成代数。对于大规模、高度并发的系统，如操作系统，SMT求解器会因无限复杂性而崩溃。
这个限制将我们带到下一层：模型检查，使用TLA+或nuXmv等工具。定理证明试图数学上解决代码本身，模型检查探索系统设计的状态空间。如果定理证明像为迷宫的物理编写数学证明，模型检查就是暴力破解迷宫本身——运行计算机沿着每个可能的走廊，确保没有死胡同。像TLA+这样的系统查看系统架构的离散数学模型，以找到基本逻辑缺陷，比如竞态条件，甚至在编写一行代码之前。
然后是加密可验证计算，比如zkVM（零知识虚拟机）。它们证明执行完整性。如果你发送一个大型数据集到第三方服务器运行复杂算法，zkVM执行代码的同时生成执行的加密跟踪——数学收据。"零知识"方面意味着你可以数学上验证这个收据，而服务器永远不必透露底层专有数据。你证明执行完美发生，同时完全保密输入。
5、分层保证和运行时安全
即使有了所有这些数学保证完美，当今的总体姿态是"分层保证"，这严重涉及"运行时保证"。
建立运行时监控器不是承认失败；而是承认现实。你根本无法形式化验证现代动态系统的每个组件，特别是在处理AI与混乱现实世界交互的概率性质时。
分层保证是关于务实的风险管理。你对小型关键安全内核使用交互式定理证明，对系统架构使用模型检查，对大规模复杂AI控制器使用架构遏制（运行时保证）。
看看NASA兰利关于自主无人机的高风险案例研究。他们想使用先进、未经验证的AI来驾驶飞机。你不能仅仅信任一个黑盒AI。所以，NASA使用了一个称为Simplex的运行时保证架构。
在Simplex中，未经验证的AI充当主控制器，因为它在优化路径方面很棒。然而，与之并行运行的是一个内部监控器和一个高度简化的、经过形式化验证的备用控制器。这就像学生驾驶汽车。AI是处理方向盘的青少年，运行时保证监控器是带有辅助刹车踏板的驾驶教练。如果AI跨越硬数学边界，教练会猛踩刹车并接管。真正的工程挑战是使用形式化定理证明来数学推导无人机传感器需要多快采样数据，以便"教练"能够在无人机物理学变得不可恢复之前做出反应。
我们在医疗设备中看到了同样的严谨性。对于自主人工胰腺系统，研究人员没有测试到安全。他们将整个系统的设计图转换为nuXmv的形式化状态模型，编写了132个从临床安全要求派生的形式化规范。很早，模型检查器就发现了一个人工审查者完全遗漏的不一致性。数学在构建任何硬件之前就捕获了一个基本设计缺陷。
在金融领域，智能合约中的单个逻辑错误可以不可逆转地抽取数十亿美元。形式化验证工具如Certora Prover现在是绝对基线。审计员编写"经济不变量"——无论代码走什么路径都必须保持为真的属性。SMT求解器试图找到任何打破不变量的奇怪数学漏洞。如果它们失败，机构就有数学证明，流动性池是安全的。
6、规范瓶颈
如果我们有这个令人难以置信的工具库，为什么不是每个关键软件都经过完美验证？
这又回到了人为因素。巨大的瓶颈不是处理能力；而是规范。验证工具非常字面。它们检查代码是否与你编写的规范匹配。但如果规范与人类工程师实际想要构建的不匹配呢？
微软研究院称之为"意图形式化问题"。人类意图是混乱、模糊和依赖上下文的。将人类愿望完美地翻译成严格的数学逻辑是极其困难的。
把它想象成神话中的灯神。问题几乎从来不是灯神（经过验证的代码）没有实现你的愿望。问题是人类的愿望是模糊的，灯神执行你规范的字面、数学精确性。你要一百万美元，灯神就用一堆便士压垮你。代码根据规范完美运行；规范只是致命的缺陷。
为了解决这个问题，有一个巨大的推动力使用AI来弥合人类意图和形式化数学之间的差距。像LioDojo和Apollo这样的智能体框架使用"验证器引导修复"。LLM编写数学规范草稿，将其馈送给严格的验证器，验证器不可避免地发现逻辑错误并将其反馈给LLM。这是AI的创造性引擎和验证器的严格真理引擎之间的持续、高速对话。
但有一个逻辑陷阱：如果我们依赖LLM——我们知道它们会产生幻觉——来编写我们的基础规范，我们是否只是将幻觉问题向左移动了一步？你可能有100%的数学保证，代码与规范匹配，但如果AI在规范本身中注入了一个微妙缺陷，整个基础就会受到损害。
为了缓解这一点，你必须要求完全独立于AI的可检查证据工件。你不能信任黑盒LLM，你也不应该盲目信任大型SMT求解器，因为求解器也是软件。这就是为什么行业正在转向像CVC5这样导出逐步数学证明的工具。你获取该证明并将其馈送到一个高度可信的、极其小型的软件中，称为内核，人类可以手动审计。除非它提供可独立审计的加密或数学收据，否则什么都不要信任。
7、重新定义确定性
无论你是评估企业工具的项目经理、设计新系统的工程师，还是只是在数字世界中导航的人，"保证"不再只是测试电子表格上的一个复选框。
今天唯一可辩护的工程姿态是分层保证矩阵。你使用模型检查来捕获架构缺陷，对关键安全组件使用SMT求解器，对不可预测的AI模型使用运行时保证安全包络，使用加密SBOM来证明供应链完整性。这是一个相互锁定的信任生态系统。
这里的要点是停止要求特定测试工具。技术发展太快。相反，要求可接受的证据工件。要求看到形式化模型、导出的数学证明、运行时反应计算和加密哈希。专注于不可辩驳的证据。
但有一个深刻令人清醒的最终想法。我们正在走向一个未来，人类工程师无法完全理解运行我们关键系统的AI生成代码，他们也无法完全理解机器生成的用于验证该代码的大量数学证明。
在什么时候，人类理解成为我们技术中真理和信任的实际瓶颈？数学可能是完美的，但我们理解它的生物学能力正撞上一堵墙。当代码是一个黑盒，验证它的数学对人类思维来说过于庞大时，我们必须从根本上重新定义确定性的含义。
原文链接: Formal Methods in the Agentic AI Era: A Strategic Agenda for High-Assurance Software
汇智网翻译整理，转载请标明出处