Skip to content

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

🕒 Published (v1): 2025-11-12 14:23 UTC · Source: Arxiv · link

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

💬 Ask ChatGPT✦ Ask Claude

TL;DR

BarrierBench introduces a 100-system benchmark and an accompanying LLM-agentic harness for synthesizing barrier certificates—scalar functions that formally prove dynamical system safety. A three-agent pipeline (Retrieval → Synthesis → Verifier) with SMT-based formal verification lifts Claude Sonnet 4's success rate from 41% (single prompt) to 90%.

Problem

Barrier certificate synthesis requires expert intuition to select polynomial templates, SMT solvers, and hyperparameters—expertise transmitted informally in natural language. Existing methods (SOS programming, CEGIS, neural approaches) suffer from exponential scaling with system dimension, reliance on fixed template families, and lack of community benchmarks to compare LLM-guided approaches.

Method

The framework instantiates three collaborating LLM-powered agents:

  1. Barrier Retrieval Agent: performs two-stage retrieval—feature-based filtering (dimension, linearity, time domain, topology) followed by LLM-ranked structural similarity—to surface analogous verified certificates from a persistent database as few-shot examples.
  2. Barrier Synthesis Agent: proposes candidate barrier functions \(B: \mathcal{X} \to \mathbb{R}\) satisfying \(B(x) \leq 0\ \forall x \in X_I\), \(B(x) > 0\ \forall x \in X_U\), and \(\nabla B(x) \cdot f(x) < 0\) (continuous-time) or \(B(f(x)) - B(x) \leq 0\) (discrete-time); jointly synthesizes controllers for controlled systems.
  3. Barrier Verifier Agent: applies two-stage verification—sample-based screening over \(N=5000\) points to discard obvious failures before invoking SMT solvers (Z3, Yices, cvc5), selected adaptively by problem structure.

Refinement proceeds for up to \(K=5\) main iterations with \(R=4\) refinements each; early refinements adjust coefficients (structure-preserving), later refinements modify coupling terms. Counterexamples from SMT are fed back to the Synthesis Agent as structured prompts.

Key Contributions

  • BarrierBench: 100 dynamical systems (1D–8D, linear/nonlinear, continuous/discrete-time, autonomous/controlled), with 68 requiring barrier–controller co-synthesis; publicly released with toolchain.
  • Three-agent harness combining LLM reasoning, RAG retrieval, two-stage verification, and iterative SMT-guided refinement.
  • Barrier–controller co-synthesis: framework jointly produces certificate and state-feedback law, ensuring mathematical compatibility.
  • Empirical ablation isolating contributions of retrieval, per-iteration refinement, and multi-iteration exploration.

Results

  • Claude Sonnet 4 full framework: 90% success (90/100) vs. 41% single-prompt baseline (+49 pp).
  • ChatGPT-4o full framework: 46% success (46/100) vs. 17% baseline (+29 pp).
  • 70% of solved cases (63/90) resolved on the first attempt without refinement (I1–R0), driven largely by retrieval.
  • 15.6% solved via non-structural coefficient refinement (R1–R2); 14.4% required structural modification (R3–R4).
  • Second iteration (I2) adds 15 problems (16.7%); \(I_{3+}\) adds 12 (13.3%), with 50% of those requiring structural refinement—showing harder problems demand deeper template exploration.

Limitations

  • 10 unsolved problems involve high-dimensional systems with mixed trigonometric/exponential dynamics where both LLM synthesis and SMT solvers struggle (solver timeouts, satisfiability failures).
  • SMT solver scalability degrades with system dimension and nonlinearity complexity.
  • Success rate gap between Claude Sonnet 4 (90%) and ChatGPT-4o (46%) indicates strong model dependence.
  • Benchmark covers polynomial and control-affine dynamics; generalization to more exotic dynamics classes is unvalidated.
  • Retrieval degrades gracefully to baseline for out-of-distribution systems, but no mechanism to detect this degradation proactively.

Relevance to Harnesses / Meta-Harnesses

BarrierBench is a concrete instantiation of a domain-specialized multi-agent harness with closed-loop tool integration: the three agents form a directed pipeline where a formal SMT oracle (external tool) generates structured feedback that re-enters the LLM synthesis loop—a pattern central to meta-harness design. The separation of concerns (retrieval, generation, verification) and the iterative refinement protocol with bounded retries (\(K \times R\)) directly mirrors harness design patterns for reliability-critical LLM pipelines. The RAG component demonstrates how persistent solution databases can be integrated as a memory substrate within agent harnesses. The ablation methodology—isolating retrieval, single-iteration refinement, and multi-iteration exploration—provides a transferable evaluation framework for other harnesses that compose similar primitives.