💻 computer science

The Machine Proposes. The Proof Disposes: Neuro-Symbolic Synthesis of Formally Verified Markov Usage Models from Natural Language Requirements

本文介绍了神经符号 MBST，这是一个通过集成 L* 学习、语法约束的大语言模型以及凸优化，将自然语言需求自动合成形式化验证的马尔可夫使用模型，从而实现高保真故障检测与覆盖率，在显著超越纯神经基准模型的同时，消除了安全关键系统中人工建模瓶颈的框架。

原作者： Nathan Ginting

发布于 2026-07-28

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Nathan Ginting

原始论文采用 CC BY 4.0 许可（https://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你正在试图教一个机器人如何驾驶汽车或浏览网站。为了做到这一点，你需要一张包含机器人所有可能动作的地图。在软件测试领域，这张图被称为“使用模型”（usage model）。它就像一张流程图，展示了系统可能处于的所有状态（例如“正在刹车”或“购物车已满”）以及从一个状态转移到另一个状态的概率（例如“用户点击‘购买’的概率为 80%”）。

几十年来，专家们一直使用这些地图来进行“统计测试”。统计测试不仅仅是检查代码是否运行一次成功，而是利用这张地图模拟成千上万次在系统中的随机旅程。如果地图是准确的，这些测试就能发现那些只在罕见、棘手情况下才会出现的隐藏漏洞（bugs）。然而，这里有一个巨大的问题：手工绘制这些地图既慢又枯燥，而且容易出现人为错误。这就像是在蒙着眼睛尝试绘制一整座城市的详细地图。最近，我们有了一个新工具：人工智能（AI），它可以阅读文本并猜测地图应该是什么样子的。但问题在于：AI 擅长猜测地图的“形状”，却不擅长把“数字”搞对。它可能会画出一条并不存在的路，或者说降水概率是 150%（这在现实中是不可能的）。这篇论文探讨的是：我们能否将 AI 的创造力与严格的数学“规则手册”结合起来，从而自动构建出一张完美的地图？

这篇题为《机器提议，证明处置》（The Machine Proposes. The Proof Disposes）的论文介绍了一种名为 NeSy-MBST 的新系统。你可以把它想象成一个创意作家与一位严厉数学老师的搭档。这个“作家”是一个大语言模型（LLM），它通过阅读自然语言需求（例如“用户应该能够将物品添加到购物车”）来起草一份系统地图的草案。而“数学老师”是一个符号求解器（symbolic solver），这是一个用于检查草案是否符合数学规律的计算机程序。

以下是这个团队是如何协作的：

提议（The Proposal）： AI 阅读需求并勾勒出状态和转换路径。它速度很快，且能很好地理解人类语言。
证明（The Proof）： 数学老师立即检查这份草图。AI 是否发明了一个物理上不可能存在的转换？它是否遗漏了某个步骤？老师会说：“不，那条路不存在，”或者“你漏掉了一个转弯。”
修正（The Fix）： AI 接收反馈，修正地图，然后再次尝试。
数字（The Numbers）： 一旦地图的形状完美无缺，数学老师就会接管并分配概率。与其让 AI 去瞎猜数字（这通常会导致错误），老师会使用“凸优化器”（convex optimizer）来精确计算概率，确保它们正确地加总为 100%，并反映真实的实际使用情况。

研究人员在两种类型的挑战上测试了这个系统：一辆自动驾驶汽车（自动驾驶汽车系统）和两个电子商务网站（一个用户购物页面和一个管理后台）。他们将这种全新的“搭档”系统与仅使用 AI 以及传统的纯人工方法进行了对比。

结果令人印象深刻。当仅使用 AI 时，系统会遗漏大约一半的重要路径，并在地图结构上出错。但通过 NeSy-MBST 这一组合，系统的得分达到了 0.9125，而在对于自动驾驶汽车等关键系统而言，0.90 是必须达到的安全阈值。这意味着仅靠 AI 是不够好的，但通过这种“搭档”模式则通过了安全测试。

具体而言，新系统成功覆盖了 85.7% 的可能转换（即系统可以采取的路径），而仅使用 AI 的版本仅覆盖了 50%。这是一个巨大的 35.7 个百分点 的增幅。用通俗的话说，新系统找到了更多样化的潜在漏洞，因为它不会像单纯的 AI 那样产生“死胡同”或“不存在的道路”等幻觉。

论文还研究了该系统在处理数字方面的表现。它使用了名为 Jensen–Shannon 散度（Jensen–Shannon divergence）的指标来衡量 AI 的概率猜测与真实数学值之间的接近程度。新系统的得分达到了 0.012，极其接近完美，而仅使用 AI 的版本则远在 0.157 之外。这证明了数学老师成功修正了 AI 的错误数学。

研究人员还进行了一项名为“消融实验”（ablation study）的特别实验，以观察团队中哪个部分承担了主要工作。他们发现，符号验证循环（即检查地图结构的数学老师）是系统找到更多路径的主要原因。而凸优化器（即进行概率计算的数学老师）则是数字如此准确的主要原因。闭环反馈（即系统通过运行测试进行学习）也有一定的帮助，但核心的魔力在于最初的这种“搭档”协作。

总之，这篇论文表明，我们不必在 AI 的速度和人类专家的安全性之间做选择。通过让 AI 提出想法，并由严格的数学系统进行验证和纠正，我们可以构建出既能快速创建又足以应对关键系统的软件测试地图。作者指出，虽然这在他们测试的系统（高达 42 个状态）中表现出色，但仍需更多研究来观察其是否能扩展到大规模、复杂的工业级系统。但就目前而言，他们已经证明了“机器提议”是一个伟大的开始，只要在最终使用地图之前，由“证明处置”掉其中的任何错误即可。

技术摘要：神经-符号合成形式化验证的马尔可夫使用模型

1. 问题陈述

阻碍基于模型的统计测试（MBST）广泛应用于安全关键领域之外的主要瓶颈，是马尔可夫链使用模型的人工构建过程。这些模型对于将测试目标从绝对代码覆盖率转向关于预期现场质量的统计推断至关重要。然而，将模糊、非结构化的自然语言需求转化为经过验证的状态转移拓扑结构和数学一致的概率矩阵，需要深厚的形式化方法专业知识。

虽然大语言模型（LLMs）已展示出语法提取能力，但纯神经方法在应用于 MBST 时存在四个关键局限性：

随机波动与幻觉： LLMs 可能会遗漏关键边缘情况、构建不可能的转移或违反系统不变性，从而导致无效的测试用例。
校准失败： LLMs 在精确数值推理方面表现不佳，通常无法满足严格的行随机约束（ $\sum_j p_{ij} = 1$ ）以及有效的马尔可夫链所需的复杂多变量约束。
状态空间爆炸： 在有限上下文窗口内运行的 LLMs 无法有效地跟踪或生成高度并发、多流的转移模型，否则会丢失结构连贯性。
语义-可行性偏差： LLMs 擅长语义进展，但经常违反物理和逻辑可行性约束（例如，在购物车为空的情况下执行结账转移），从而生成在语义上逻辑通顺但在物理上无法执行的路径。

现有文献缺乏关于自动化模型构建是否能保持 MBST 故障检测保证所需的结构和概率属性的端到端评估。

2. 方法论：NeSy-MBST 框架

本文引入了神经-符号模型基于统计测试（NeSy-MBST），这是一个将语义解析与数学约束求解解耦的混合框架。该架构集成了五个紧密耦合的阶段：

A. 进度-可行性双记忆架构

系统将模型构建划分为两个互补的记忆系统：

神经进度记忆： 微调后的 LLM 解析自然语言需求，以起草语义流图（“做什么”），捕捉预期的行为拓扑结构。
符号可行性记忆： 基于规则的引擎强制执行严格的逻辑不变性、前置条件和转移守卫（“怎么做”），在准入前验证每一个候选转移。

B. 通过 $L^*$ 与 LLM Oracle 进行的主动自动机学习

该框架采用了一种专门的 $L^*$ 主动自动机学习算法变体来发现状态空间。

成员查询（Membership Queries）： 算法查询一个受语法约束的 LLM Oracle（其输出被限制为：是、否、不确定），以确定候选输入序列是否被接受。
等价查询（Equivalence Queries）： 当前的假设自动机通过对实际被测系统（SUT）进行测试。差异产生的反例被用于精炼假设。
升级机制（Escalation）： 如果 LLM 返回“不确定”，则将查询升级至人类专家或 SUT 运行时执行，确保学习循环永远不会纳入未经验证的信息。

C. 路径依赖的分层建模

为了解决路径依赖问题而不引起组合爆炸，NeSy-MBST 使用了两层分层结构：

上层树状结构： 频繁的、路径依赖的序列被建模为嵌入在树中的高阶马尔可夫链。
下层马尔可夫模型： 不频繁或异常的路径使用标准的阶马尔可夫链进行建模。

D. 数学约束优化

框架并非要求 LLM 直接生成数值概率，而是将此任务交给符号求解器：

约束提取： LLM 从需求中提取比较关系（例如， $P(\text{checkout}|\text{cart}) > P(\text{browse}|\text{cart})$ ）。
凸优化： 凸规划引擎（SLSQP）求解转移概率矩阵 $P$ ，使其满足提取的所有约束、行随机性以及领域特定的边界，同时最大化熵以避免无理偏见。

E. 闭环模型自适应

该框架将使用模型视为一种动态产物。运行时遥测数据（执行日志、覆盖率指标、故障数据）被反馈到建模引擎。LLM 分析预测行为与观察行为之间的差异，并由符号求解器重新校准概率，确保模型向真实世界的使用模式收敛。

3. 核心贡献

NeSy-MBST 框架： 一种结合了 $L^*$ 主动学习、语法约束 LLM Oracle、符号求解器和闭环反馈的创新架构，用于自动化使用模型合成。
LLM 输出的形式化验证： 引入了一个符号验证循环，用于检测结构违规（不可达状态、缺失自环）并触发有针对性的重新提示，从而将受限于召回率的生成问题转化为由验证引导的补全问题。
误差的正交分解： 本文确立了结构完整性（拓扑）和概率校准（权重）是正交属性，分别由符号循环和凸优化器处理。
实证验证： 在自动驾驶汽车（AV）CPS 基准测试和两个电子商务规范上进行了全面评估，并将 NeSy-MBST 与纯神经基线和传统的各种人工方法进行了对比。

4. 实验结果

在 AV CPS 基准测试（9 个状态，13 个转移）和电子商务模型（高达 42 个状态，218 个转移）上进行的评估显示，NeSy-MBST 实现了以下目标：

提取准确度 (RQ1)： 实现了 0.9125 的系统级 F1 分数，超过了 0.90 的安全关键阈值。这比表现最好的 GPT-4o 基线（Hybrid SMF）提升了 39.1%，比最强的单模型基线（Claude 3.5 Sonnet）提升了 14.8%。
故障检测覆盖率 (RQ2)： 实现了 85.7% 的转移覆盖率，比纯神经基线（50%）高出 35.7 个百分点。这表明故障揭示路径的多样性显著增加。
概率校准 (RQ3)： 实现了 0.012 的 Jensen–Shannon 散度 (JSD)（相比之下，纯神经基线为 0.157），证实了凸优化器保留了操作测试分配的保真度。归一化 Frobenius 距离为 0.0654，表明其与参考分布具有高度的结构相似性。
效率： 对于包含多达 42 个状态的模型，在不到 六分钟 内即可生成完整的模型覆盖测试套件。
消融研究 (RQ4)：
- 符号循环 被确定为结构完整性的主要驱动力（将转移 F1 从 0.78 提高到 0.96）。
- 凸优化器 被证明在不改变结构指标的情况下控制概率校准。
- 闭环反馈 对分布保真度提供了边际改进，主要在长期测试活动中具有价值。

5. 意义与主张

本文声称 NeSy-MBST 消除了手动建模的瓶颈，且没有损害安全关键网络物理系统（CPS）所要求的统计严谨性。

弥合差距： 结果表明，神经-符号集成可以实现 MBST 所需的结构保真度（F1 $\ge$ 0.90）和概率校准，而纯神经方法无法保证这一点。
故障检测代理： 虽然本研究并未针对注入故障的语料库测量直接的缺陷检测率，但论文认为，观察到的 35.7% 转移覆盖率增益 是一个强有力的故障检测代理，这与工业级 MBT 部署文献中报告的 25–40% 的提升是一致的。
工程标准： 作者提出，LLM 增强形式化测试模型生成应从研究好奇心转变为标准工程实践，前提是满足两个条件：(1) LLM 必须在结构约束下运行（语法约束输出、符号验证）以防止幻觉；(2) 数值参数应由经过认证的求解器而非 LLM 直接分配。

论文总结道，这种方法使严谨的统计测试变得更加易于获取，使其能够超越专业的安全关键团队，走向更广泛的软件开发实践，同时也承认未来需要在更大规模的工业系统和多样化的需求风格上验证这些发现。