如何使用 Marabou 对小型神经网络进行端到端鲁棒性形式化验证

在 AI 基础设施的生产实践中，传统的测试（Testing）只能证明错误的存在，而不能证明模型在特定扰动下的绝对安全性。对于自动驾驶、医疗诊断等高风险领域，形式化验证（Formal Verification）提供了数学上的保证。本文将演示如何使用 Marabou（一个基于 SMT 求解器的神经网络验证框架）对一个小型多层感知机（MLP）进行局部鲁棒性验证。

1. 核心概念：局部鲁棒性

局部鲁棒性是指：对于给定的输入 $x$ 和扰动半径 $\epsilon$，如果模型 $f$ 将 $x$ 分类为 $y$，那么对于所有满足 $||x’ – x||_{\infty} \le \epsilon$ 的 $x’$，其预测结果 $f(x’)$ 依然必须是 $y$。

2. 环境准备

首先，我们需要安装 Marabou 及其 Python 接口。建议在 Linux 环境下运行。

# 克隆并安装 Marabou
git clone https://github.com/NeuralNetworkVerification/Marabou.git
cd Marabou
pip install .

3. 模型准备与导出

Marabou 原生支持 ONNX 格式。我们先用 PyTorch 定义并训练一个简单的 3 层 MLP，用于处理简单的分类任务（如 MNIST 的精简版），然后导出为 ONNX。

import torch
import torch.nn as nn
import torch.onnx

class SimpleMLP(nn.Module):
    def __init__(self):
        super(SimpleMLP, self).__init__()
        self.fc1 = nn.Linear(784, 64)
        self.relu = nn.ReLU()
        self.fc2 = nn.Linear(64, 10)

    def forward(self, x):
        x = self.relu(self.fc1(x))
        x = self.fc2(x)
        return x

model = SimpleMLP()
# 导出模型为 ONNX 格式
dummy_input = torch.randn(1, 784)
torch.onnx.export(model, dummy_input, \"model.onnx\", verbose=False)

4. 编写验证脚本

验证的核心逻辑是：设定输入范围约束，并设定一个反向属性（Property）。如果 Marabou 找到了满足反向属性的解（SAT），说明模型不鲁棒；如果找不到（UNSAT），说明模型在范围内是鲁棒的。

from maraboupy import Marabou
import numpy as np

def verify_robustness(onnx_path, input_data, epsilon, target_class):
    # 加载 ONNX 模型
    network = Marabou.read_onnx(onnx_path)

    # 获取输入张量的索引
    input_vars = network.inputVars[0].flatten()
    output_vars = network.outputVars[0].flatten()

    # 1. 设置输入约束：x_i - epsilon <= x_i' <= x_i + epsilon
    for i in range(len(input_vars)):
        lb = input_data[i] - epsilon
        ub = input_data[i] + epsilon
        network.setLowerBound(input_vars[i], lb)
        network.setUpperBound(input_vars[i], ub)

    # 2. 设置验证属性：是否存在某个类别 j != target_class，使得 output[j] > output[target_class]
    # 我们通过添加矛盾约束来检查：寻找是否存在满足 output[other] >= output[target] 的反例
    for other_class in range(len(output_vars)):
        if other_class == target_class:
            continue

        # 创建一个独立的验证查询副本
        query = network.copy()
        # 约束：output[other_class] - output[target_class] >= 0
        # 注意 Marabou 接受的格式为：sum(c_i * x_i) <= scalar
        # 我们转化为：output[target_class] - output[other_class] <= 0
        eqn = Marabou.Equation(Marabou.Equation.LE)
        eqn.addAddend(1, output_vars[target_class])
        eqn.addAddend(-1, output_vars[other_class])
        eqn.setScalar(0)
        query.addEquation(eqn)

        # 运行求解器
        exit_code, vals, stats = query.solve()

        if exit_code == \"sat\":
            print(f\"[!] 发现反例！在类别 {other_class} 上不鲁棒。\")
            return False

    print(\"[+] 验证通过：该模型在给定范围内具有形式化鲁棒性。\")
    return True

# 模拟输入数据和验证
sample_input = np.random.rand(784)
verify_robustness(\"model.onnx\", sample_input, epsilon=0.01, target_class=3)

5. 结果分析与优化

• SAT (Satisfiable): 意味着模型存在漏洞。vals 字典会包含导致模型预测错误的精确输入值（即攻击样本）。
• UNSAT (Unsatisfiable): 意味着数学上证明了在该 $\epsilon$ 范围内，没有任何输入能让模型改变分类结果。

对于更深的网络，Marabou 可能会遇到搜索空间爆炸的问题。在 AI Infra 层级，我们可以通过以下方式优化：
1. 分段线性近似：Marabou 对 ReLU 激活函数有很好的优化。
2. 并行化：利用 Marabou 的多线程模式加速 SMT 分支定界过程。

通过这种端到端的流程，开发者可以将鲁棒性验证集成到 CI/CD 流水线中，确保每次模型迭代都不会引入安全回退。”,”tags”:[“AI Infra”,”Formal Verification”,”Model Robustness”,”Marabou”,”ONNX”],”summary”:”本文详细介绍了如何利用 Marabou 验证框架对基于 ONNX 的小型神经网络进行端到端局部鲁棒性形式化验证，并提供了完整的代码实现流程。”}
“`