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

Understand

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.