Verified-Intelligence/auto_LiRPA

解决的问题

auto_LiRPA 提供了一种形式化验证神经网络鲁棒性的方法。它解决了在输入数据或模型权重受到扰动时，确定模型输出范围（边界）的保证问题，确保网络在特定约束下预测结果保持稳定和可预测。

工作原理

该库将基于线性松弛的扰动分析（LiRPA）算法推广为一种在 PyTorch 计算图上运行的图算法。用户以标准的 nn.Module 定义模型，库会遍历图以自动推导并计算任意节点的边界。由于实现是可微的，可用于优化网络参数，构建“可证明防御”（即具有可证明鲁棒性的模型）。

适用人群

专为需要证明 AI 模型形式鲁棒性的研究人员和开发者设计，尤其适用于处理视觉模型（ResNet、DenseNet）、序列模型（LSTM、Transformers）以及用于李雅普诺夫稳定性的神经控制器的用户。

主要亮点

• 广泛的算法支持：实现了多种技术，包括 CROWN、DeepPoly、$α$-CROWN、$β$-CROWN、IBP 以及混合方法。
• 自动推导：无需用户手动推导复杂的 LiRPA 边界，其处理方式类似于自动微分中的梯度。
• 多样的模型支持：支持各种激活函数（ReLU、sigmoid、tanh、maxpool）和复杂架构（如 Transformers 和 LSTMs）。
• 高性能：包含内存高效的 GPU 实现和多 GPU 支持，可扩展至 ImageNet 等大规模数据集。
• 王冠之胜：作为 $α, β$-CROWN 的核心库，自 2021 年至 2025 年连续在 VNN-COMP 竞赛中夺冠。