大型语言模型作为赛博物理系统的证伪器

证伪是在赛博物理系统（CPS）中寻找形式化规范的反例。当规范以 Signal Temporal Logic（STL）编写时，证伪可以被表述为鲁棒性优化问题，传统上使用黑盒搜索算法来处理。与此同时，大型语言模型（LLMs）最近在与迭代提示相结合时，展现出令人惊讶的高效优化能力。在这项工作中，我们将这些思想联系起来，并提出 LLM-Falsifier，一种基于 LLM 的方法，通过最小化 STL 鲁棒性程度来证伪规范。除了通用的基于提示的优化之外，我们的核心思想是向 LLM 暴露语义信息，这些信息对语言模型而言是自然的，但在标准数值优化器中并不存在，包括自然语言输入和输出名称、输出轨迹，以及最小鲁棒性值的关键时间见证。这些补充使得鲁棒性搜索更加智能且样本效率更高。在 ARCH-COMP 证伪基准测试中，以找到反例所需的平均仿真次数衡量，LLM-Falsifier 在 21 个规范中的 14 个上被证明优于基于多种优化范式的现有证伪工具，这些范式包括基于替代模型的优化、Bayesian optimization 以及基于搜索的测试。