分支定界新突破！神经反馈系统验证可扩展性大幅提升
Closing the Loop: Branch-and-Bound for Scalable Verification of Nonlinear Neural Feedback Systems
📖 AI 总结
该研究针对非线性神经反馈系统验证中的可扩展性瓶颈展开。现有组合式求解器难以应对大规模网络，而传播式求解器则精度损失过大。作者将验证问题建模为闭环系统抽象上的分支定界过程，提出RAIL接口，将动力学的多面体外包暴露给LiRPA风格的边界传播，并设计CLIPPER分支定界算法，联合细化外包并分裂控制器激活。该框架支持在闭环系统计算图上进行联合推理，跨时间步保留符号相关性。实验表明，该方法相较当前最优方案取得显著改进，为自主系统中大规模非线性神经反馈系统的可扩展验证提供了新路径。
🔑 关键词速览
| 分支定界 (Branch-and-Bound) | 一种通过分支搜索空间并计算边界来寻找最优解的算法，常用于组合优化和验证。 |
| 神经反馈系统 (Neural Feedback System) | 包含神经网络控制器的闭环动力系统，控制器根据系统状态产生反馈控制输入。 |
| LiRPA 风格边界传播 (LiRPA-style Bound Propagation) | 一种基于线性松弛的边界传播方法，用于高效计算神经网络输出的上下界。 |
| 多面体包围 (Polyhedral Enclosure) | 用多面体集合来近似表示系统状态或轨迹的可能范围，常用于可达性分析。 |
| 符号相关性 (Symbolic Correlations) | 在计算图中保持变量之间的符号关系，以精确传播约束，避免过度近似。 |
📱 每天一份 AI 前沿日报
关注公众号，每天 09:00 推送 · 不错过任何重磅