邁向可驗證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的發展奠定了基礎。