做安全关键系统（如自动驾驶、机器人）验证的团队，终于有了处理未知动力学的方法——用一条轨迹就能生成带形式保证的屏障证书，比传统依赖精确模型的方式实用得多，值得关注。
传统离散时间屏障证书要求安全函数每一步都非增，约束严格。本文提出 k-inductive 屏障证书，允许函数在 k-1 步内暂时增加（每步不超过阈值 ε），同时保证整体安全，提升了灵活性。研究利用神经网络构建 k-inductive 神经屏障证书（k-NBCs），适用于部分未知的非线性系统。为解决神经网络缺乏形式化保证的问题，采用反例引导归纳合成（CEGIS）与可满足性模理论（SMT）验证，但传统方法需已知系统动力学。本文借助 Willems 基本引理的推广，仅用单条状态轨迹构建数据驱动表示，实现未知模型的 SMT 验证，且不牺牲精度。在三个非线性案例上验证了方法的有效性。
k-Inductive Neural Barrier Certificates for Unknown Nonlinear Dynamics
While conventional (k=1) discrete-time barrier certificate conditions impose strict safety constraints by requiring the function to be non-increasing at every step, k-inductive barrier certificates relax this by allowing a temporary increase -- up to k-1 times, each within a threshold $ε$ -- while maintaining overall safety, and improving flexibility. This paper leverages neural networks and constructs k-inductive neural barrier certificates (k-NBCs) for (partially) unknown nonlinear systems. While neural networks offer scalability in the design process, they lack formal guarantees, requiring additional approaches such as counterexample-guided inductive synthesis (CEGIS) with satisfiability modulo theories (SMT) for verification. However, the CEGIS-SMT framework requires knowledge of system dynamics, which is unavailable in practical settings. To address this, we leverage the generalization of the Willems et al.'s fundamental lemma, using a single state trajectory, to construct a data-driven representation of (partially) unknown models for SMT verification without sacrificing accuracy. Additionally, CEGIS-SMT further removes the constraint of restricting barrier certificates to specific function classes, such as sum-of-squares, enabling greater flexibility in their design. We validate our approach on three nonlinear case studies with (partially) unknown dynamics.