迈向可验证Transformer：用求解器验证电路解释的正确性
可解释性研究在AI领域日益重要，但现有方法多依赖示例、消融实验和人工推理来验证对模型内部电路的解释，缺乏严格证明。最新研究论文《Towards Verifiable Transformers: Solver-Checkable Circuit Explanations》提出了一种新框架，将Transformer电路转化为求解器可检查的有界命题，从而实现对电路功能的正式验证。
核心思路：用SMT求解器验证电路
该框架名为Verifiable Transformers，其核心思路是：针对特定行为、有限任务域和候选token投影，提取任务电路，然后利用SMT（可满足性模理论）求解器验证多种属性，包括投影功能等价性、边必要性、任务相关不变性和最终残差鲁棒性。
当电路中包含难以精确或高效编码的算子时，研究者提出替代中介验证方法：先训练一个SMT可编码的替代模型，在有限域上验证其与原始电路的一致性，再对替代模型进行符号验证。这种方法扩展了验证的适用范围。
实验验证：从符号任务到GPT-2规模
论文在两类场景中验证了框架的有效性：
小规模符号序列任务：训练了一个使用Signed L1 BandNorm、sparsemax注意力和LeakyReLU的GPT风格Transformer，并提取了用于引号闭合和括号类型追踪的稀疏电路。通过直接SMT编码，成功穷举验证了投影功能等价性、内容不变性、边必要性和最终残差鲁棒性。
GPT-2规模：相同算子堆栈在OpenWebText上稳定训练，但直接SMT验证仍不可行。然而，通过替代中介验证，研究者对难以编码的注意力电路进行了验证，既得到了可证明的符号解释，也发现了求解器生成的反例。
意义与局限
该工作的目标并非对完整模型进行验证，而是提供一条具体路径，将机制性电路解释转化为可证明或可反驳的形式化命题。这弥补了“找到合理电路”与“证明电路功能”之间的鸿沟。
当前局限在于：直接SMT验证仅适用于小规模模型和特定算子组合；替代中介验证虽然扩展了适用性，但替代模型的训练和验证本身也需额外成本。不过，该方法为AI可解释性提供了更严谨的数学基础，有望推动安全关键场景下Transformer的可信应用。