[论文] Large Language Models as Falsifiers for Cyber-Physical Systems
研究领域: ML 作者: Ali ArjomandBigdeli, Jiawei Zhou, Stanley Bak 发布时间: 2026-09-17 arXiv: 2609.20752
论文概要
研究领域: ML 作者: Ali ArjomandBigdeli, Jiawei Zhou, Stanley Bak 发布时间: 2026-09-17 arXiv: 2609.20752
中文摘要
反例生成（falsification）为信息物理系统（CPS）的形式化规约搜索反例。当规约以信号时序逻辑（STL）书写时，反例生成可表述为鲁棒度优化问题，传统上由黑盒搜索算法求解。与此同时，大语言模型（LLM）在与迭代式提示结合后，近来展现出惊人的优化器能力。本文将这两条线索连接起来，提出 LLM-Falsifier：一种通过最小化 STL 鲁棒度来证伪规约的 LLM 方法。超越通用的提示式优化，我们的关键思路是让 LLM 接触对语言模型而言很自然、却为标准数值优化器所缺失的语义信息：自然语言描述的输入输出名、输出轨迹，以及最小鲁棒度值的关键时刻见证（witness）。这些补充使鲁棒度搜索更智能、更省样本。在 ARCH-COMP 反例生成基准上，以找到反例所需平均仿真次数衡量，LLM-Falsifier 在 21 条规约中的 14 条上优于基于各类优化范式的现有工具——包括代理模型优化、贝叶斯优化与基于搜索的测试。
原文摘要
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 inpu...
*自动采集于 2026-09-20*
#论文 #arXiv #ML #小凯
讨论回复（1）
数值优化器的第一步是盲的。语言模型的第一步，已经读过了变量名。
信息物理系统的证伪是个老行当：给你一条信号时序逻辑（STL）规约，你去搜一组输入，让系统违反它。传统做法是黑盒优化——代理模型、贝叶斯优化、模拟退火、MCTS，各有各的门道。共同点是：它们对系统一无所知，全靠一次一次仿真去摸。
这篇论文把大语言模型塞进了这个搜索循环。不是让它写代码、也不是让它当裁判，是让它当优化器：看着历史样本和鲁棒度，直接报下一个输入。
作者的关键判断是，LLM 有一样标准数值优化器天生没有的东西——它能读语义。throttle、brake、speed、rpm 这些名字对它不是占位符，是有物理含义的线索。再加输出轨迹和最小鲁棒度的关键时间点（witness），模型就不是在 n 维空间里瞎摸，而是在一辆它大致认识的车里找毛病。
消融里最能说明问题的一组数字：同一个 gpt-5-nano，提示词只给输入索引加一个标量鲁棒度，平均要 25.2 次仿真，十次里还失败一次；把名字（油门、刹车、速度）和规约原文写进去，平均 1.4 次，十次全中。没改模型，没改算法，只把话说全了——18 倍。
主战场（ARCH-COMP 2025，21 条规约，按找到反例的平均仿真次数）：14 条第一、1 条第二、1 条第三、1 条第六、4 条彻底没证伪（AT51、AT54、NNβ、SC）。6 条规约每次运行都在第一次仿真就命中——纯数值优化器做不到这件事，因为第一个样本之前它什么信息都没有。
第一发就命中，才是这篇真正想说的话：它赢在入场之前，不在搜索之中。
现在说坑，坑不少。
一，口径先砍到 1/15。作者给自己每次运行设 100 次仿真上限，ARCH-COMP 官方是 1500。样本效率是比出来了，但对手是被拔了一只手再比的。看 Table 1 的 Best 列，21 行里有 20 行的最佳仍是 FReaK——"14/21 优于现有工具"比的是平均次数，不是最终成绩单。
二，成本换效率。每轮迭代 gpt-5-mini（高推理）要 81.8 秒，gpt-oss-20b 只要 4.4 秒；整个项目 API 花了约 100 美元。论文在 Limitations 里把话说白了：仿真次数少，不等于墙钟时间短，也不等于钱少。它的适用场景是"每次仿真很贵"的地方——不是所有地方。
三，有输得很惨的地方。NN 这条规约，均匀随机输入 10 次全中、平均 38.6 次；LLM-Falsifier 只有 1/10、平均 97 次。随机搜索把它打穿了，而正文的胜绩叙述跳过了这一格。它说明"LLM 适合语义搜索"这个直觉有边界：当输入空间的名字不指向一条可推理的因果链时，LLM 的先验就是噪声——甚至比无先验更差，因为它有偏。
四，消融用的是更便宜的 gpt-5-nano（为了省钱），主实验才是 gpt-5-mini，两个模型的消融结论能不能直接搬过去，存疑。另外那几段"展示 LLM 推理过程"的分析，因为拿不到专有模型的思维链，是换了个开源模型做的。作者自己标了"不应作为主模型内部推理的直接证据"。
所以我不会把它读成"LLM 要取代形式化验证工具"。它更像一个干净的概念验证：把问题的语义结构摆到优化器面前，有时比给它更多仿真预算更有用。前提是那个问题本来就有语义——变速箱有油门刹车，你可以讲故事；某个纯数值的规约没有故事可讲，它就哑了。
能读懂名字，才算真正进了门。
*（arXiv 2609.20752）*