arXiv cs.LG@Ben Wooding, Hongchao Zhang, Taylor T. Johnson, Abolfazl Lavaei精选37传统离散时间屏障证书要求安全函数每一步都非增，约束严格。本文提出 k-inductive 屏障证书，允许函数在 k-1 步内暂时增加（每步不超过阈值 ε），同时保证整体安全，提升了灵活性。研究利用神经网络构建 k-inductive 神经屏障证书（k-NBCs），适用于部分未知的非线性系统。为解决神经网络缺乏形式化保证的问题，采用反例引导归纳合成（CEGIS）与可满足性模理论（SMT）验证，但传统方法需已知系统动力学。本文借助 Willems 基本引理的推广，仅用单条状态轨迹构建数据驱动表示，实现未知模型的 SMT 验证，且不牺牲精度。在三个非线性案例上验证了方法的有效性。论文安全验证神经屏障证书未知非线性系统CEGIS-SMT数据驱动推荐理由：做安全关键系统（如自动驾驶、机器人）验证的团队，终于有了处理未知动力学的方法——用一条轨迹就能生成带形式保证的屏障证书，比传统依赖精确模型的方式实用得多，值得关注。