Large Language Models as Falsifiers for Cyber-Physical Systems
作者: Ali ArjomandBigdeli, Jiawei Zhou, Stanley Bak
分类: eess.SY, cs.AI, cs.LO, cs.SE
发布日期: 2026-09-17
备注: 22 pages, 5 figures, 3 tables
💡 一句话要点
提出LLM-Falsifier以解决网络物理系统的反例搜索问题
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 网络物理系统 反例搜索 鲁棒性优化 大型语言模型 信号时序逻辑 自动化测试 智能优化
📋 核心要点
- 现有的反例搜索方法在处理复杂的网络物理系统时效率低下，尤其是在鲁棒性优化方面。
- 本文提出LLM-Falsifier，通过利用大型语言模型的语义理解能力，优化反例搜索过程。
- 实验结果表明，LLM-Falsifier在ARCH-COMP基准测试中显著减少了找到反例所需的模拟次数，表现优于多种现有工具。
📝 摘要（中文）
反例搜索旨在寻找网络物理系统（CPS）中形式规范的反例。通过使用信号时序逻辑（STL）编写的规范，反例搜索可以被形式化为一个鲁棒性优化问题，传统上采用黑箱搜索算法来解决。近年来，大型语言模型（LLMs）在结合迭代提示时表现出意想不到的优化效果。本文提出LLM-Falsifier，一种基于LLM的方法，通过最小化STL鲁棒性度量来反例化规范。与通用的基于提示的优化不同，我们的关键思想是向LLM提供自然语言输入和输出名称、输出轨迹及关键时间见证等语义信息，从而实现更智能和更高效的鲁棒性搜索。在ARCH-COMP反例搜索基准测试中，LLM-Falsifier在21个规范中有14个的平均模拟次数上超越了现有的基于多种优化范式的反例搜索工具。
🔬 方法详解
问题定义：本文解决的是网络物理系统中反例搜索的鲁棒性优化问题。现有方法通常依赖黑箱搜索算法，效率较低，尤其在复杂系统中难以找到有效反例。
核心思路：论文的核心思路是利用大型语言模型的语义信息，通过自然语言输入和输出，增强反例搜索的智能性和样本效率。通过最小化STL鲁棒性度量，LLM-Falsifier能够更有效地探索反例空间。
技术框架：整体架构包括数据输入模块、LLM处理模块和输出生成模块。数据输入模块负责接收规范和初始条件，LLM处理模块则利用语言模型进行鲁棒性优化，最后输出生成模块提供反例或优化结果。
关键创新：最重要的技术创新在于将语言模型的语义理解能力引入反例搜索中，使得模型能够处理自然语言信息，而不仅仅依赖于数值优化。这一设计使得反例搜索更加高效和智能。
关键设计：在模型设计中，采用了特定的提示策略来引导LLM进行鲁棒性优化，并设置了合适的损失函数以反映STL鲁棒性度量。此外，关键时间见证的引入也增强了模型的搜索能力。
🖼️ 关键图片
📊 实验亮点
实验结果显示，LLM-Falsifier在ARCH-COMP反例搜索基准测试中，平均模拟次数在21个规范中有14个超越了现有的反例搜索工具，展现出显著的性能提升。这表明该方法在鲁棒性优化方面具有更高的效率和有效性。
🎯 应用场景
该研究的潜在应用领域包括自动驾驶、智能制造和机器人控制等网络物理系统。在这些领域中，确保系统的安全性和可靠性至关重要，LLM-Falsifier能够有效地帮助开发者验证系统的行为是否符合预期规范，降低系统故障风险，提升安全性。
📄 摘要（原文）
Falsification searches for counterexamples to formal specifications in cyber-physical systems (CPS). With specifications written in Signal Temporal Logic (STL), falsification can be formulated as a robustness optimization problem, traditionally tackled with black-box search algorithms. In parallel, large language models (LLMs) have recently emerged as surprisingly effective optimizers when coupled with iterative prompting. In this work, we connect these ideas and introduce LLM-Falsifier, an LLM-based approach that falsifies specifications by minimizing the STL robustness degree. Beyond generic prompt-based optimization, our key idea is to expose the LLM to semantic information that is natural for language models but absent from standard numerical optimizers, including natural-language input and output names, output trajectories, and critical-time witnesses for the minimum robustness value. These additions enable smarter and more sample-efficient robustness search. On the ARCH-COMP falsification benchmarks, LLM-Falsifier is shown to outperform existing falsification tools based on a range of optimization paradigms, from surrogate-based and Bayesian optimization to search-based testing, on 14 of 21 specifications when measured by the average number of simulations required to find a counterexample.