Towards Verifiable Transformers: Solver-Checkable Circuit Explanations
This paper introduces a framework called Verifiable Transformers that converts task-localized Transformer circuits into bounded, solver-checkable claims. It employs direct verification for exactly encodable operators and surrogate-mediated verification for complex ones, demonstrating exhaustive verification on small symbolic tasks and applicability at GPT-2 scale, aiming to formalize mechanistic circuit explanations into provable or refutable propositions.
Article intelligence
Key points
- Proposes a framework to convert task-localized Transformer circuits into bounded, solver-checkable claims.
- Uses direct verification and surrogate-mediated verification for different operator types.
- Achieves exhaustive verification on small symbolic tasks and shows feasibility at GPT-2 scale.
- Aims to turn mechanistic circuit explanations into formal propositions that can be proven or refuted.
Why it matters
This matters because proposes a framework to convert task-localized Transformer circuits into bounded, solver-checkable claims.
Technical impact
May affect model selection, inference cost, product capability, and evaluation benchmarks.
[2605.24033] Towards Verifiable Transformers: Solver-Checkable Circuit Explanations
[Submitted on 21 May 2026]
Title:Towards Verifiable Transformers: Solver-Checkable Circuit Explanations
View a PDF of the paper titled Towards Verifiable Transformers: Solver-Checkable Circuit Explanations, by Neel Somani
View PDF HTML (experimental)
Abstract:Mechanistic interpretability often identifies circuits inside Transformer models, but explanations of those circuits are usually validated through examples, ablations, and manual reasoning. This leaves a gap between finding a plausible circuit and proving what the circuit does. We introduce Verifiable Transformers, a framework for converting task-localized Transformer circuits into bounded, solver-checkable claims. Given a behavior, a finite task domain, and a candidate-token projection, we extract a task circuit and verify properties such as projected functional equivalence, edge necessity, task-relevant invariance, and final-residual robustness. Direct verification encodes the extracted circuit itself into an SMT solver. When a circuit contains operators that are not exactly or tractably encodable, surrogate-mediated verification fits an SMT-encodable surrogate, validates it against the extracted circuit over the bounded domain, and verifies symbolic explanations against the surrogate. We instantiate direct verification with a GPT-style architecture using Signed L1 BandNorm, sparsemax attention, and LeakyReLU. On small symbolic sequence tasks, we train an SMT-representable Transformer, extract sparse circuits for quote closing and bracket type tracking, and exhaustively verify projected functional equivalence, content invariance, edge necessity, and final-residual robustness. At GPT-2 scale, the same operator stack trains stably on OpenWebText, although naive direct SMT verification remains intractable. We also demonstrate surrogate-mediated verification on task-localized circuits with hard-to-encode attention, showing both verified symbolic explanations and solver-generated counterexamples. The goal is not full-model verification, but a concrete path for turning mechanistic circuit explanations into formal propositions that can be proven or refuted.
Subjects:
Machine Learning (cs.LG); Logic in Computer Science (cs.LO)
Cite as: arXiv:2605.24033 [cs.LG]
(or arXiv:2605.24033v1 [cs.LG] for this version)
https://doi.org/10.48550/arXiv.2605.24033
arXiv-issued DOI via DataCite (pending registration)
Submission history
From: Neel Somani [view email] [v1] Thu, 21 May 2026 05:21:40 UTC (30 KB)
Full-text links:
Access Paper:
View a PDF of the paper titled Towards Verifiable Transformers: Solver-Checkable Circuit Explanations, by Neel Somani
View PDF
HTML (experimental)
TeX Source
view license
Current browse context:
cs.LG
new | recent | 2026-05
Change to browse by:
cs cs.LO
References & Citations
NASA ADS
Google Scholar
Semantic Scholar
Loading...
Data provided by:
Bibliographic Tools
Bibliographic and Citation Tools
Bibliographic Explorer Toggle
Bibliographic Explorer (What is the Explorer?)
Connected Papers Toggle
Connected Papers (What is Connected Papers?)
Litmaps Toggle
Litmaps (What is Litmaps?)
scite.ai Toggle
scite Smart Citations (What are Smart Citations?)
Code, Data, Media
Code, Data and Media Associated with this Article
alphaXiv Toggle
alphaXiv (What is alphaXiv?)
Links to Code Toggle
CatalyzeX Code Finder for Papers (What is CatalyzeX?)
DagsHub Toggle
DagsHub (What is DagsHub?)
GotitPub Toggle
Gotit.pub (What is GotitPub?)
Huggingface Toggle
Hugging Face (What is Huggingface?)
ScienceCast Toggle
ScienceCast (What is ScienceCast?)
Demos
Demos
Replicate Toggle
Replicate (What is Replicate?)
Spaces Toggle
Hugging Face Spaces (What is Spaces?)
Spaces Toggle
TXYZ.AI (What is TXYZ.AI?)
Related Papers
Recommenders and Search Tools
Link to Influence Flower
Influence Flower (What are Influence Flowers?)
Core recommender toggle
CORE Recommender (What is CORE?)
IArxiv recommender toggle
IArxiv Recommender (What is IArxiv?)
Author
Venue
Institution
Topic
About arXivLabs
arXivLabs: experimental projects with community collaborators
arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.
Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.
Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.
Which authors of this paper are endorsers? | Disable MathJax (What is MathJax?)