用大模型自动生成安全验证证书，提升系统可靠性。
BarrierBench: Evaluating Large Language Models for Safety Verification in Dynamical Systems
- 通过自然语言推理驱动模板发现与验证，实现自动化安全证书合成。
- 在100个动态系统上成功率超90%，支持控制器协同设计。
- 适合从事形式化验证与智能系统安全的科研人员使用。
通过屏障证书对动态系统进行安全验证，是保障自主应用正确性的关键。现有方法在合成屏障证书时存在可扩展性差、依赖精心设计的模板、需穷举或增量搜索函数空间等问题，且高度依赖人工经验——包括模板选择、求解器配置、超参数调整及采样策略设计，这些知识传统上依赖语言推理而非形式化方法传递。这引发一个核心问题：能否用语言模型捕捉并实现这种专家推理？本文提出基于大语言模型的智能体框架，利用自然语言推理生成、优化和验证候选证书，结合LLM驱动的模板发现与SMT验证，并支持屏障-控制器协同合成以保证一致性。为评估该能力，我们构建了包含100个动态系统的BarrierBench基准，涵盖线性、非线性、离散时间与连续时间场景。实验评估了语言模型引导合成的有效性，以及检索增强生成与智能体协作策略对可靠性和性能的提升。框架在各项任务中成功生成有效证书的比例超过90%。我们公开发布BarrierBench及配套工具链，旨在建立社区测试平台，推动语言推理与形式化验证在动态系统中的融合。基准数据集可访问：https://hycodev.com/dataset/barrierbench
原文摘要 · Abstract (English)
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
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。