BarrierBench：用大模型验证动态系统安全的智能体框架

BarrierBench是一个包含100个动态系统测试用例的基准数据集，配合基于大语言模型（LLM）的智能体框架，用于自动化合成屏障证书以验证系统安全性。该框架结合检索增强生成（RAG）、SMT形式化验证与迭代优化，在Claude Sonnet 4上达到90%以上的成功率。

在自动驾驶、机器人控制和工业自动化等领域，确保动态系统的安全性是核心难题。传统方法依赖专家手动设计屏障证书（Barrier Certificate），但随着系统复杂度增加，手动设计变得困难且易出错。近年来LLM展现出强大推理和代码生成能力，然而缺乏标准化测试基准来评估其在形式化验证领域的表现。

BarrierBench由伊斯法罕理工大学、马克斯·普朗克软件系统研究所和科罗拉多大学博尔德分校联合开发，已被第8届学习动力学与控制会议（L4DC 2026）接收。核心贡献包括：100个涵盖多种动力学系统的测试用例、每个用例配有正确的屏障函数多项式和控制律表达式、开源数据集（地址：https://hycodev.com/data/BarrierBench.json）。

BarrierBench的多智能体协作框架结合LLM与形式化工具：

1. 检索增强生成（RAG）模块：从数据集找相似已解决案例，辅助LLM参考历史经验；
2. 屏障合成智能体：引导LLM探索屏障函数形式，生成数学表达式并支持迭代优化；
3. 屏障验证智能体：用SMT求解器对候选证书进行形式化验证，确保满足安全约束；
4. 迭代优化循环：验证失败时反馈错误信息，触发新一轮候选生成。

研究团队在BarrierBench上对比不同配置性能：

配置	Claude Sonnet 4	ChatGPT-4o
基线（单次提示）	41%	17%
完整框架	90%	46%
性能提升	+49%	+29%
Claude Sonnet 4在完整框架下成功率超90%，证明架构有效性，显示合理任务分解和工具集成可让LLM胜任专业化形式化验证任务。

项目使用Python实现，依赖包括：anthropic（调用Claude API）、sympy（符号数学计算）、z3-solver（SMT求解器）、numpy（数值计算）。代码结构清晰，含智能体定义、验证逻辑和数据集加载模块，开发者替换API密钥即可运行合成流程。

BarrierBench代表神经符号AI的重要应用方向，结合神经网络模式识别与符号推理严谨性，兼顾自动化与可验证性。对自动驾驶安全验证、机器人控制、工业控制系统、AI安全研究等领域有参考价值。随着LLM能力提升，类似智能体框架有望在更多科学工程领域结合人类专业知识与AI计算能力。