闭环：用于非线性神经反馈系统可扩展验证的分支定界法
Closing the Loop: Branch-and-Bound for Scalable Verification of Nonlinear Neural Feedback Systems
- Stanford University（斯坦福大学）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
针对非线性神经反馈系统验证的可扩展性难题，提出基于闭环抽象的分支定界框架，通过接口与算法联合细化包络和分割激活，显著提升性能。
AI中文摘要：
尽管非线性神经反馈系统验证方面近期取得了进展，但可扩展性仍是核心障碍，因为最先进的求解器尚无法处理自主应用中网络规模和非线性动态。组合求解器无法扩展到大型网络，而传播式求解器则过度牺牲精度。本工作旨在通过将验证问题表述为闭环系统抽象上的分支定界来提高组合求解器的可扩展性。我们引入了\rail，一个将动态的多面体包络暴露给LiRPA风格边界传播的接口，以及\clipper，一种联合细化包络并分割控制器激活的分支定界算法。该框架能够在闭环系统的计算图上进行联合推理，跨时间步保留符号相关性。我们展示了我们的构造，并表明其相较于最先进方法带来了显著改进。
英文摘要：
Despite recent advances in the verification of nonlinear neural feedback systems, scalability remains the central obstacle, as state-of-the-art solvers do not yet handle the network sizes and nonlinear dynamics of autonomy applications. Combinatorial solvers do not scale to large networks, whereas propagative solvers excessively sacrifice precision. This work seeks to improve the scalability of combinatorial solvers by formulating verification as branch-and-bound on an abstraction of the closed-loop system. We introduce \rail, an interface that exposes polyhedral enclosures of the dynamics to LiRPA-style bound propagation, and \clipper, a branch-and-bound algorithm that jointly refines enclosures and splits controller activations. This framework enables joint reasoning on the computational graph of the closed-loop system, preserving symbolic correlations across time steps. We present our construction and show that it yields significant improvements over the state of the art.
