做AI项目的人十有八九都有过这种体验模型在测试集上跑得漂漂亮亮一上真实环境就被几个刁钻样本打回原形。我见过一个视觉检测团队把测试集从两万张加到了五万张某个阴雨场景下的准确率依旧在60%附近晃荡。为什么因为测试的本质是抽样你永远只能“希望”没有漏掉更隐蔽的情况。而形式化方法Formal Methods走的是另一条路——它不靠抽样而是试图用数学证明的方式告诉你说这个系统在给定假设下一定满足某个性质。这篇我特别想聊聊当这种“证明式验证”遇上以统计规律为核心的人工智能Artificial Intelligence到底会发生什么化学反应又有哪些地方是真能落地的。写这篇文章的另一个原因是我发现身边搞AI的工程师和做形式化验证的老派程序员经常互相看不上。做AI的觉得形式化那套东西“太慢、太严格、根本规模化不了”做形式化的人觉得AI“不可解释、无法保证、就是个黑盒”。但这两年我实际做下来两者非但不矛盾反而能把对方最大的短板补上。这篇文章不打算写成教科书式科普只讲我真实接触过的场景、踩过的坑以及那些值得你亲自试一次的技术路线。1. 形式化方法究竟在“验证”什么——先把它跟测试彻底分开1.1 形式化方法的完整套路规范、建模、证明形式化方法的第一课是把“测试”和“验证”这两件事从根上区分开。常规测试是给系统喂一组输入看输出是否符合预期。它管用的前提是你喂进去的输入有代表性。但问题是真实世界的输入空间往往大到不可能全部采样。而形式化方法是三段式结构先写一份精确到没有歧义的规范specification然后给被验证对象建一个数学模型最后用逻辑推理手段证明“这个模型满足那条规范”。我给你一个最直观的例子。假设你要给一个网络缓冲区写安全性质自然语言是“缓冲区长度不能超过16”。这句话看起来清楚但严格意义上有歧义——是任何时候都不能超过还是只在某个操作期间不能超过形式化规范会把它写成类似下面这样的逻辑property buffer_size_max: always (len(buffer) 16)这里的always是时序逻辑算子表示“在所有可达状态下都成立”。写清楚之后验证工具要做的就是在系统模型里遍历所有可达状态逐一确认这个条件没有被违反。这和写测试用例完全不是一个思路测试用例描述的是“某个具体输入下输出应该是什么”形式化规范描述的却是“所有可能的运行状态里系统不能违反什么”。这也解释了为什么很多团队第一次接触形式化方法时极度不适应。做测试的时候你是在“设计例子”做形式化验证的时候你是在“定义真理”。想把模糊的需求翻译成数学语言远比想象中耗时。法国原子能委员会用Frama-C做嵌入式C代码验证时一个核心原则就是规范占整个验证工作量的七成。这个比例我没有精确考证过但亲身体会告诉我规范阶段确实是整个流程里最烧脑、也最能暴露需求漏洞的部分。1.2 模型检测与定理证明两条流派分别解决什么问题形式化方法内部有两个主要流派刚接触的人特别容易搞混。一个是模型检测Model Checking思路是自动遍历系统所有可达状态检查安全性质是否成立。它的优点是全自动写完模型和规范工具自己去搜缺点是著名的“状态空间爆炸”——系统稍微复杂点状态数就指数增长算到天荒地老也跑不完。经典工具包括SPIN、NuSMV、TLA Toolbox适合验证通信协议、并发系统、状态机这类离散模型。另一个流派是定理证明Theorem Proving把系统和性质编码进逻辑系统用人机交互的方式一步步推导出结论。代表工具有Coq、Isabelle/HOL、Lean、Why3。它能对付无限状态空间因为你可以在逻辑层面做归纳、抽象代价是证明过程极其依赖人的专业能力自动化程度低常常一个不复杂的程序也要写上千行证明脚本。打个比方模型检测是派一群人把整个迷宫每一格都走一遍定理证明是请一位数学家在黑板上论证“迷宫里绝对不存在某个出口”。但两者有个共同的底线结论由推理规则保证而不是由运行样本保证。这点在任何工程讨论里都必须最先明确。2014年亚马逊工程师公开发过一篇关于他们用TLA验证DynamoDB内部协议的文章他们用模型检测发现了多个真实存在的深层bug而这些bug在长时间运行和压测中都没有暴露。这个案例让我印象很深——不是因为它多炫技而是它证明了对大公司来说某些bug一旦线上爆发代价远远高于前期做形式化验证的成本。2. 为什么深度学习让形式化方法“无从下嘴”——AI给验证带来的新难题2.1 对抗样本揭示的真相决策边界比想象中狰狞得多在讨论AI验证时最常见的误区是“我把测试集做得够大网络肯定就可靠了。”对抗样本Adversarial Examples研究把这种幻想彻底击碎了。你在一张被正确识别为熊猫的图片上叠加一层人眼几乎不可见的微小噪声模型就会以极高置信度把它识别成长臂猿。公开实验里有一个反复出现的现象一个在CIFAR-10上准确率超过90%的分类器面对用梯度方法生成的、扰动幅度只有0.03左右的输入时整体准确率会暴跌到不足50%。这个现象在形式化验证语境下意味着什么意味着神经网络的决策边界不是那种“大部分区域平滑只有角落有点毛刺”的形状而是像一个极高维空间里的复杂褶皱。坏点不是孤立地藏在某一两个角落而是渗透在大量看似正常的输入附近。你采样一万个点可能一个坏点都碰不到但如果你想证明“这附近所有点都安全”那就等于要面对一个无穷集合。更令人头痛的是深度学习模型的高维输入空间里体积大部分集中在边界附近这让“穷举式测试”显得格外苍白。2.2 神经网络是个“异形软件”没有状态机、没有显式控制流传统软件和神经网络在结构上的差异是形式化方法在AI面前失语的另一个原因。传统软件有明确的变量、函数调用、循环和控制流这些都能映射成状态转移系统模型检测可以直接套用。而神经网络本质上是一长串矩阵乘法和非线性激活函数的复合它没有显式的if-else分支没有状态变量没有值得枚举的“状态”。一个残差网络有上千万甚至上亿参数你既没法把它展开成有限状态机也没法用传统的程序分析手段去抽象它。更麻烦的是激活函数引入的分段线性结构。一个含 k 个ReLU神经元的网络在输入空间中最多可以形成 2^k 个线性区域。k20时已经超过一百万k100时这个数字已经大到超出任何穷举的可能。所以你会发现传统形式化工具里的“搜索所有路径”策略在神经网络面前完全失效——因为网络里的线性区域数量本身就是天文数字。2.3 连“要证明什么”都还没谈拢规范层面的危机还有一个比算法更难的问题很多AI系统压根说不清楚“正确”和“安全”的数学定义。对核反应堆你可以写“堆芯温度永远低于某阈值”对数据库协议你可以写“两个客户端不会同时获得同一把锁”。但“自动驾驶行为安全”对应什么数学命题是“永远不压线”吗可是为了避让行人必须压线怎么办是“跟前车距离始终大于2米”吗那如果后车跟得很近急刹反而会导致追尾呢这些歧义不是形式化方法能自动解决的。形式化方法要求把规范写死但AI系统的很多能力特性公平性、可解释性、与人类价值观对齐本身就缺乏公认的数学定义。所以你经常遇到的情况是不是验证器不够强而是你根本不知道该把哪条性质交给它。这也解释了为什么目前AI形式化验证领域里最多的工作集中在“鲁棒性”这种数学定义相对清晰的性质上——至少它把“对抗样本是否会对模型造成影响”这个问题变成了一个严格的数学命题。3. 反向冲击AI开始反过来给形式化方法当“加速器”3.1 让大模型当证明助手Lean、Coq 里的“copilot”模式很多人不知道的是形式化方法自身也在被AI改变。最明显的方向是交互式定理证明。以前用Coq或Lean证明一个数学定理需要人手动输入每一步tactic——也就是告诉证明器下一步该用什么规则。这个过程非常慢既考验数学功底又考验对证明器内部机制的记忆。现在的主流研究思路是把当前要证明的目标goal和上下文翻译成文本喂给大语言模型让模型预测一个tactic比如induction n或exact mul_comm _ _。然后证明引擎验证这个tactic合不合法合法就推进状态不合法就再换一个。在Mathlib和MiniF2F这类形式化数学基准上这几年AI的解题成功率从接近零涨到了两三成。单看数字觉得不高但要知道形式化证明对逻辑正确性的要求极其严格大模型做错一步就会被引擎毫不留情地打回。这种“人机协同”最实用的价值不是让AI独立写证明而是给你当“副驾”当你卡在某个子目标半小时没思路时让模型帮你猜一个可能的推理路径往往能带来启发。我用Lean做项目时经常这么干省下的查文档时间非常可观。3.2 用学习算法猜循环不变式自动解决验证里的“老大难”程序验证领域有个著名的痛点循环不变式loop invariant。在软件验证里要证明一个带循环的程序正确你得先找到一个性质它在循环每次迭代前后都成立循环结束后又能推导出最终结论。一个简单的例子是实现数组累加和的程序# 目标验证循环结束后 s sum(a) s 0 for i in range(len(a)): s a[i]要证明这个程序正确需要的不变式是s sum(a[:i]) and 0 i len(a)。看起来不难但真实项目里的循环逻辑复杂得多手工写不变式既费脑又容易漏。Code2Inv这类研究把机器学习引了进来先用图神经网络把程序结构编码成图然后训练模型去猜候选不变式再用Z3这样的SMT求解器去验证候选不变式是否成立。猜对了就通过猜错了求解器会返回一个反例模型再根据反例继续改。这个流程的本质是把“死记硬背的启发式搜索”换成了“从大量程序里学到的模式”。我实际跑过几个开源数据集上的实验这套方法确实能自动生成不少传统工具找不到的循环不变式。这个方向最值得借鉴的地方是它的角色分工AI负责生成和猜测验证器只负责终极审判。正因为有验证器兜底AI偶尔产生幻觉也无所谓因为错误提案会被直接拒绝不会污染最终结论。这也算是把AI的“不靠谱”控制在了一个安全范围内的典型做法。3.3 给SMT求解器装一个“策略大脑”SMT求解器比如Z3、CVC5是现代形式化验证的发动机但它们有个让普通用户抓狂的脾气同一个问题换个写法、调个参数求解效率天差地别。尤其是处理带量词的逻辑公式时什么时候该实例化哪个量词、选哪种模式都非常讲究调参体验不亚于玄学。机器学习正在逐步改善这个局面。已经有研究者用强化学习和监督学习根据公式的结构特征预测合适的求解策略比如选择量词实例化顺序、决定是否先做理论组合预处理等。对使用者来说意味着不再需要把时间花在理解求解器的内部黑魔法上。我自己用Z3跑带量词公式时试过手动调整启发式模式和让AI推荐策略两种方式后者在很多情况下更省心尤其当你不清楚Z3内部到底有哪些旋钮可拧时。4. 正向验证形式化方法如何给神经网络“上保险”4.1 鲁棒性验证的数学表述一个绕不开的全称量词现在聊更硬核的问题能不能直接拿形式化方法验证一个神经网络目前技术上最成熟、研究最密集的方向是“局部鲁棒性验证”。它的数学定义特别干净给定神经网络 f: R^n - {1, ..., K} 输入样本 x0扰动半径 epsilon通常按 L_inf 范数 验证目标对任意 x若 || x - x0 ||_inf epsilon则有 f(x) f(x0)翻译一下就是在以样本 x0 为中心、半径为 epsilon 的方盒子内所有输入都必须被分成同一个类别。注意那个“任意”——这意味着你不能抽样哪怕一百万个点而是要处理这个区域内的所有无穷多个点。这个性质一旦证明成功就表示你找到了一个以 x0 为中心的“安全气泡”模型在这个气泡内不会出错。多分类情况下验证器通常会把目标分解成若干个“logit差”问题对每个错误类别 c证明在扰动区域内“正确类别的logit始终大于类别c的logit”。这一下就把分类不确定性转化成了连续函数在紧集上的不等式验证传统优化和逻辑方法都能派上用场。4.2 区间传播与抽象解释把无穷输入折叠成一个盒子要处理“无穷个输入”最直观的思路是不要一个一个地看而是给所有输入一个整体表示。这就是抽象解释Abstract Interpretation和区间传播Interval Propagation的思路输入一个超立方体区间让它一层层经过线性层和ReLU最后得到输出区间的一个超近似。难点主要在ReLU激活函数。如果输入区间完全落在正半轴ReLU就是恒等变换很好处理如果完全落在负半轴它会变成零函数也好处理但很多区间是跨越0的ReLU会把一个区间“折”成两部分这时如果不想精确枚举就必须做过度近似over-approximation用一个更大的凸区域去包裹ReLU的输出牺牲一点精度换来计算可行性。市面上几个代表性工具就是这个思路的具体实现ERAN基于DeepPoly抽象能处理几百万神经元的网络并给出可用的鲁棒性边界Marabou则支持把ReLU逻辑编码成SMT公式通过求解器精确搜索反例。两者各有优缺点抽象解释快但可能误报说你不安全其实安全SMT精确但慢。需要坦白的是这类验证目前仍然只适用于相对小的网络和局部邻域对一个真实自动驾驶感知模型做大范围全局验证计算开销仍然高到不现实。但它已经足够用来做一件关键事情对核心安全场景里的具体样本证明一个可接受扰动范围内模型的决策不会被改变并且如果性质不成立求解器会直接给你找到一个实际反例输入。4.3 ACAS Xu真实航空系统里的深度学习验证要说这个领域的标志性案例绕不开ACAS Xu。它是飞机防撞系统的神经网络版本输入包括本机与入侵机的距离、相对航向、相对速度等5个连续维度输出是5种飞行建议动作比如“保持航向”“向上回避”“向下回避”等。工程上有几项要求非常明确的安全性质比如“当两机距离足够大时系统不应给出某个特定的危险动作”。研究者先用Reluplex一种SMT方案对这些网络做验证后来又迁移到Marabou上。这项工作成了教科书级的案例因为它第一次在航空安全语境下把神经网络从“用测试数据评估”提升到了“用数学证明来确认安全边界”的层面。更让我印象深刻的是它找反例的能力验证器如果发现某个性质不成立会直接输出一个具体的输入点让你清楚地看到模型在哪里失效。这种“机器自动设计攻击样本”的能力比传统人工构造测试用例效率高出好几个量级。我自己带团队复现类似流程时也验证过这个现象。起初大家都在手工构造对抗样本去试探模型忙活半天找不全换成SMT编码后反例是求解器一辆一辆“算”出来的整个过程完全不依赖人的灵感。5. 把两者焊在一起的三条工程路径安全护栏、运行时验证、分层设计5.1 安全护栏模式AI只提建议形式化逻辑做最后裁决对绝大多数实际工程来说指望“完整验证一个海量参数神经网络”短期内还不现实。但换个思路就有解让AI不直接控制执行器只负责给出意图在AI和执行器之间加一层经过形式化验证的“安全护栏”。这层护栏逻辑简单、状态少完全可以用模型检测或定理证明做全量验证。AI输出一旦越界护栏直接驳回或降级为保守策略。这个模式的精髓在于把验证目标从“证明神经网络没问题”转移到了“证明护栏逻辑没问题”。前者目前基本不可行后者完全可行。我在无人机避障项目里就采用过类似架构视觉模块用深度网络识别障碍物但最终的飞行动作必须经过一个预先验证过的“安全包络”逻辑检查只有通过检查的动作才允许下发。效果非常直接——系统没有因为模型误识别导致过安全事故。打个不恰当的比方这就像汽车里的保险丝。你不需要证明所有电器设备绝对不会短路只需要保证电流一旦过大保险丝一定熔断。把不可预测的组件蒙在可验证的安全边界里工程上才是理性的选择。5.2 运行时验证在运行中实时检查时序规范安全护栏是一种静态架构运行时验证则是在动态过程中持续把关。你可以把信号时序逻辑STL这类规范编译成一个监控器让它像看门狗一样盯着系统实时输出。比如无人车场景里规范可以是“目标车与前车距离永远大于2米”always (distance 2.0)更复杂一点的可以是“一旦检测到行人出现3秒内必须启动制动或转向避让”。这些时序性质可以直接写成STL公式然后运行时监控器在每个控制周期检查过去一段时间的轨迹是否满足公式。一旦发现即将违反就触发降级、告警或人工接管。这项技术的好处是部署成本低不需要改模型、不需要重训练直接在系统外面做一层“有数学依据的检查”。要注意的是监控器再可靠输入数据的质量问题依然存在。传感器噪声和丢帧可能导致规范误判所以要在公式里加入“输入有效”的前置条件让监控器在数据不可用时主动进入“无法判定”状态而不是强行给出一个错误结论。5.3 分层架构感知交给神经网络决策交给可验证的状态机第三种路径是我个人最看好的——把系统拆成分层结构神经网络只负责感知层面的工作比如目标检测、图像分割、语音识别决策层用一个显式规则引擎或状态机来完成。状态机的转移条件都是离散可枚举的可以被模型检测完整验证。这种架构下神经网络的输出不完全可信也没关系因为决策逻辑只依赖离散的、经过确认的事件。比如一个服务机器人感知层用深度学习识别桌面上的物体类别决策层则是一个状态机只有检测到“抓取目标存在”且“当前机械臂位姿安全”两个条件同时满足时才允许进入抓取状态。这些条件来源于感知输出但决策路径本身是形式化验证过的。这套架构的缺点是决策能力天然受限做不了端到端那种极度灵活的复杂行为优点是安全关键路径上获得了实实在在的可证明性。对安全要求高、任务模式相对固定的工业场景这是相当务实的“双轨制”。6. 从项目里总结的四个坑规范不清、复现性差、验证范围错位、盲目“全证明”6.1 踩坑一验证结果没法复现差点推翻整个交付结论不是吓唬你形式化验证工具本身也是个工程系统它同样有版本兼容、环境依赖问题。我遇到过的情况是同一个性质在公司服务器上用Z3 8.11验证通过换到我笔记本上的Z3 8.12就跑超时。更隐蔽的是某些SMT求解器在开启并行线程时可能给出不同的结果。如果验证结果不稳定那它在工程评审中就没有可信度。后来我定了一条规矩所有验证工具链都必须固化成Docker镜像镜像里精确锁定每个工具的版本号和编译参数验证脚本记录工具输出的哈希值。对关键结论还要用两套不同原理的验证工具交叉校验。宁可多花一倍机器时间也要保证“验证通过”这件事本身经得起推敲。6.2 踩坑二规范写得“太像人话”验证通过了却没达成安全目标形式化验证最隐蔽的失败模式不是算法跑不动而是规范本身定义错了。我参与过一个机械臂项目安全规范最初写成“机械臂不能离障碍物太近”。“太近”两个字描述起来很自然但没法验证。团队后来把“太近”定义成“欧氏距离小于0.1米”然后花大力气验证全绿。结果现场工程师马上就发现了问题在某个特殊姿态下机械臂的实际碰撞距离是0.08米比定义的安全距离更小但被手臂自身结构挡住了因为测量点在几何中心而不是在真实碰撞面。教训就是形式化验证能证明的永远只是你写下的那条数学命题。规范翻译过程中必须由懂现场、懂物理的一线工程师反复确认边界条件。最有效的办法是先故意让验证器找违反场景根据它生成的反例反过来审查规范本身是否合理再迭代修正。这个过程虽然费时但也是形式化方法倒逼团队把需求彻底想清楚的独特价值。6.3 踩坑三把验证当测试用又把测试当验证用我经常遇到团队问“你不是有形式化验证吗帮我测一下这个神经网络在所有可能输入下会不会崩。”这本质上还是抽样思维——他们想要的其实是一个更大规模的测试。反过来也有人跑了一百万个测试用例就觉得系统“安全了”可测试用例再多也无法覆盖全称量词约束下的无穷输入空间。更合理的使用姿势是让两者各司其职形式化验证覆盖那些“可精确定义、一旦违反就是事故”的安全性质统计测试覆盖那些“语义模糊、难以形式化”的用户体验和性能期望。安全边界用数学证明去锁死行为质量用大规模数据去打磨这样分工才符合现实。6.4 踩坑四试图“完全证明AI”忘了系统里其他不可控环节最后一个坑是心态问题。有段时间团队拿到几个漂亮的验证结果兴奋得恨不得宣称“系统绝对安全”。但仔细想想就知道验证范围只是整个系统中极小的一部分我们证明了感知网络在某个局部邻域内鲁棒但镜头脏了、系统延迟、执行器卡顿、网络丢包这些物理环节全都还没有纳入验证。你证明了数学层面的一条性质不等于证明了整车不会出事故。所以我在评审会上最喜欢追问的一句话是“这个验证 гарантирует 的到底是什么性质的成立”如果有人回答“保证系统安全”那就是在夸大。正确的表达应该是“保证‘模型在输入扰动不超过epsilon时分类不变’这条数学性质成立”。整个系统的安全永远要靠数学验证、实时监控、物理冗余、人工接管这些备份协同构建。形式化方法在其中负责它擅长的逻辑层面而不是扮演万能的安全之神。最后说一点自己的心得。这几年下来我越来越觉得AI和形式化方法的关系不是非此即彼而更像一支队伍里的侦察兵和工兵AI擅长在开放、模糊、高维的环境里发现模式和可能性形式化方法擅长在明确、关键、影响重大的边界上提供确定性。真正成熟的AI工程应该懂得把有限的形式化验证资源放在最昂贵、最致命、最容易用数学定义清楚的环节上而不是对每一个细节做无差别证明也不是对每一个风险都靠堆数据硬扛。如果你正在做安全攸关的AI系统可以从一个很小的约束开始尝试比如先挑一个你最担心的安全性质写成严谨的数学命题再用工具试试看能不能验证。多半到那时你才会发现最难的不是验证本身而是把心里那句“应该没问题吧”翻译成无懈可击的逻辑语言。