迈向可验证Transformer：可求解器检查的电路解释
该论文提出了“可验证Transformer”框架，将局部任务Transformer电路转化为有界、可求解器检查的命题，通过直接验证和替代中介验证两种方法，在小型符号序列任务上实现了对电路属性的穷举验证，并在GPT-2规模上展示了替代中介验证的有效性，旨在为机械论解释提供形式化证明路径。
文章情报
要点
- 提出可验证Transformer框架，将任务局部电路转化为有界、可求解器检查的命题。
- 采用直接验证和替代中介验证两种方法，处理可精确编码或难以编码的算子。
- 在小型符号任务上实现穷举验证，在GPT-2规模上展示替代中介验证的实用性。
- 目标不是完全模型验证，而是为机械论电路解释提供可证明或反驳的形式化命题。
为什么重要
这条新闻值得关注，因为提出可验证Transformer框架，将任务局部电路转化为有界、可求解器检查的命题。
技术影响
可能影响模型选型、推理成本、产品能力和评测基准。
一篇新论文《Towards Verifiable Transformers: Solver-Checkable Circuit Explanations》（迈向可验证Transformer：可求解器检查的电路解释）提出了一个框架，旨在将Transformer模型内部的电路解释转化为形式化、可由求解器检查的命题。这项工作由Neel Somani完成，于2026年5月21日提交至arXiv。
当前，机械论可解释性方法通常识别出模型内部的电路，但验证这些电路解释大多依赖于示例、消融实验和人工推理，缺乏严格的证明。该论文引入的“可验证Transformer”框架填补了这一空白，通过将任务局部电路编码为有界、可由SMT（可满足性模理论）求解器检查的声明，实现了对电路属性的形式化验证。
该框架包含两种验证方法：直接验证和替代中介验证。直接验证适用于电路中所有算子均可精确且可处理地编码的情况，例如使用Signed L1 BandNorm、sparsemax注意力和LeakyReLU的GPT风格架构。替代中介验证则用于电路中包含难以编码的算子（如注意力机制）时，通过拟合一个可SMT编码的替代模型，在有限域内验证其与提取电路的一致性，再对替代模型进行符号解释验证。
研究者在小型符号序列任务（如引号闭合、括号类型跟踪）上训练了SMT可表示的Transformer，并穷举验证了投影功能等价性、内容不变性、边必要性和最终残差鲁棒性等属性。在GPT-2规模上，相同的算子堆叠在OpenWebText上训练稳定，但直接SMT验证仍然难以处理。论文展示了替代中介验证在难以编码注意力机制的电路上的应用，既获得了验证的符号解释，也生成了求解器提供的反例。
论文强调，其目标并非对整个模型进行完全验证，而是提供一条具体路径，将机械论电路解释转化为可证明或反驳的形式化命题，从而增强可解释性的严谨性和可靠性。这项工作在cs.LG和cs.LO领域均有影响，为未来可验证AI的发展奠定了基础。