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

arXiv: https://arxiv.org/abs/2511.09363 · HTML: https://mlsanity.com/paper/2511.09363/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 28 of its 45 references that are in the map.
- First posted on arXiv 12 Nov 2025.

## Builds on (most cited first, 28 of 28)

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Do As I Can, Not As I Say: Grounding Language in Robotic Affordances](https://mlsanity.com/paper/2204.01691/) (2022)
- [Solving Quantitative Reasoning Problems with Language Models](https://mlsanity.com/paper/2206.14858/) (2022)
- [Large Language Models](https://mlsanity.com/paper/2307.05782/) (2023)
- [DriveGPT4: Interpretable End-to-end Autonomous Driving via Large Language Model](https://mlsanity.com/paper/2310.01412/) (2023)
- [Control Barrier Functions: Theory and Applications](https://mlsanity.com/paper/1903.11199/) (2019)
- [SayPlan: Grounding Large Language Models using 3D Scene Graphs for Scalable Robot Task Planning](https://mlsanity.com/paper/2307.06135/) (2023)
- [Text2Motion: From Natural Language Instructions to Feasible Plans](https://mlsanity.com/paper/2303.12153/) (2023)
- [Safe Control with Learned Certificates: A Survey of Neural Lyapunov, Barrier, and Contraction methods](https://mlsanity.com/paper/2202.11762/) (2022)
- [Personalized Autonomous Driving with Large Language Models: Field Experiments](https://mlsanity.com/paper/2312.09397/) (2023)
- [Visually-Grounded Planning without Vision: Language Models Infer Detailed Plans from High-level Instructions](https://mlsanity.com/paper/2009.14259/) (2020)
- [Safe Learning of Quadrotor Dynamics Using Barrier Certificates](https://mlsanity.com/paper/1710.05472/) (2017)
- [Formal Synthesis of Stochastic Systems via Control Barrier Certificates](https://mlsanity.com/paper/1905.04585/) (2019)
- [Control Barrier Functions for Unknown Nonlinear Systems using Gaussian Processes](https://mlsanity.com/paper/2010.05818/) (2020)
- [Data-driven verification and synthesis of stochastic systems via barrier certificates](https://mlsanity.com/paper/2111.10330/) (2021)
- [Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings](https://mlsanity.com/paper/2403.10497/) (2024)
- [Robust Control Barrier Functions for Nonlinear Control Systems with Uncertainty: A Duality-based Approach](https://mlsanity.com/paper/2208.05955/) (2022)
- [Safe Reach Set Computation via Neural Barrier Certificates](https://mlsanity.com/paper/2404.18813/) (2024)
- [Neural Continuous-Time Supermartingale Certificates](https://mlsanity.com/paper/2412.17432/) (2024)
- [Counter-Example Guided Synthesis of Control Lyapunov Functions for Switched Systems](https://mlsanity.com/paper/1509.03688/) (2015)
- [Unmatched Control Barrier Functions: Certainty Equivalence Adaptive Safety](https://mlsanity.com/paper/2207.13873/) (2022)
- [A data-driven approach for safety quantification of non-linear stochastic systems with unknown additive noise distribution](https://mlsanity.com/paper/2410.06662/) (2024)
- [Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems](https://mlsanity.com/paper/1303.6885/) (2013)
- [PRoTECT: Parallelized Construction of Safety Barrier Certificates for Nonlinear Polynomial Systems](https://mlsanity.com/paper/2404.14804/) (2024)
- [Data-Driven Permissible Safe Control with Barrier Certificates](https://mlsanity.com/paper/2405.00136/) (2024)
- [LLM-Enhanced Symbolic Control for Safety-Critical Applications](https://mlsanity.com/paper/2505.11077/) (2025)
- [Stochastic Control Barrier Functions with Bayesian Inference for Unknown Stochastic Differential Equations](https://mlsanity.com/paper/2312.12759/) (2023)
- [Sum-of-Squares Certificates for Almost-Sure Reachability of Stochastic Polynomial Systems](https://mlsanity.com/paper/2510.25513/) (2025)

## Abstract (arXiv)

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