Researchers propose using invertible neural networks to find provable forward invariant sets for AI control systems

核心问题是：AI控制器事先给定时，如何找到可解析证明的前向不变集（Forward-Invariant Set, FIS），使轨迹留在集内且与不安全状态集不相交。

• 认证场景：作者称神经网络控制器被用在传统控制理论往往难以处理好的非线性控制上；航空、智能驾驶、手术机器人等又常因法规需要可认证的可信性。控制器难以解释或验证时，作者称认证机构不会批准。
• FIS的作用：FIS是状态空间子集，从其中任一状态出发的未来轨迹始终留在该子集内。作者称，若它与不安全集F不相交，则从FIS内出发的轨迹与F不相交，机构可以信任相应初始状态。
• 现有缺口：作者称寻找FIS是已知难题，非线性高时更难。Yang et al. [14]联合调整控制器与Lyapunov函数，不面向控制器事先给定（例如厂商提交认证）。α,β-CROWN能证明超矩形输入域上的输出是否落在给定多面体内，但作者称高非线性系统的FIS呈超矩形的机会低。
• 本文提出：用可逆网络把原状态空间映到潜空间，固定超矩形候选并训练变换，再用α,β-CROWN验证。作者证明：验证返回成功时，该候选及其逆像都是可解析证明的FIS。

按论文第二节与引言中的对比来写。

传统控制里的不变集

• LMI [22] [23] [24]：线性系统上寻找FIS的经典方法。论文指出它要求纯线性动态，不适用于非线性AI控制系统。
• 非线性系统方法：Lyapunov间接法、Zubov方法、平方和规划、LaSalle不变原理、Krasovskii方法、变梯度法。论文称它们假定线性、多项式或其他可解析处理的闭式动态；含神经网络的动态非线性、非多项式，且解析上难处理。

用形式化工具处理神经网络

• SMT、MIP、HJ可达性与SDP [36] [37] [38] [39]：被用来为神经网络寻找FIS。论文称SMT、MIP、HJ有可扩展性问题；SDP要求网络能被光滑二次包络较好近似。

控制器可调或已经给定

• Yang et al. [14]：作者称为面向AI控制系统寻找FIS的当时先进方法。它联合训练控制器与Lyapunov函数，训练成功则该函数蕴含一个FIS；论文指出它不是为控制器事先给定而设计。
• Harapanahalli et al. [40]：系统事先给定时，解析证明一个给定平行多面体候选是不是FIS。论文指出：若证不成，它不说明如何再找候选；这是充分条件，不是主动搜索FIS的方法。

基线与测试床

• 基线：把Yang et al. [14]改成搜索中禁止修改控制器。植物模型来自Gymnasium的pendulum、cart pole，以及Yang et al.的PVTOL。

作者称据其所知，文献中没有正好解决同一问题的工作；本文与Yang et al.的差别是控制器由认证场景事先给定，并用可逆网络把验证转到潜空间的超矩形上。

整体上，Normalized INN（NINN）把给定闭环从原空间X0映到潜空间X1，固定超矩形候选并训练变换，再用α,β-CROWN做解析验证。

离散闭环与要找的集合

• 对象：控制器π事先给定。连续植物写成x的导数等于fplt(x, π(x))。控制器在离散计算机上运行，论文把问题转到周期δ下的离散闭环xd(k+1)=fcld(xd(k))，执行为零阶保持。
• 离散FIS：从Id中任一xd(0)出发，离散轨迹永远留在Id内。Proposition 2称：若Id中每一点的下一步仍在Id内，则由归纳，Id就是FIS。
• 与连续安全的关系：作者讨论的情形是，可由不依赖于k的执行界Bad得到离散化误差界Bed；初始状态在Id内时，连续轨迹落在Id与Bed的Minkowski和内。作者称可证明安全是该和与F不相交；系统本来就是离散模型时，则为Id与F不相交。对宏观物理对象，作者称δ足够小时Bed趋于空，可经验上放宽为Id与F不相交。作者称缺失的一环是寻找超矩形离散FIS。

潜空间候选与NINN

• 双射：NINN是归一化层Nnorm(μ, σ)与可逆网络(T, T^{-1})的串联，在X0与X1之间双射。μ、σ事先给定。作者称它们宜分别对应X0中偏好FIS的中心与各维半径；若安全集是超矩形，μ取其心，σ的各分量取对应半边长。
• 候选固定：在X1取以原点为中心的超立方体。I_d,1=C(R_fis)表示∞-范数半径为预设常数Rfis的该超立方体；训练不改这个集合，只改NINN。实验中Rfis=1.0。
• “更规则”：作者将其定义为能在X1找到超矩形FIS。X0中的对应集为Id,0=T̃^{-1}(Id,1)，形状由逆变换决定，不必是超矩形。

训练损失、采样与早停

• 偏差：给定时域K，d*是K步轨迹相对某个中心超立方体的超出量最大值，未超出记0。收缩半径Rshr=ρshr·Rfis，ρshr∈(0,1]。损失鼓励Id,1内的点相对Rshr的d*为0，并惩罚大于0的情形。论文称K可按算力在3到5之间取；实验取3，ρshr=0.995。
• 四个子集：内部点Zinr、边界点Zb、用PGD最大化相对Rfis之偏差得到的不利点Zadv，以及回放区中以往大偏差边界点Zrep（附录A）。偏差损失对每子集最难的比例ρhrd和全体分别加权；中心损失鼓励T̃^{-1}(0)靠近μ。总损失为二者加权和。论文给出的经验权重为wZinr=30、wZb=120、wZadv=80、wZrep=220、λ=0.15、wcen=5。
• 早停与回放：连续若干轮里，训练点相对Rfis（不是Rshr）的d*全为0且达到θstp后，再用PGD采Istp个点；若相对Rfis仍全为0则提前返回，否则计时清零。训满E轮也返回当前NINN。回放区最多存Irep^max个元素，采样概率正比于历史偏差，每Erep轮用当前网络重算偏差。

验证与总流程

• 三步：选定Id,1；用上述损失训练NINN，从而确定X1中的闭环fcld,1；调用α_β_CROWN(f=fcld,1, X=Id,1, B=Id,1, Tmax)。返回true则success，false或unknown则failure。论文未写失败后更换Rfis再搜的外层循环。
• 定理所用条件：∀ x⃗∈ I_d,1, f_cld,1(x⃗)∈ I_d,1。这是α,β-CROWN在时限内返回true时所解析确立的一步包含；Theorem 1据此称Id,1是X1上可解析证明的超矩形FIS，Id,0是X0上可解析证明的FIS。
• 工具：α,β-CROWN要求输入域为超矩形、输出界为多面体，可处理多种网络层与激活；超时返回unknown。超矩形也是多面体，故候选可同时作为输入域和输出界。

实验设置

• 测试床：pendulum、cart pole的植物模型来自Gymnasium，PVTOL来自Yang et al. [14]。状态维数分别为2、4、6，执行维数1、1、2。
• 被测控制器：用Stable Baselines3（SB3）的强化学习实现分别训练20、20、5个神经网络控制器，共45个。内部神经元数η：前两者128，PVTOL为24；激活函数写为SB3 default。控制器训练好后固定，再接回植物模型。
• 基线：Yang et al. [14]的改写版，搜索时禁止修改控制器。作者称未改其源代码，只改配置以固定控制器，并由两名领域专家独立复查。移植的植物模型做了同输入一致性检查。
• 本文配置：Table II。三类均为Rfis=1.0、K=3、ρshr=0.995、ρhrd=0.25。μ、σ由领域专家设定。训练轮数上限E为3000、50000、100000。Tmax设得足够大，调用不因碰到Tmax而中止。
• 判定与指标：Overall Procedure返回success，即α,β-CROWN对fcld,1在Id,1上返回true。另报告运行时间、X0中FIS大小（Monte Carlo估计）、各维范围大小与中心漂移。论文未报告同一控制器的重复次数，也未使用LLM评审。
• 硬件：32核AMD Ryzen系列CPU、64 GB内存、NVIDIA GeForce RTX 4090（24 GB VRAM）。

主结果

据Table III：

Swipe horizontally to read the table

应用	控制器数	本文成功率	基线成功率
Pendulum	20	100% (20/20)	0% (0/20)
Cart pole	20	100% (20/20)	0% (0/20)
PVTOL	5	100% (5/5)	0% (0/5)

• 成功率：作者报告本文在全部45个系统上找到FIS，基线一个都没找到。
• 时间：正文未给出秒数。作者称pendulum与cart pole上本文耗时小于基线；PVTOL上基线更小，并称部分原因是基线很快确认失败。摘要称45个中有40个本文耗时更小。Fig. 3是该对比，纯文本中无可读端点数值。
• 比较对象：作者称基线原方法不是为控制器事先给定而设计，这里比较的是禁止改控制器之后的版本。

X0中FIS的大小

只统计本文找到的原空间FIS；基线没有FIS。大小用Monte Carlo估计：在足够大的超矩形C0中均匀采样，用落入Id,0的比例乘C0的大小。论文未报告采样次数。偏好大小按领域专家的μ、σ，并假设偏好FIS为超矩形，取各维2σ[i]的乘积。

据Table IV：

Swipe horizontally to read the table

应用	min	median	mean	max	preferred
Pendulum	0.929	1.307	1.288	1.308	1.800
Cart Pole	0.033	0.346	0.473	1.348	0.896
PVTOL	0.008	0.012	0.011	0.013	51.200

• 作者称pendulum与cart pole的大小在偏好大小的3.7%到150.4%之间波动。
• 作者称PVTOL只在偏好大小的0.016%到0.025%之间，并认为这可能因为PVTOL的X0 FIS非线性高，而偏好大小按超矩形计算。
• 作者称FIS更大则初始状态的选择更多；机构只在初始状态位于找到的FIS内时信任该系统。

各维范围与中心漂移

• 范围：Table V给出各维范围的min、median、mean、max及偏好范围2σ[i]。作者称各维范围在对应偏好的15.8%到430.6%之间波动。表中例如Cart Pole第1维max为3.014、偏好为0.700；PVTOL第3维min为0.253、偏好为1.600。
• 中心：Table VI的数值单位为10^{-3}。作者称各维中心漂移在对应偏好范围的−5.6%到6.5%之间，并认为较小的漂移可能与中心损失有关，也称中心大致符合领域专家设定的偏好中心。
• 例外：基线在三类上成功率都是0。PVTOL上本文找到了FIS，但原空间大小相对偏好很小；该应用上作者称基线耗时更短。

其他消融与分析

• 论文未报告对K、Rfis、ρshr、损失权重或采样规模的消融。
• Table II：内部点与边界点采样数，pendulum和cart pole为4096，PVTOL为65536；不利点与回放采样为其一半。
• θstp为3（pendulum）或5（cart pole、PVTOL）；Istp为4096或16384；回放大修周期Erep均为25。
• 作者称除μ、σ外的配置是best effort，如何优化超出本文范围（Section VI-A）。

作者指出的局限与后续方向

• 最大可行FIS：作者在Section VI-C写到，还可以有其他评价指标；若已知最大可行FIS，或进一步已知给定forbidden set F时的最大可行FIS，现有指标会更相关。如何计算这些量是超出本文焦点的非平凡问题，作者称值得后续多篇论文。作者把本文定位为先给出一个能找到FIS的方法。
• PVTOL个数：作者在Section VI-C写到，计算预算有限，PVTOL只评了5个而不是20个；同时称按应用分开的比较已经呈现出他们所写的重要事实。
• 测试床可否再扩：作者在Section VI-C写到，测试床总可以扩展到更多控制应用，并称pendulum、cart pole、PVTOL作为经典测试床是合理代表，状态维数2到6，与Gymnasium中classic control的维数范围一致。

实验覆盖范围

• 被测系统是pendulum、cart pole、PVTOL上事先训练好的神经网络控制器，数量20、20、5，状态维数2、4、6（Table I，Section VI-A）。
• 对照只有禁止修改控制器的Yang et al. [14]；植物模型来自Gymnasium与Yang et al.，控制器由SB3训练（Section VI-A、VI-B）。
• 报告的是找FIS是否成功（Table III）、耗时对比（Fig. 3，正文无秒数）、X0 FIS大小（Table IV）以及各维范围与中心漂移（Table V、VI）。
• 论文未报告Monte Carlo样本量、同一控制器的重复次数、与某个具体F的交集，以及Bed或连续轨迹安全的数值结果；Section IV讨论了Bed与F，Section VI的结果表未给出这些量。
• 验证器为α,β-CROWN；Tmax被设得足够大，实验中没有因超时得到unknown（Section VI-B）。激活函数只写SB3 default，论文未给出具体函数名。

本文处理的是认证场景：AI控制器事先给定，不能为了构造Lyapunov函数去改控制器，却仍要给出可解析核验的安全依据。

• 要找的对象：一个前向不变集。从其中出发的未来状态留在集内；作者称它若不与不安全集F相交，认证机构就可以信任相应初始状态。直接在原空间找超矩形不变集的机会低，所以先把离散闭环用归一化可逆网络映到潜空间。
• 做法：潜空间候选固定为半径Rfis的中心超立方体，训练只改变换。偏差损失把K步轨迹压进略小的立方体，中心损失把原空间像的中心拉向领域专家指定的μ。α,β-CROWN若确认一步像仍在候选内，作者证明该候选及其逆像是可解析证明的FIS。评测成功对应这一离散闭环结论；连续安全还要处理离散化误差界Bed与F，实验未报告这一步。
• 结果：45个系统（pendulum 20、cart pole 20、PVTOL 5）上本文找FIS的成功率为100%，禁止改控制器的Yang et al.基线为0%（Table III）。作者称40/45个测试床上本文耗时更小，PVTOL上基线更快。按作者对Table IV的概括，X0 FIS大小相对偏好，pendulum与cart pole在3.7%到150.4%，PVTOL在0.016%到0.025%。作者称找到的中心大致符合偏好。
• 作者的收束：该方法能为这些给定的AI控制系统找到可解析证明的FIS，基线找不到。作者把相对最大可行FIS、以及给定F时的最大可行FIS，留作后续工作。