基于生成式障碍证书的非线性系统形式化安全验证
Formal Safety Verification for Nonlinear Systems with Generative Barrier Certificate
中文总结 AI 辅助
该研究针对非线性系统安全验证中障碍证书推导计算成本高的问题，提出基于大语言模型的生成式框架，将BMI问题转化为LMI测试，实现了远超传统方法的速度与性能提升。
中文摘要 AI 辅助
安全验证是控制理论的基础问题。障碍证书（BCs）提供了强大的形式化机制，但推导BCs的计算成本很高。本文提出一种生成式框架，利用大语言模型（LLMs）通过推理合成BCs。基于经典的平方和（SOS）方法，我们训练了一个领域特定的LLM，能够为非线性系统生成高质量的BC候选。随后，LLM生成的BCs将难以处理的双线性矩阵不等式（BMI）求解问题转化为凸线性矩阵不等式（LMI）可行性测试，在保持正确性的同时显著提升了效率。实验结果表明，我们的生成式方法比传统的数值BC方法实现了数个数量级的加速，且出人意料地超过了最先进的专用神经BC模型。这些发现标志着在将生成式AI与动力系统的形式化安全验证相结合方面迈出了实质性的一步。
英文摘要
Safety verification is a fundamental problem in control theory. Barrier certificates (BCs) provide a powerful formal mechanism, yet deriving BCs is computationally intensive. This paper introduces a generative framework that leverages large language models (LLMs) to synthesize BCs through reasoning. Based on the classical Sum-of-Squares (SOS) approach, we train a domain-specific LLM capable of generating high-quality BC candidates for nonlinear systems. Then, the LLM-generated BCs transform the intractable Bilinear Matrix Inequality (BMI) solving problems into convex Linear Matrix Inequality (LMI) feasibility test, significantly improving efficiency while preserving correctness. Experimental results show that our generative method achieves several orders of magnitude speedup over traditional numerical BC approaches and, perhaps surprisingly, surpasses the state-of-the-art dedicated neural BC model. These findings mark a substantive step toward integrating generative AI with formal safety verification for dynamical systems.
