🤖 machine learning

Synthesis and Verification of Transformer Programs (Technical Report)

本文提出了新的算法技术，通过利用与 Lustre 模型检测和局部搜索的关联，自动验证和学习 C-RASP 程序——即捕捉 Transformer 表达能力的语言构造——从而推动 Transformer 程序优化和约束学习的应用。

原作者： Hongjian Jiang, Matthew Hague, Philipp Rümmer, Anthony Widjaja Lin

发布于 2026-05-19

📖 1 分钟阅读☕ 轻松阅读

原作者： Hongjian Jiang, Matthew Hague, Philipp Rümmer, Anthony Widjaja Lin

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你拥有一个非常聪明、强大的机器人（一个"Transformer"），它能阅读故事、撰写邮件并解决谜题。这个机器人极其擅长它的工作，但它也是一个"黑箱”。你可以看到它做了什么，却难以看清它是如何思考的，也无法证明它绝不会犯某个特定的错误。

本文提出了一种为这些机器人构建蓝图的新方法。作者没有试图直接理解机器人那混乱、复杂的大脑，而是创造了一种更简单、更清晰的语言，称为C-RASP。可以将 C-RASP 视为机器人遵循的“简化版操作手册”。它足够简单，让我们能够阅读、理解并检查其中的错误；同时又足够强大，能够精确描述机器人的行为。

以下是他们两项主要成就的分解说明，辅以日常类比：

1. “安全检查员”（验证）

问题： 你拥有一份 C-RASP 操作手册（即一个程序），你想知道：“这个程序是否始终做正确的事？它是否会接受错误的词，或拒绝正确的词？”手动检查这一点，就像试图在一本百万页的书中寻找一个拼写错误——这几乎不可能，有时在数学上甚至无法做到百分之百确定。

解决方案： 作者构建了一个“安全检查员”。他们找到了一种将这些 C-RASP 操作手册翻译成另一种非常严格的语言Lustre的方法。

类比： 想象你有一份写在凌乱手写笔记本里的复杂食谱（C-RASP）。你很难直接检查其中的数学计算是否正确。于是，你将这份凌乱的食谱翻译成一种僵硬的、计算机可读的格式（Lustre），让一个超高速机器人（“模型检测器”）能够瞬间读取。
结果： 这个机器人可以瞬间扫描食谱，并回答：“是的，这是安全的”，或者“不，错误就发生在这一步”。论文表明，这种方法的速度极快（仅需几秒钟），而训练一个新的 AI 机器人则可能需要数小时。

2. “自动编辑器”（合成）

问题： 假设你有一份示例列表（例如：“这些是好的句子，这些是坏的”），你希望写出一份符合这些示例的 C-RASP 操作手册。你还没有这份手册；你必须从零开始发明它。

解决方案： 作者创建了一个“自动编辑器”，它使用了一种称为模拟退火的技术。

类比： 想象你正在寻找制作蛋糕的完美配料组合，但在烤好之前你无法品尝。
1. 你从一个随机、凌乱的食谱开始。
2. 你烤制它，看看它是否符合你的示例。
3. 如果它很接近，你就做一个微小的改动（用蜂蜜代替糖，加一撮盐）。
4. 如果新蛋糕更好，你就保留它。如果它更差，你可能仍然会保留它（以防它最终能导向一个更好的蛋糕），但随着你越来越接近完美食谱，你会逐渐停止冒险。
结果： 这个过程会自动编写出一份完美符合你示例的 C-RASP 程序。这就像拥有一位仅凭品尝最终成品就能逆向工程出食谱的厨师。

为什么这很重要（根据论文）

作者在各种“谜题”（如检查括号是否平衡或统计字母数量）上测试了他们的工具。

速度： 他们的工具在几秒钟内就解决了这些谜题。
对比： 他们指出，如果你尝试训练一个标准 AI（如 GPT-2）从零开始学习这些相同的谜题，可能需要数小时，而且仍然可能无法正确完成。
两个有趣的用途：
1. 最小化： 如果你有一份庞大、臃肿的操作手册，他们的工具可以将其缩减为仍能有效工作的最小、最简版本。
2. 约束学习： 如果你对该程序应做什么有一个初步想法（即一个“规范”），他们的工具可以填补空白，确保最终程序既符合你的示例，又符合你的规则。

简而言之： 这篇论文提供了一种方法，将 AI 神秘的“黑箱”转化为清晰、可检查且可编辑的操作手册，使我们能够比以往更快地验证其安全性并构建新的程序。

技术摘要：Transformer 程序的合成与验证

问题陈述

Transformer 作为大语言模型（LLM）的基础架构，以其难以进行形式化分析而闻名。尽管它们具有强大的表达能力且可并行化，但验证其属性是不可判定的，且引入思维链（Chain of Thoughts）后，它们甚至变得图灵完备。为解决这一问题，研究人员开发了声明式语言，如 RASP（受限访问序列处理语言）及其变体 C-RASP（计数 RASP），旨在以精确的语义捕捉 Transformer 的行为。

然而，尽管 C-RASP 与 Transformer 之间存在理论联系，仍存留两个关键缺口：

验证：目前尚无自动验证 C-RASP 程序的方法。在一般情况下，检查一个 C-RASP 程序是否识别某种平凡语言是不可判定的，且缺乏实用工具来分析语言等价性或包含性等属性。
合成：目前尚无已知方法能从示例中自动学习或合成 C-RASP 程序。现有方法依赖于训练神经网络并提取规则，这往往无法生成可实现的翻译，或需要理想化的假设。

本文通过开发针对 C-RASP 程序验证与合成的首个自动技术，解决了上述挑战。

方法论

1. 通过归约至 Lustre 进行验证

作者建立了 C-RASP 与 Lustre（一种用于嵌入式系统的同步数据流语言）之间的形式化联系。

翻译：将 C-RASP 程序翻译为 Lustre 节点。该翻译将 C-RASP 规则映射为 Lustre 变量（布尔型和整数流）。
- 计数算子：C-RASP 的计数算子 #φ（计算满足 φ 的位置数量）在 Lustre 中通过辅助整数变量进行模拟，这些变量在无限流上累积数值。
- 有限与无限：由于 C-RASP 操作于有限词，而 Lustre 操作于无限流，输入被编码为带有特定流结束标记（#）和永恒标记（Ω）的无限流。
模型检测：一旦翻译完成，语言等价性、包含性和空性等属性即可利用最先进的模型检测器（特别是 Kind2）结合优化的 SMT 求解器（CVC5, Z3）进行验证。
复杂度：只要 #rs,re 算子中的范围参数采用一元编码，该翻译在规模上即为多项式级。

2. 通过模拟退火进行合成

本文提出了一种基于 模拟退火 的局部搜索算法，用于从正负示例中合成 C-RASP 程序。

状态空间：搜索被限制在由布尔规则数量（ $N_b$ ）、计数规则数量（ $N_c$ ）以及数值常数上限（ $K$ ）定义的固定“程序形状”内。
变异算子：算法通过对当前程序应用语法变异来探索状态空间。这些变异包括：
- 重采样：完全替换规则的右侧。
- 微变异：局部更改，如交换逻辑连接词、切换否定或翻转比较的严格性。
- 约束：变异被限制在浅层语法片段中（例如，计数表达式的深度为 2），以引导搜索偏向简单、可解释的模型。
目标函数：评分函数 $E(P)$ 优先最小化误分类（ $\lambda_{mis}$ ），随后惩罚不可达规则（ $\lambda_U$ ）和抽象语法树的总大小（ $\lambda_S$ ）。
退火动力学：该算法以依赖于冷却温度调度表的概率接受较差的解，从而使其能够跳出局部最优。

3. 集成应用

作者将这两个组件集成到一个统一框架中，支持两种应用：

Transformer 程序最小化：给定一个 C-RASP 程序，该系统合成一个结构更小且等价的程序。它在局部搜索与等价性检查之间交替进行；验证器提供的反例指导搜索过程。
约束学习：给定部分规范（一个 C-RASP 程序 $P_{spec}$ ）和带标签的示例，该系统合成一个既符合示例又包含于 $P_{spec}$ 语言中（ $L(P) \subseteq L(P_{spec})$ ）的程序。

主要贡献

首个自动验证方法：本文提出了通过归约至 Lustre 并利用模型检测来自动验证 C-RASP 程序的首个技术。这使得语言等价性、包含性和空性的验证成为可能。
首个自动合成方法：作者引入了一种局部搜索算法（模拟退火），能够直接从示例中合成 C-RASP 程序，无需中间神经网络的训练。
实现与基准测试：实现了一个统一的 Scala 工具链，并针对文献中的一套基准测试进行了评估，包括正则语言、基于计数的语言以及上下文无关风格的语言。

实验结果

作者在包含 Dyck-1、Majority 以及各种 Tomita 自动机语言的基准测试套件上评估了其工具。

效率：该工具在 300 秒的超时限制内，成功为大多数基准测试合成了正确的 C-RASP 程序。例如，合成 Dyck-1 的程序耗时约 3.92 秒，而 AnBnCn 耗时 80.05 秒。
准确性：在 C-RASP 表达能力范围内的语言上，合成实现了高训练和评估准确率（通常达到 100%）。
与 Transformer 的比较：论文指出，对于某些基准测试，训练一个 Transformer（例如通过 HuggingFace 的 GPT-2）以达到正确的语言可能需要数小时，而 C-RASP 合成工具则在数秒内完成了任务。
局限性：正如可表达性理论所预期的，超出 C-RASP 能力的语言（例如 Parity、Tomita 3、Tomita 5）无法以高准确率被学习，最佳训练准确率保持在 80% 以下。

意义与主张

本文将 C-RASP 定位为不仅是理解 Transformer 表达能力的理论工具，更是一种 可解释的代理模型。通过提供自动验证和合成方法，作者认为 C-RASP 可以利用形式化方法（FXAI）进行分析，从而弥合神经网络的“黑盒”性质与可解释性需求之间的鸿沟。

其意义在于：

实践中的可判定性：尽管一般性验证是不可判定的，但归约至 Lustre 提供了一条实用的、自动化的路径，用于验证特定的、现实世界的 Transformer 行为。
直接合成：合成方法提供了一条直接生成可解释程序的途径，避免了训练深度神经网络的不稳定性或晦涩性。
优化：最小化现有 Transformer 程序并在约束下学习它们的能力，展示了 C-RASP 在程序细化和安全关键应用中的实用性。

作者总结道，他们的工作为 Transformer 的形式化分析奠定了基础，未来的方向包括鲁棒性验证以及思维链（CoT）机制的整合。