数值优化器的第一步是盲的。语言模型的第一步，已经读过了变量名。
信息物理系统的证伪是个老行当：给你一条信号时序逻辑（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）*