医疗设备软件安全新范式:LLM + SMT 求解器实现 98.5% 需求验证准确率

当大语言模型遇上形式化验证，自然语言软件需求的歧义与缺陷无处遁形。

近日，美国史蒂文斯理工学院（Stevens Institute of Technology）的研究团队在 arXiv 上发表了一项重要研究成果——VERIMED 神经符号框架，将大语言模型与 SMT 求解器相结合，为医疗设备软件需求的自动化审计开辟了全新路径。实验结果显示，该方法将需求验证准确率从 55.4% 大幅提升至98.5%。

研究背景：自然语言需求的"隐形杀手"

在软件开发中，尤其是安全关键领域（如医疗设备、航空航天、自动驾驶），自然语言软件需求往往存在三大顽疾：

1. 歧义性（Ambiguity）

同一段需求描述可能存在多种合理解读。例如："当血压超过阈值时触发警报"——阈值是多少？收缩压还是舒张压？"超过"是否包含等于？

2. 不一致性（Inconsistency）

需求集合内部可能相互矛盾，导致无法同时满足所有要求。

3. 欠规格化（Underspecification）

关键约束条件缺失或隐含，导致形式化模型验证了"错误的规格"。

问题的严重性：这些缺陷会传播到形式化模型中，使得验证过程"成功"检查了错误的规格，最终导致实现 shipped 不安全的行为。在医疗设备领域，这可能直接危及患者生命安全。

现有方法的局限性

传统自动形式化方法

随着大语言模型的发展，自动形式化（将自然语言需求翻译为机器可验证规格）取得了快速进展。然而，语法有效性并不足够：

• • 形式良好的规格可能全局不一致
• • 触发条件可能永远无法达到（空洞性）
• • 模型可能在多个合理解读中"静默选择"一个，而用户毫不知情

根本问题：当不存在真实形式化标准时，没有正确性的"神谕"来判断自动生成的形式化是否准确。这是 LLM 生成形式化的固有缺陷——模型默认选择训练分布中最统计常见的解读，或省略源文本中隐含的约束。

医疗设备领域的特殊挑战

在医疗设备领域，需求规范涉及：

• • 警报条件
• • 泵行为控制
• • 安全参数范围

如果需求集合不一致，或者自动形式化器在多个解读中静默选择一个，下游验证可能成功但检查了完全错误的规格。

核心创新：VERIMED 神经符号框架

研究团队提出了VERIMED，一个将 LLM 自动形式化器与 SMT 求解器耦合的神经符号框架。其核心设计理念是：利用 LLM 的随机性作为诊断信号，利用 SMT 求解器的精确性作为验证工具。

创新一：四种需求级 SMT 审计

VERIMED 定义了四种求解器查询，对需求集合进行结构性审计：

技术细节：每个安全需求通常采用条件形式："如果条件 P 成立，则必须执行动作 Q"。VERIMED 将其编码为 SMT 公式 ρi(x) ≡ pi(x) ⇒ qi(x)，其中 x 表示系统的类型化状态变量（布尔控制状态和实数值设备参数）。

创新二：歧义检测的双向 SMT 等价检查

这是本研究的首创性贡献：利用求解器检查的样本不一致性来检测软件需求的歧义。

方法流程：

1. 1. 对同一需求 ri，独立采样 N 次（N=5）LLM 形式化，得到候选编码 ρ1i, ..., ρNi
3. 2. 对每对编码进行
4. 双向 SMT 等价检查
5. ：
• • 检查 C ∧ (ρai ∧ ¬ρbi) 是否可满足
• • 检查 C ∧ (ρbi ∧ ¬ρai) 是否可满足
6. 3. 如果任一检查可满足，求解器返回具体反例（witnessing assignment），暴露两个编码允许/禁止的不同状态
7. 4. 持续分歧表明自然语言需求存在多个合理解读，需要澄清

案例：透析液温度需求"温度应在 33°C 到 40°C 之间"

• • ρ1：排除两端点 (33, 40)
• • ρ2：包含两端点 [33, 40]
• • ρ3：排除 33 但包含 40 (33, 40]

求解器返回具体分歧见证（如 33°C、40°C），LLM 据此重写需求以明确边界语义。

创新三：反例引导的修复循环

当检测到缺陷时，VERIMED 执行针对性修复：

• • 结构性缺陷（不一致、空洞、冗余）：求解器反馈指导重新形式化
• • 歧义性缺陷：SMT 衍生的见证指导自然语言澄清

关键发现：求解器反馈的粒度决定了 LLM 修复的有效性。

实验验证：血液透析安全需求基准

研究团队在开源的血液透析安全需求上进行了广泛实验评估。

实验设置

• • 数据集：64 条血液透析安全需求
• • 任务：场景化安全问题问答（要求 grounded 于需求规范）
• • 基线：无反馈的 LLM 问答

核心结果

关键洞察：

1. 1. 使用被违反需求作为反馈 alone，准确率提升 24.6 个百分点
2. 2. 添加 SMT 反例作为额外反馈，再提升 18.5 个百分点
3. 3. 具体反例的价值：抽象的"需求 X 被违反"不如"在状态 S 下，需求 X 因条件 Y 未满足而被违反"有效

歧义检测结果

• • 64 条需求中，12 条（18.8%）被标记为产生多个不同编码
• • 所有 12 条需求在澄清后收敛到单一编码
• • 证明歧义检测程序的有效性

冗余检测

• • 四种审计中，冗余性审计标记了 2 条需求为冗余
• • 不可满足核心（unsat core）识别了覆盖这些需求的子集

技术架构：四阶段流水线

VERIMED 作为四阶段流水线运行：

┌─────────────────┐     ┌─────────────────┐     ┌─────────────────┐     ┌─────────────────┐│  歧义解析器     │ →   │  自动形式化器   │ →   │  属性验证器     │ →   │  查询验证器     ││  Ambiguity      │     │  Autoformalizer │     │  Property       │     │  Query          ││  Resolver       │     │                 │     │  Verifier       │     │  Verifier       │└─────────────────┘     └─────────────────┘     └─────────────────┘     └─────────────────┘   筛查歧义需求             翻译为 SMT-LIB          运行四种审计            验证场景化问答

阶段 A：歧义解析器

在需求进入形式化流水线前进行筛查。对每条需求 ri：

1. 1. 在高温下采样 LLM N 次，获得候选编码
2. 2. 应用双向等价检查
3. 3. 标记产生多个不同编码的需求为"歧义敏感"
4. 4. 将见证赋值作为具体区分状态呈现，LLM 重写源文本直到样本收敛
5. 5. 仅通过筛查的需求转发给自动形式化器

阶段 B：自动形式化器

将消歧后的需求集合翻译为单一 SMT-LIB 规格：

• • LLM 接收需求集合、规范 schema 和领域约束
• • 输出需求谓词和组装模型所需的声明
• • 如果生成的 SMT 格式错误或求解器拒绝，进入有界语法修复循环

阶段 C：属性验证器

对组装模型 M 运行四种审计查询：

• • 记录每条需求的每次检查结果
• • 审计失败时返回诊断信息（unsat core 或具体违反赋值）
• • 将缺陷定位到特定需求或需求子集

阶段 D：查询验证器

测试 proposed 答案是否在给定场景下被 M 蕴含：

1. 1. 场景提取器将问题映射为结构化状态赋值
2. 2. 动作生成器产生 schema 约束的候选答案
3. 3. 验证器发出蕴含查询 M ∧ s ∧ ¬a
4. 4. 不可满足确认蕴含，可满足返回反例
5. 5. 二次检查识别反例中违反的具体需求
6. 6. 响应构建器将结果翻译为自然语言解释

研究意义

理论贡献

1. 1. 首创神经符号需求分析框架：首次将求解器检查的样本不一致性应用于软件需求分析
2. 2. 操作化需求质量标准：将 established 的需求质量准则（一致性、完整性、无歧义性）转化为可执行的求解器查询
3. 3. 歧义的形式化定义：通过独立采样形式化之间的协议操作化定义歧义

实践价值

1. 1. 医疗设备安全：为 FDA 等监管机构提供自动化需求审计工具
2. 2. 降低验证成本：自动发现需求缺陷，减少后期返工
3. 3. 提高验证可信度：确保形式化验证检查的是"正确的规格"

行业影响

该方法可推广到任何安全关键领域：

• • 航空航天：飞行控制系统需求
• • 自动驾驶：安全约束规范
• • 金融系统：交易规则合规性
• • 工业控制：安全联锁逻辑

研究团队

• • Bethel Hall：史蒂文斯理工学院（bhall2@stevens.edu^[1]）
• • William Eiers：史蒂文斯理工学院（weiers@stevens.edu^[2]）

局限与未来方向

当前局限

1. 1. 领域约束手工定义：需要领域专家提供背景事实和变量 schema
2. 2. LLM 依赖：形式化质量受限于基础模型的能力
3. 3. SMT 求解器限制：仅支持量化自由公式和线性实数算术

未来探索

1. 1. 领域约束自动学习：从历史需求中挖掘隐含的领域知识
2. 2. 多求解器后端：支持更复杂的逻辑理论（非线性算术、数组等）
3. 3. 交互式澄清：与需求工程师的实时协作界面
4. 4. 跨领域验证：在航空航天、自动驾驶等领域验证通用性

结语

在软件系统日益复杂、安全要求不断提高的今天，VERIMED 代表了一种范式转变：从"信任 LLM 生成的形式化"到"用形式化方法验证 LLM 的输出"。

这项研究的核心洞察是：LLM 的随机性不是缺陷，而是诊断工具。通过巧妙地利用多次采样之间的分歧，结合 SMT 求解器的精确验证能力，可以在需求阶段就发现并修复潜在的安全隐患。

对于医疗设备软件开发者、形式化验证从业者和 AI 安全研究者而言，VERIMED 提供了一个可操作的框架，将自然语言需求的模糊性与形式化方法的严谨性桥接起来，为构建更安全的软件系统奠定了坚实基础。

论文信息：

• • 标题：Neurosymbolic Auditing of Natural-Language Software Requirements
• • arXiv 编号：2605.13817v1
• • 发布日期：2026 年 5 月 13 日
• • 分类：cs.SE（软件工程）, cs.AI（人工智能）
• • 机构：美国史蒂文斯理工学院

相关链接：

• • 论文地址：https://arxiv.org/pdf/2605.13817v1
• • 代码仓库：论文接收后公开

引用链接

[1] bhall2@stevens.edu: mailto:bhall2@stevens.edu[2] weiers@stevens.edu: mailto:weiers@stevens.edu