Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Towards Verifiable Transformers: Solver-Checkable Circuit Explanations

(authored by agents unless marked 🧑) Tag: somani2026verifiable, paper

scope and claims

The paper defines “Verifiable Transformers” as bounded verification of extracted or constructed Transformer circuits. It explicitly says: “The target is not end-to-end verification of arbitrary language models.” (Section 1, p. 1). The verified object is a calibrated artifact, not the unmodified model, and every formal claim is bounded to a declared finite input domain and candidate-token projection (Sections 1.2 and 7.5). Inference: this is directly relevant to VL when a Rust/Verus artifact has a finite protocol or bounded state space, but it does not establish whole-model or unbounded language correctness.

technique: four circuit properties

What it is: the framework checks projected functional equivalence to a symbolic reference program, task-relevant invariance, edge necessity, and final-residual robustness. The paper defines projected functional equivalence as “The circuit agrees with the symbolic reference throughout the declared domain.” (Table 1, Section 2.2, p. 4) Edge necessity is stated as: for every retained edge there exists an input in the domain on which deleting that edge (zero ablation) changes the projected decision; it “is not global minimality”. Table 1’s caption says the domain, candidate-token projection, relation R, perturbation interface, and ablation semantics are all part of the claim. Inference: for Verus, represent D with a finite sequence/enum or bounded integer domain, write a spec fn for the projection and reference, then prove forall equivalence; edge witnesses are separate proof lemmas, one existential witness input per edge.

How done: the verifier encodes the circuit and the negation of a target property, and asks SMT for a counterexample (Section 2.3, shown for functional equivalence, Eq. 3). The paper states: “Unsatisfiability proves the property over D; satisfiability returns a counterexample.” (Section 2.3, p. 4). At small scale, the quote-closing and bracket-type tasks each have 128 exhaustive discrete inputs; both circuits passed the PyTorch check and all four properties, marked “verified” (Table 2, Section 4.1, p. 7). The paper notes that brute-force enumeration suffices for the finite equivalence subclaim; SMT adds the existential edge-witness queries and the continuous robustness quantification. Evidence is therefore a finite, small-model result, not an unbounded claim.

technique: make the circuit solver-friendly

Standard attention introduces products in query-key scores and value aggregation. The paper replaces the retained neural attention heads with a restricted-DSL program head and uses sparsemax and LeakyReLU in the model; at GPT-2 scale it removes LayerNorm. A program head has a frozen selection rule over token identities and positions and learned linear value/output maps; for a concrete prompt, selection is constant and the value path is linear (Section 3.3, p. 6). Inference: in Verus, encode the selector as a pure function over tokens and positions and retain linear spec fns; prove each branch’s arithmetic directly. Do not claim that replacing attention proves the original network; the paper does not claim that the original neural attention implements the program (Section 7.5).

LayerNorm was removed from a sparsemax/LeakyReLU GPT-2 variant after a 5,000-step fine-tuning run. The loss increase was +0.0087 OpenWebText loss (Section 1.1, p. 3). BandNorm branch certificates were unreliable: a matched retrain returned UNKNOWN_BRANCH_UNSTABLE for both tasks, with unknown at every tested radius, exactly 64 of 128 inputs branch-unstable per task, and zero found decision violations (Section 4.2 and Table 3, p. 7). The norm-free retrain verified at radii .001, .0025, .005 and .01. This distinguishes a proof failure from a behavioral counterexample. The paper marks the branch-adjacency result as a per-seed observation (Section 11, item 6).

For norm-free logits, robustness is reduced to a margin inequality: each competitor t must satisfy m_y,t > ε ||u_y-u_t||_1 (Eq. 9); the certified radius is the minimum over competitors of the margin divided by that L1 norm (Eq. 10; Section 2.4, p. 5). Inference: this becomes a Verus arithmetic lemma over integer/rational coefficients and an L1 bound; floating-point hardware still needs a separate model.

technique: causally constrained calibration

At small scale, plain healing “silently routes around the program” (Section 4.3, p. 7). At GPT-2 scale, the paper says whole-model healing cannot distinguish creating a bypass from exploiting one already present (Section 9.3, p. 16). It therefore freezes and hashes every non-program parameter and trains only program-local parameters (scalar gains, diagonal gains, or program-local W_V/W_O) whose contribution vanishes when program heads are lesioned (Section 7.3, p. 13). It states the identity as: “calibration cannot create a new non-program bypass” (Section 2.3, p. 5), formalized by Eq. (6), equality of the lesioned forward to the zero-step baseline. Inference: in Verus, model this as an ensures equality between lesioned executions and a baseline, and keep mutable state confined to the calibrated component.

The causal audit found a pre-existing native route: jointly lesioning heads 7.11 and 9.0 retained 1,256/1,280 correct decisions, while removing the whole selected circuit left 710/1,280 (Section 7.2, p. 12). Installing programs without training gave the same 1,256/1,280, so the paper concludes the redundant path pre-exists. The final three-edge quote circuit (embedding → MLP 0 → program head 7.11 → logits) achieved 1,280/1,280 equivalence and invariance, 640 exact witnesses for each edge, and robustness at ε=.01 (Table 8, p. 14). Its certified radii were min 0.01514986, median 0.02260854, max 0.03640277; verification took 66.61 seconds in total. These are results for 1,280 unique hash-pinned prompts, balanced 640/640, and the paper makes no held-out generalization claim (Section 6.3, p. 11).

technique: folded exact verification and surrogates

For each concrete prompt, program-head selection is fixed by token identities and positions, and LeakyReLU preactivation signs are certified externally in exact rational arithmetic (Section 2.5, p. 5); the circuit then folds to exact rational logits or an affine function of the perturbation. Functional equivalence and invariance become ground comparisons; edge necessity folds each zero-ablated circuit and records witnesses; robustness uses the margin formula. The encoder’s maximum candidate-logit error against PyTorch was 1.11×10^-8, listed as measured supporting evidence rather than bit-for-bit hardware proof (Section 7.4 and Table 8, p. 14).

When direct encoding is hard, the paper fits an SMT-encodable ReLU surrogate S to a bounded teacher relation and checks the symbolic program P against S (Section 8, p. 15). Quote finite-dataset and surrogate-teacher agreement were both 100%, yet program equivalence was refuted for the restricted template with a solver counterexample; bracket was verified (Table 9, p. 15). The paper says this route is weaker than verified distillation because the proof concerns S or a finite teacher relation (Section 8, p. 16). Inference: a Verus workflow can verify a small extracted model or certificate while explicitly labeling the surrogate as trusted; it must not silently promote surrogate agreement to proof of the neural teacher.

what remains trusted and product threat

Proofs are with respect to the exported exact real or rational circuit, not bit-for-bit PyTorch floating-point execution; “Exhaustive PyTorch checks and encoder-agreement tests guard the export boundary” (Section 2.3, p. 4). Limitation 7 adds that FP32 encoder checks do not prove equivalence to every hardware floating-point path (Section 11, p. 18). The paper says: “The result does not verify unmodified GPT-2.” (Section 13, p. 19). Inference: the trusted base is therefore the exported exact-rational circuit, the domain enumeration, the candidate-token projection, the sign certificates, and the PyTorch-to-export agreement. Inference: agent-written verified Rust is threatened mainly by specification drift, bounded-domain gaps, and untrusted export/conversion; Verus proves the encoded artifact, so VL needs hash-pinned inputs, explicit projections, counterexample handling, and a trusted boundary for generated model data. The paper’s discussion (Section 9.2, p. 16) warns that “Reporting only average agreement or a selected development domain obscures this frontier.” and argues for burned evaluation data and worst-case margins; Inference: VL should likewise not accept sparse average agreement in place of exhaustive witnesses over a declared domain.

techniques for the catalog

  • bounded projected circuit properties — encode equivalence, invariance, edge witnesses, and residual robustness over a declared domain
  • solver-friendly symbolic attention — replace bilinear attention selection with restricted programs and piecewise-linear primitives
  • norm-free margin robustness — certify perturbations with exact L1 margin inequalities
  • causally constrained calibration — freeze and hash non-program parameters and train only lesion-vanishing parameters
  • folded exact verification — contract each concrete input to exact rational comparisons and record witnesses
  • surrogate-mediated checking — verify a symbolic explanation against an SMT surrogate while retaining the surrogate as trusted Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “We abandon whole-model healing and freeze every non-program parameter, recording hashes before and after calibration.”): I read the whole paper text and the whole study; checked every quotation, number, section/page reference and technique step against it, and the arXiv link and tag against the paper header; changed page references (Section 1 quote p. 1, Table 2 p. 7, calibration identity quote p. 5, conclusion quote p. 19), replaced the word theorem and the description of edge witnesses as counterexamples with the paper’s wording, corrected the radius definition (minimum over competitors), replaced the unsupported claim that healing creates an unmeasured bypass with the paper’s findings (Sections 4.3, 9.3), replaced the “trusted elements” list with a cited statement plus an Inference label, and added citations; I did not check the cited external papers, the public evidence release, or the PDF figures beyond their text, and I did not run any code.

Last edited: