Towards Verifiable Transformers: Solver-Checkable Circuit Explanations

• URL: http://arxiv.org/abs/2605.24033v1
• Date: Thu, 21 May 2026 05:21:40 GMT
• Title: Towards Verifiable Transformers: Solver-Checkable Circuit Explanations
• Abstract summary: We introduce Verifiable Transformers, a framework for converting task-localized Transformer circuits into bounded, solver-checkable claims.<n>We instantiate direct verification with a GPT-style architecture using Signed L1 BandNorm, sparsemax attention, and LeakyReLU.<n>We also demonstrate surrogate-mediated verification on task-localized circuits with hard-to-encode attention.
• Score: 0.23689955632456092
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Can Language Model Agents be Helpful Circuit Explainers in Mechanistic Interpretability? [17.61177889205537]
  We introduce AgenticInterpBench, a benchmark for circuit explanation built from 84 semi-synthetic transformer circuits.<n>We propose HyVE (Hypothesize,, Explain), an agentic explainer that analyzes each component through an iterative loop of observation, hypothesis generation, and causal validation.<n>Across four LM backbones, HyVE recovers useful component- and task-level explanations, but no backbone is uniformly best.
  arXiv  Detail & Related papers  (2026-06-23T00:04:31Z)
• Demystifying Variance in Circuit Discovery of LLMs [51.97489679448601]
  We develop a new circuit discovery method that substantially lessens resampling variance.<n>We show that rephrasing variance arises because prompts with different templates tend to activate different circuits in the model.<n>We argue that sparsity, which has been claimed to form more compact and interpretable task circuits, fails to solve this problem.
  arXiv  Detail & Related papers  (2026-06-15T16:25:07Z)
• DifFRACT: Diffusion Feature Reconstruction and Attribution for Circuit Tracing [8.306039957986394]
  We extend transcoder-based circuit tracing to multimodal diffusion transformers.<n>We find mechanisms underlying attribute binding and cross-stream semantic propagation.<n>Our results provide causal explanations for systematic generation errors.
  arXiv  Detail & Related papers  (2026-06-14T13:02:44Z)
• Seeing Through Circuits: Faithful Mechanistic Interpretability for Vision Transformers [54.2202951543048]
  We investigate whether useful mechanistic circuits can be identified through computational graphs in vision transformers.<n>We propose an effective method for Automatic Visual Circuit Discovery (Vi-CD) that recovers class-specific circuits for classification.<n>We find that insightful and actionable edge-based circuits can be recovered from vision transformers, adding transparency to the internal computations of these models.
  arXiv  Detail & Related papers  (2026-04-15T23:25:46Z)
• Residual Connections and the Causal Shift: Uncovering a Structural Misalignment in Transformers [9.617245548268437]
  Large Language Models (LLMs) are trained with next-token prediction, implemented in autoregressive Transformers.<n>This creates a subtle misalignment: residual connections tie activations to the current token, while supervision targets the next token.<n>We propose a lightweight residual-path mitigation based on residual attenuation, implemented either as a fixed-layer intervention or as a learnable gating mechanism.
  arXiv  Detail & Related papers  (2026-02-16T14:04:42Z)
• Explaining the Explainer: Understanding the Inner Workings of Transformer-based Symbolic Regression Models [3.7957452405531265]
  We introduce PATCHES, an evolutionary circuit discovery algorithm that identifies compact and correct circuits for symbolic regression.<n>Using PATCHES, we isolate 28 circuits, providing the first circuit-level characterisation of an SR transformer.
  arXiv  Detail & Related papers  (2026-02-03T13:27:10Z)
• Weights to Code: Extracting Interpretable Algorithms from the Discrete Transformer [65.38883376379812]
  We propose the Discrete Transformer, an architecture engineered to bridge the gap between continuous representations and discrete symbolic logic.<n> Empirically, the Discrete Transformer not only achieves performance comparable to RNN-based baselines but crucially extends interpretability to continuous variable domains.
  arXiv  Detail & Related papers  (2026-01-09T12:49:41Z)
• Measuring Uncertainty in Transformer Circuits with Effective Information Consistency [0.0]
  We develop a sheaf/cohomology and causal emergence perspective to Transformer Circuits.<n>EICS combines (i) a normalized sheaf inconsistency computed from local Jacobians and activations, with (ii) a Gaussian EI proxy for circuit-level causal emergence.<n>We provide practical guidance on score interpretation, computational overhead (with fast and exact modes), and a toy sanity-check analysis.
  arXiv  Detail & Related papers  (2025-09-08T18:54:56Z)
• Position-aware Automatic Circuit Discovery [59.64762573617173]
  We identify a gap in existing circuit discovery methods, treating model components as equally relevant across input positions.<n>We propose two improvements to incorporate positionality into circuits, even on tasks containing variable-length examples.<n>Our approach enables fully automated discovery of position-sensitive circuits, yielding better trade-offs between circuit size and faithfulness compared to prior work.
  arXiv  Detail & Related papers  (2025-02-07T00:18:20Z)
• Complex Event Recognition with Symbolic Register Transducers: Extended Technical Report [51.86861492527722]
  We present a system for Complex Event Recognition based on automata. Our system is based on an automaton model which is a combination of symbolic and register automata. We show how SRT can be used in CER in order to detect patterns upon streams of events.
  arXiv  Detail & Related papers  (2024-07-03T07:59:13Z)
• Circuit Transformer: A Transformer That Preserves Logical Equivalence [20.8279111910994]
  We introduce a generative neural model, the "Circuit Transformer", which produces logic circuits strictly equivalent to given Boolean functions.<n>A Markov decision process formulation is also proposed for optimizing certain objectives of circuits.
  arXiv  Detail & Related papers  (2024-03-14T03:24:14Z)
• Learning Bounded Context-Free-Grammar via LSTM and the Transformer:Difference and Explanations [51.77000472945441]
  Long Short-Term Memory (LSTM) and Transformers are two popular neural architectures used for natural language processing tasks. In practice, it is often observed that Transformer models have better representation power than LSTM. We study such practical differences between LSTM and Transformer and propose an explanation based on their latent space decomposition patterns.
  arXiv  Detail & Related papers  (2021-12-16T19:56:44Z)
• On the Power of Saturated Transformers: A View from Circuit Complexity [87.20342701232869]
  We show that saturated transformers transcend the limitations of hard-attention transformers. The jump from hard to saturated attention can be understood as increasing the transformer's effective circuit depth by a factor of $O(log n)$.
  arXiv  Detail & Related papers  (2021-06-30T17:09:47Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.