BarrierBench : Evaluating Large Language Models for Safety Verification in Dynamical Systems

TL;DR

This work tackles the challenge of safety verification for cyber-physical systems by leveraging large language models (LLMs) to synthesize barrier certificates, with an agentic framework that couples Retrieval, Synthesis, and Verification. BarrierBench, a 100-system benchmark spanning linear, nonlinear, continuous-time, discrete-time, and controlled dynamics, assesses the effectiveness of LLM-guided barrier design and barrier–controller co-synthesis, using SMT solvers for formal verification. The approach achieves over 90% success on BarrierBench and demonstrates that retrieval-augmented generation and iterative refinement materially improve reliability and efficiency beyond single-prompt baselines. By releasing BarrierBench and the accompanying toolchain, the authors provide a public, extensible platform to advance the integration of language-based reasoning with formal verification in dynamical systems. The work highlights a promising direction for automated, interpretable safety guarantees in CPS, while acknowledging current limitations and the need for broader coverage and scalability.

Abstract

Safety verification of dynamical systems via barrier certificates is essential for ensuring correctness in autonomous applications. Synthesizing these certificates involves discovering mathematical functions with current methods suffering from poor scalability, dependence on carefully designed templates, and exhaustive or incremental function-space searches. They also demand substantial manual expertise--selecting templates, solvers, and hyperparameters, and designing sampling strategies--requiring both theoretical and practical knowledge traditionally shared through linguistic reasoning rather than formalized methods. This motivates a key question: can such expert reasoning be captured and operationalized by language models? We address this by introducing an LLM-based agentic framework for barrier certificate synthesis. The framework uses natural language reasoning to propose, refine, and validate candidate certificates, integrating LLM-driven template discovery with SMT-based verification, and supporting barrier-controller co-synthesis to ensure consistency between safety certificates and controllers. To evaluate this capability, we introduce BarrierBench, a benchmark of 100 dynamical systems spanning linear, nonlinear, discrete-time, and continuous-time settings. Our experiments assess not only the effectiveness of LLM-guided barrier synthesis but also the utility of retrieval-augmented generation and agentic coordination strategies in improving its reliability and performance. Across these tasks, the framework achieves more than 90% success in generating valid certificates. By releasing BarrierBench and the accompanying toolchain, we aim to establish a community testbed for advancing the integration of language-based reasoning with formal verification in dynamical systems. The benchmark is publicly available at https://hycodev.com/dataset/barrierbench

Figures (1)

• Figure 1: Architecture of the agentic framework integrating Retrieval, Synthesis, and Verifier agents for LLM-guided barrier certificate synthesis.

Theorems & Definitions (3)

• Definition 1: Safety Specification
• Definition 2: Barrier Certificate
• Theorem 1: Safety via Barrier Certificates prajna2004safety