{"id":"arxiv/2608.18118","url":"https://arxiv.org/abs/2608.18118","tags":["math.OC","eess.SY"],"score":0,"title":"Formal Safety Verification for Nonlinear Systems with Generative Barrier Certificate","domain":"math.OC","source":"arxiv","authors":["Mengxin Ren","Hanrui Zhao"],"reviews":0,"subject":"math.OC","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-07-13","reactions":{}}