Certified Mechanistic Interpretability: Lifting Single-Input Findings to Bounded Neighbourhoods

Zhen Zhang; Yanliang Huang; Peng Xie; Wenyuan Wu; Amr Alanwar

cs.LGAug 17, 2026

Certified Mechanistic Interpretability: Lifting Single-Input Findings to Bounded Neighbourhoods

Authors: Zhen Zhang, Yanliang Huang, Peng Xie, Wenyuan Wu, Amr Alanwar

Organizations: School of Computation, Information and Technology Technical University of Munich, Germany

Abstract

Mechanistic interpretability reverse-engineers transformer circuits one input at a time, leaving observed mechanisms without guarantees over bounded input neighbourhoods. We address this gap with a framework based on constrained polynomial-zonotope (CPZ) propagation that lifts mechanistic-interpretability observations from a single input to certified statements over a bounded set of perturbations. Three internal-attention queries (top- $k$ stability, evidence mass, and attention entropy) are formulated as tractable programs over the simplex of attention weights, and CPZ propagation through transformer blocks is shown to preserve the softmax simplex and the LayerNorm zero-mean identity exactly. A recursive Jacobian zonotope construction extends the same certificates across layer depth by linearising the block stack at the input and avoids per-layer generator growth. We instantiate the framework on transformer attention; the resulting certificates offer a way to sharpen mechanistic statements that single-input inspection cannot resolve on its own, and to inform downstream decisions in regimes where empirical heuristics may be misleading.

Figures & tables

Figure 1: Pipeline overview. A post-embedding perturbation set around the clean input $z_{0}$ is encoded as a CPZ and propagated through the transformer. Top: $Q^{\top}K$ stays exact under CPZ algebra; softmax is tightened by the simplex constraint $\sum_{j}s_{ij}{=}1$ ; a recursive Jacobian–zonotope connector (§ 4.2 ) lifts bounds across layer depth. Bottom: the feasible attention polytope $R_{\epsilon}=\Delta_{S}\cap[\underline{s},\overline{s}]$ supports three certified queries Q1/Q2/Q3 (§ 3 ).

Figure 2:

\epsilon

-ball certification cannot distinguish BERT-tiny heads that a structured CPZ does. BERT-tiny SST-

2

Layer-

0

, three

5

-sentence paraphrase sets. Hatched bars (

\epsilon{=}0.002

ball, App. G.3 ): both heads saturated on Q1/Q2/Q3, indistinguishable. Solid bars (CPZ over the

5

-paraphrase polytope, construction in § 4.4 ): left Q1 top-

1

stability, H 0

43

–

57\%

vs. H 1

0

–

57\%

; middle Q2 evidence mass (

\tau{=}0.2

71\%

vs.

14

–

71\%

; right Q3 entropy width,

{\sim}0.68

vs.

0.88

–

1.41

nat.

Head	Clean	$5{\times}10^{-4}$	$10^{-3}$	$2{\times}10^{-3}$
$0.1^{*}$	$36/60$	$\mathbf{1.7}$	$\mathbf{0}$	$0$
$0.5$	$59/60$	$58$	$3$	$0$
$0.6$	$31/60$	$47$	$7$	$0$
$0.10^{*}$	$60/60$	$\mathbf{100}$	$\mathbf{95}$	$0$

Table 1: Per-head (left) and cross-head circuit (right) Q1 cert rates on the same

60

IOI prompts. ∗ marks Wang-classified DTHs. The Wang pair satisfies clean attention but not joint

\epsilon

-robustness; empirically-stable pairs/triples certify jointly at near-saturation.

Internal Layer queries (Q1 top- $1$ attention stability)
Setting	$\epsilon$	CPZ	MC	CROWN	IBP	sec/sample
Synthetic $d{=}8$ , Layer- $0$	$2{\times}10^{-2}$	$\mathbf{85.0}$	$85.0$	$72.5$	$57.5$	$<\!0.1$
BERT-tiny ( $d{=}128$ ), Layer- $1$	$2{\times}10^{-3}$	$\mathbf{92.5}$	$95.0$	$51.2$	$\phantom{0}3.8$	$0.7$
GPT- $2$ ( $d{=}768$ ), Layer- $0$	$1{\times}10^{-3}$	$\mathbf{70.2}$	$72.7$	$43.5$	$52.3$	$\sim\!5$
GPT- $2$ ( $d{=}768$ ), Layer- $1$	$1{\times}10^{-3}$	$\mathbf{47.9}$	$78.1$	$\phantom{0}0.2$	$26.9$	$\sim\!22$
GPT- $2$ medium ( $d{=}1024$ ), Layer- $1$	$5{\times}10^{-4}$	$\mathbf{41.1}$	$90.9$	$\phantom{0}0.8$	$10.7$	$\sim\!2700$

Table 2: Main results. Top-

1

attention/output stability (%) across model sizes; “–” = baseline does not apply at this scale. MC = MC+PGD, empirical upper bound. CROWN

<

IBP at GPT-

2

Layer-

1

as input-dependent argmax explodes CROWN’s softmax back-substitution at

d{=}768

(App. D.2 ).

95\%

Clopper–Pearson CIs in App. G.2 .

	$\epsilon{=}0.01$			$\epsilon{=}0.02$			$\epsilon{=}0.05$
Head	Q1	Q2	Q3	Q1	Q2	Q3	Q1	Q2	Q3
H0	$88$	$27$	$.021$	$72$	$25$	$.042$	$55$	$18$	$.105$
H1	$\mathbf{97}$	$\mathbf{68}$	$.027$	$\mathbf{97}$	$\mathbf{58}$	$.053$	$\mathbf{88}$	$\mathbf{48}$	$.134$

Table 3: CPZ per-head certified queries on the induction model (Step 2 of § 5 ;

\tau{=}0.3

for Q2 here vs.

\tau{=}0.2

elsewhere). H1’s attention is consistently stable (bold), H0’s is responsive within the ball; high stability here signals an inert head, since induction needs content-tracking attention. Q1/Q2 in %; Q3 in nat. IBP rows omitted: Q1/Q2 within

10

pp of CPZ, Q3 entropy bounds vacuous at

1.45

–

1.47

vs. CPZ’s

0.02

–

0.14

(

10

–

70{\times}

tighter).

Seed	42	2024	31415	271828	11	23	67	101	All-seed mean
CPZ-guided	100	80	100	90	100	100	100	100	$\mathbf{84.5}$
Gradient-guided	90	50	90	60	90	90	90	90	$78.5$
$\Delta$	$+10$	$+30$	$+10$	$+30$	$+10$	$+10$	$+10$	$+10$	$+6.0$

Table 4: Per-seed adversarial accuracy (%) under CPZ-guided vs. gradient-guided pruning across

20

seeds, restricted to disagreement seeds at

\epsilon{=}0.05

(

8/20

); rightmost column reports the all-seed mean. CPZ-guided pruning never underperforms gradient-guided (Wilcoxon signed-rank one-sided,

p{=}0.0042

Appendix figures & tables33 assets

Supplementary material from the paper’s appendix.

Appendix

Method	$\epsilon{=}0.01$	$\epsilon{=}0.02$	$\epsilon{=}0.05$	$\epsilon{=}0.1$
IBP + softmax	63.8	72.1	76.1	76.5
PZ + softmax (no CPZ)	0.88	7.6	127.5	2,767
CPZ (ours)	0.49	2.9	6.1	8.9
CPZ vs. IBP	99.2%	95.9%	92.0%	88.4%

Appendix

Table 5: Average output bound width after 2 encoder layers (5-sample avg). CPZ remains stable while baseline PZ+softmax explodes at large

\epsilon

	PZ+softmax		CPZ
Stage	$G_{I}$	Width	$G_{I}$	Width
L0 input	0	0.10	0	0.10
L0 attention	8	0.78	8	0.78
L0 LN1	16	0.37	16	0.37
L0 LN2	80	0.29	80	0.29
L1 attention	120	6.64	8	2.92

Appendix

Table 6: Independent generator count (

G_{I}

) and width at key stages (

\epsilon=0.05

). CPZ’s softmax constraint resets

G_{I}

from

120

8

at Layer 1 attention.

Configuration	$\epsilon{=}0.01$	$\epsilon{=}0.02$	$\epsilon{=}0.05$	$\epsilon{=}0.1$
IBP + softmax	63.7	71.7	76.2	76.6
PZ + softmax (no constraints)	1.10	11.5	196.7	4,481
+ LN constraint only	1.10	7.3	7.7	8.3
+ Softmax LP only	0.70	3.6	32.2	656
CPZ (both + LP)	0.70	4.5	7.3	7.6

Appendix

Table 7: Ablation of CPZ constraints (3-sample avg). At small

\epsilon

the softmax LP dominates; at large

\epsilon

the LN constraint prevents explosion.

		Q1 Top-1 (%)		Q2 Evidence (%)		Q3 Entropy W.
$\epsilon$	Layer	CPZ	MC	CPZ	MC	CPZ	MC
$0.005$	L0	$90.0$	$92.5$	$95.0$	$95.0$	$0.0015$	$0.0007$
	L1	$90.0$	$92.5$	$75.0$	$75.0$	$0.0059$	$0.0028$
	L2	$\mathbf{95.0}$	$95.0$	$87.5$	$87.5$	$0.0032$	$0.0015$
	L3	$\mathbf{85.0}$	$80.0$	$97.5$	$97.5$	$0.0005$	$0.0003$
$0.010$	L0	$90.0$	$90.0$	$95.0$	$95.0$	$0.0031$	$0.0015$

Appendix

Table 8: Multi-layer certification on the

4

-layer synthetic transformer (

5

samples,

40

queries per

(\epsilon,L)

). CPZ uses the recursive Jacobian-zonotope connector; MC uses

5{,}000

random samples plus

10{\times}50

PGD per query. CPZ matches MC within

0

–

7.5

pp on Q1 at every layer and

\epsilon

Target layer $L$	$\epsilon$	$R_{\mathrm{analytical}}$ (Prop. 7 )	$1.5\,\widehat{V}$ (production)	ratio
$1$	$0.005$	$1.15$	$4.6{\times}10^{-3}$	$0.40\%$
$1$	$0.010$	$2.29$	$3.0{\times}10^{-2}$	$1.33\%$
$2$	$0.005$	$10.74$	$1.3{\times}10^{-2}$	$0.12\%$
$2$	$0.010$	$21.49$	$5.8{\times}10^{-2}$	$0.27\%$
$3$	$0.005$	$124.68$	$6.1{\times}10^{-2}$	$0.05\%$
$3$	$0.010$	$249.36$	$2.2{\times}10^{-1}$	$0.09\%$

Appendix

Table 9: Analytical Lipschitz fallback (Prop. 7 ) vs. the sampled remainder used in production (

N_{\mathrm{jac}}{=}30

samples plus

1.5{\times}

safety factor) on the

4

-layer synthetic transformer (

d{=}8

\text{seq\_len}{=}4

n_{\mathrm{dim}}{=}32

). Across all six

(L,\epsilon)

settings, the production estimate is

\leq 1.33\%

of the analytical closed-form bound, validating that sampling is conservative against the worst-case Lipschitz envelope. Per-layer block Lipschitz contributions:

L_{0}{=}20.3

L_{1}{=}9.4

L_{2}{=}11.6

L_{3}{=}25.7

Model	Layer	$\epsilon$	Sequential CPZ	Jac connector	MC+PGD
Synthetic ( $d{=}8$ )	L2	$0.005$	$12.5$	$\mathbf{95.0}$	$95.0$
	L3	$0.005$	$\phantom{0}0.0$	$\mathbf{85.0}$	$80.0$
	L2	$0.010$	$\phantom{0}0.0$	$\mathbf{82.5}$	$90.0$
	L3	$0.010$	$\phantom{0}0.0$	$\mathbf{72.5}$	$75.0$
GPT- $2$ small (124M)	L1	$0.001$	$\phantom{0}0.0$	$\mathbf{47.9}$	$78.1$

Appendix

Table 10: Connector ablation: same model/

\epsilon

/query (Q1 top-

1

)/MC+PGD ground truth, only the inter-layer connector changes. Sequential CPZ collapses on every multi-layer cell; the recursive Jacobian-zonotope connector recovers all of them. (Referenced from § 4 .)

$\epsilon$	CPZ %	MC %	Mean margin	Agreement	Conservative	Unsound	Time/sample
$5{\times}10^{-4}$	$\mathbf{98.0}$	$99.0$	$1.53$	$99/100$	$1$	$\mathbf{0}$	$0.7$ s
$10^{-3}$	$\mathbf{97.0}$	$98.0$	$1.52$	$99/100$	$1$	$\mathbf{0}$	$0.7$ s
$2{\times}10^{-3}$	$\mathbf{95.0}$	$98.0$	$1.51$	$97/100$	$3$	$\mathbf{0}$	$0.7$ s

Appendix

Table 11: Output verification on BERT-tiny SST-2 (

100

samples, seq. length

8

d{=}128

, top-

256

Jacobian columns). Zero unsound certifications across

300

(sample,

\epsilon

) pairs. The CPZ-MC gap is

1

–

3

samples per

\epsilon

and consists of boundary cases (CPZ worst-case margin in

[-0.03,0]

); the residual gap is dominated by CORA order-reduction at the bilinear

Q^{\top}K

step and shrinks with larger

k

(§ 4.3 ).

$\epsilon$	CPZ %	MC %	Agreement	Conservative	Unsound	Time/sample
$5{\times}10^{-4}$	$\mathbf{98.0}$	$100.0$	$49/50$	$1$	$\mathbf{0}$	${\sim}22$ s
$10^{-3}$	$\mathbf{92.0}$	$96.0$	$48/50$	$2$	$\mathbf{0}$	${\sim}22$ s
$2{\times}10^{-3}$	$\mathbf{40.0}$	$90.0$	$25/50$	$25$	$\mathbf{0}$	${\sim}22$ s

Appendix

Table 12: Full-vocabulary next-token verification on GPT-2 (

124

M parameters,

50{,}257

vocab,

50

samples per

\epsilon

). CPZ certifies that the clean top-

1

token remains the argmax over the full vocabulary, combining a direct top-

K{=}20

check with a Lipschitz tail bound. Zero unsound certifications across

150

(sample,

\epsilon

) pairs.

	$\alpha$ -CROWN (surrogate, $N{=}10$ )			CPZ (original, $N{=}100$ )
$\epsilon$	cert. (%)	time/sample	unsound	cert. (%)	time/sample	unsound
$5{\times}10^{-4}$	$90$	$11.2$ s	$0$	$98$	$0.7$ s	$0$
$10^{-3}$	$90$	$11.2$ s	$0$	$97$	$0.7$ s	$0$
$2{\times}10^{-3}$	$80$	$12.1$ s	$0$	$95$	$0.7$ s	$0$

Appendix

Table 13:

\alpha

-CROWN [ 25 ] on a quick-GELU surrogate of BERT-tiny SST-2 (clean accuracy

90\%

N{=}10

); CPZ on the original BERT-tiny (clean accuracy

100\%

N{=}100

). Because the two columns evaluate different GELU activations, this is a baseline-availability check rather than a like-for-like comparison; see the surrounding text for caveats.

Model	$d$	Params	Bound Width	Time (s)	CPZ vs. IBP
$d{=}8,h{=}2$	8	1.2K	2.0	0.4	99.2% tighter
$d{=}16,h{=}2$	16	4.5K	12.8	0.7	—
$d{=}32,h{=}4$	32	17K	9.5	1.0	—
$d{=}64,h{=}4$	64	67K	105.9	1.8	—
$d{=}128,h{=}4$	128	265K	233	54	79.5% tighter

Appendix

Table 14: CPZ verification across model sizes (

\epsilon{=}0.01

). Verification time scales sub-quadratically in

d_{\text{model}}

and CPZ maintains meaningful bounds at 265K parameters. The

d{=}128

row uses the dedicated 10-sample run of Tab. 15 ; smaller models use a 3-sample sweep.

$\epsilon$	CPZ	IBP	Improvement
0.01	233.1	1,141.6	79.6%
0.02	234.3	1,141.6	79.5%
0.05	234.0	1,141.6	79.5%
0.10	234.3	1,141.6	79.5%

Appendix

Table 15: CPZ vs. IBP output bound width on the

d{=}128

model (10-sample average). CPZ consistently achieves

{\sim}5\times

tighter bounds.

$K_{J}$	Cert. rate (%)	Mean margin	sec/sample
$32$	$96.7$	$1.493$	$0.050$
$64$	$96.7$	$1.488$	$0.069$
$128$	$90.0$	$1.480$	$0.082$
$256$	$90.0$	$1.471$	$0.083$
$512$	$90.0$	$1.459$	$0.093$
$1024$	$90.0$	$1.452$	$0.114$

Appendix

Table 16:

K_{J}

-sweep on BERT-tiny SST-2 end-to-end output verification (

\epsilon{=}2{\times}10^{-3}

30

samples). The certified rate is stable at

90

–

96.7\%

across two orders of magnitude of

K_{J}

, so the BERT-tiny rate is not bottlenecked by Jacobian-zonotope truncation. The implication for GPT-

2

Layer-

1

is that the larger CPZ–MC gap there (

30.2

pp) reflects the absolute truncation ratio at

d{=}768

(

K_{J}{=}128

6{,}144

, retain

1/48

) rather than a structural limit of the construction.

	$\epsilon{=}0.01$			$\epsilon{=}0.02$			$\epsilon{=}0.05$
Model	MC	CPZ-marg.	C/I	MC	CPZ-marg.	C/I	MC	CPZ-marg.	C/I
$d{=}8,h{=}2$	92.5	92.5	67.5	85.0	85.0	57.5	60.0	60.0	12.5
$d{=}16,h{=}2$	95.0	95.0	60.0	82.5	82.5	32.5	57.5	57.5	0 5.0
$d{=}32,h{=}4$	81.2	81.2	45.0	73.8	73.8	20.0	46.2 †	45.0	0 0.0
$d{=}64,h{=}4$	81.2	81.2	25.0	68.8	68.8	0 1.2	30.0	30.0	0 0.0

Appendix

Table 17: Layer-

0

top-

1

stability across scales (

5

samples/cell, all heads). CPZ-marg. is exact (Theorem 1 ); MC = MC+PGD (

200

k corner-biased +

20{\times}50

); C/I = CROWN/IBP (coincide at Layer-

0

). CPZ-margin matches MC+PGD in

11/12

cells; the

12

th (

d{=}32,\epsilon{=}0.05

, † ) is verified by aggressive PGD as correct.

$\epsilon$	Method	Q1 Rank (%)	Q2 Evid. (%)	Q3 Ent. $\overline{H}$
0.001	MC	99.4	100.0	0.0040
	CPZ	99.4	100.0	0.0207
	IBP	97.5	100.0	0.0277
0.002	MC	99.4	100.0	0.0079
	CPZ	96.2	100.0	0.0415
	IBP	94.4	100.0	0.0556

Appendix

Table 18: Certified queries on BERT-tiny / SST-2 , Layer 0,

d{=}128

, 2 heads, 10 samples, 160 queries,

\tau{=}0.2

. CPZ dominates IBP, with the gap negligible at small

\epsilon

(both saturate) and widening at larger

\epsilon

. At

\epsilon{=}0.001

, CPZ matches MC+PGD exactly on Q1 at

99.4\%

. Q3 reports the worst-case entropy upper bound; lower is tighter.

$\epsilon$	Method	Q1 Rank $\uparrow$	Q2 Evid $\uparrow$	Q3 Ent $\downarrow$
0.002	MC+PGD	95.0	96.2	0.011
	CPZ	92.5	96.2	0.079
	CROWN	51.2	88.8	0.449
	IBP	3.8	20.0	1.401

Appendix

Table 19: Certified queries on BERT-tiny Layer 1 ,

d{=}128

, 2 heads,

\tau{=}0.2

80

certified queries per

\epsilon

(

5

samples

\times

2

heads

\times

8

query positions). All methods receive the same Jacobian-zonotope enclosure of Layer 0 output; they differ only in how Layer 1 attention is verified. CPZ stays within

2.5

pp of MC+PGD on Q1, while CROWN and IBP collapse on the bilinear

Q^{\top}K

product. The same BERT-tiny model is verified end-to-end on

100

samples per

\epsilon

in App. D.1 (zero unsound across

300

output verifications), confirming the internal-query picture at

20{\times}

larger sample size.

$\epsilon$	Method	Q1 Rank $\uparrow$	Q2 Evid $\uparrow$	Q3 Ent $\downarrow$
0.001	MC+PGD	72.7	89.0	0.049
	CPZ	70.2	95.4	0.044
	IBP	52.3	72.3	0.387
	CROWN	43.5	63.1	0.505
0.002	MC+PGD	54.4	76.2	0.095
	CPZ	50.2	94.2	0.089

Appendix

Table 20: Certified queries on GPT-2 , Layer 0,

d{=}768

, 12 heads, 5 samples, 480 queries. MC+PGD uses 200k random samples plus

20{\times}50

PGD restarts. CPZ Q1 nearly matches MC+PGD at

70.2\%

vs.

72.7\%

, and CPZ exceeds MC+PGD on Q2 at

95.4\%

vs.

89.0\%

because PGD finds adversarial perturbations that random sampling misses. CROWN underperforms IBP due to McCormick per-dimension cancellation loss; see text. PZ [ 1 ]

\equiv

CPZ at Layer 0 because no constraints are active before the first softmax.

$\epsilon$	Method	Q1 Rank $\uparrow$	Q2 Evid $\uparrow$	Q3 Ent $\downarrow$
0.001	MC+PGD	78.1	75.2	0.030
	CPZ	47.9	55.6	0.398
	IBP	26.9	36.5	0.773
	CROWN	0 0.2	0 1.9	1.458

Appendix

Table 21: Certified queries on GPT-2 Layer 1 (

d{=}768

\tau{=}0.2

480

certified queries per

\epsilon

5

samples

\times

12

heads

\times

8

query positions). The Jacobian zonotope connector enables CPZ to certify

47.9\%

Q1 at

\epsilon{=}0.001

, while CROWN collapses to

0.2\%

. MC+PGD budget per Tab. 36 .

$\epsilon$	Method	Q1 Rank $\uparrow$	Q2 Evid $\uparrow$	Q3 Ent $\downarrow$
$5{\times}10^{-4}$	MC+PGD	90.9	89.3	0.023
	CPZ	41.1	46.9	0.814
	IBP	10.7	26.0	1.185
	CROWN	0 0.8	0 3.6	1.736
$10^{-3}$	MC+PGD	83.1	87.5	0.044
	CPZ	13.5	13.5	1.380

Appendix

Table 22: Certified queries on GPT-2 medium Layer 1 (

d{=}1024

h{=}16

\tau{=}0.2

K_{J}{=}128

384

certified queries per row:

3

samples

\times

16

heads

\times

8

query positions). At both

\epsilon

values, CPZ remains the only sound method to certify a non-trivial fraction; CROWN/IBP collapse. The CPZ–MC gap narrows from

70

pp at

\epsilon{=}10^{-3}

50

pp at

\epsilon{=}5{\times}10^{-4}

, i.e., the degradation is graceful rather than catastrophic, consistent with the Jacobian-zonotope truncation budget shrinking as

\epsilon

shrinks. No MC-found adversarial contradicts a CPZ certification at either

\epsilon

$\epsilon$	Method	Q1 Rank $\uparrow$	Q2 Evid $\uparrow$	Q3 Ent $\downarrow$
0.001	MC+PGD	62.5	63.5	0.022
	CPZ	27.1	37.5	0.461
	IBP	21.9	29.2	0.756
	CROWN	0 4.2	16.7	1.247

Appendix

Table 23: Certified queries on GPT-2 small Layer 2 (

d{=}768

h{=}12

\tau{=}0.2

K_{J}{=}128

96

certified queries:

1

sample

\times

12

heads

\times

8

query positions;

2

encoder blocks propagated through the recursive Jacobian-zonotope connector). CPZ retains a

6.5{\times}

multiplicative lead over backward-CROWN at the second layer, demonstrating that the connector enables genuine multi-layer certification on a real pretrained transformer; the absolute CPZ–MC gap widens with depth, consistent with the same Jacobian truncation source as the Layer-

1

gap (Limitations (i)).

Framework	Internal Q	Simplex	$Q^{\top}K$ exact	LLM internal	Downstream
IBP / CROWN / DeepPoly [ 5 , 26 , 21 ]	$\times$	$\times$	$\times$	$\times$	$\times$
$\alpha$ -CROWN [ 25 ]	$\times$	$\times$	$\times$	$\sim$	$\times$
Transformer verifiers [ 19 , 2 ]	$\times$	$\times$	$\times$	$\times$	$\times$
PZ for transformers [ 13 ]	$\times$	$\times$	$\sim$	$\times$	$\times$
Compact proofs [ 6 ]	$\checkmark$	$\times$	—	$\times$	$\sim$
This work (CPZ-based)	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$

Appendix

Table 24: Capability matrix. Frameworks vs. five technical dimensions chosen to clarify the design space for internal-mechanism certification at pretrained scale.

\sim

= partial; cells reflect structural support, not evaluation strength.

		$\epsilon{=}5{\times}10^{-4}$			$\epsilon{=}10^{-3}$			$\epsilon{=}2{\times}10^{-3}$
Head	Clean ind.	Q1	Q2	Q3	Q1	Q2	Q3	Q1	Q2	Q3
$\boxed{H_{5}}$	$28/30$	$83$	$97$	$100$	$\mathbf{47}$	$\mathbf{90}$	$\mathbf{100}$	$0$	$13$	$13$
$\boxed{H_{10}}$	$30/30$	$100$	$100$	$100$	$97$	$100$	$100$	$\mathbf{73}$	$\mathbf{100}$	$\mathbf{0}$
$H_{6}$	$21/30$	$73$	$57$	$100$	$43$	$10$	$100$	$3$	$0$	$10$
$H_{8}$	$19/30$	$63$	$40$	$100$	$27$	$13$	$93$	$3$	$0$	$0$

Appendix

Table 25: GPT-2-small Layer-

0

Q1/Q2/Q3 cert rates on

30

induction-pattern prompts. The two boxed rows show heads with orthogonal failure modes:

H_{5}

fails Q1 while passing Q2 and Q3;

H_{10}

fails Q3 while passing Q1 and Q2.

	CPZ-guided		Gradient-guided		Full
$\epsilon$	Clean	Adv	Clean	Adv	Adv
$0.01$	$100$	$\mathbf{100}$	$100$	$100$	$100$
$0.02$	$100$	$\mathbf{100}$	$100$	$90$	$100$
$0.05$	$100$	$\mathbf{100}$	$100$	$90$	$100$

Appendix

Table 26: Certified pruning vs. gradient-guided pruning on the induction model (

d{=}8

h{=}2

; Step 3 of § 5 ). CPZ-guided pruning keeps the responsive H0 (whose attention tracks the duplicate token) and removes the stable-but-inert H1; gradient-guided pruning makes the opposite choice because H0 has near-zero input gradient. Both 1-head models reach

100\%

clean accuracy; the gap emerges only under adversarial perturbation.

$\epsilon$	Method	Q1 Rank $\uparrow$	Q2 Evid $\uparrow$	Q3 Ent $\downarrow$
$0.01$	MC+PGD	$92.5$	–	$0.0068$
	CPZ	$\mathbf{92.5}$	$\mathbf{20.0}$	$\mathbf{0.0091}$
	PZ	$90.0$	$20.0$	$0.0104$
	CROWN	$90.0$	$17.5$	$0.0105$
	IBP	$67.5$	$15.0$	$0.0200$
$0.02$	MC+PGD	$85.0$	–	$0.0136$

Appendix

Table 27: Certified mechanistic queries at Layer 0 (

d{=}8

h{=}2

S{=}4

5

samples,

40

queries per

\epsilon

). At this layer, attention scores are bilinear in the input, so CPZ, PZ, and CROWN achieve similar rates for Q2. The key differentiator is Q1: CPZ-margin (Theorem 1 ) matches the MC ground truth exactly at both

\epsilon

, while softmax-based methods (PZ, CROWN) drop to

72.5\%

\epsilon{=}0.02

$\epsilon$	Method	Q1 Rank $\uparrow$	Q2 Evid $\uparrow$	Q3 Ent $\downarrow$
$0.01$	MC+PGD	$87.5$	–	$0.0064$
	CPZ	$\mathbf{85.0}$	$\mathbf{5.0}$	$\mathbf{0.0113}$
	PZ	$57.5$	$5.0$	$0.0174$
	CROWN	$60.0$	$5.0$	$0.0161$
	IBP	$0.0$	$0.0$	$1.3863$
$0.02$	MC+PGD	$80.0$	–	$0.0130$

Appendix

Table 28: Certified mechanistic queries at Layer 1 (same model). Scores are propagated through the full Layer 0 pipeline. CPZ-margin maintains

85.0\%

Q1 at

\epsilon{=}0.01

(within

2.5

pp of MC), while CROWN drops to

60.0\%

and PZ to

57.5\%

. IBP collapses to

0\%

entirely. The Layer-0

\to

Layer-1 degradation is

4{\times}

smaller for CPZ (

-7.5

pp) than for CROWN (

-30

pp).

$\epsilon$	MC+PGD	CPZ-margin	CROWN
$0.005$	$95.0$	$\mathbf{95.0}$	$87.5$
$0.010$	$86.2$	$\mathbf{86.2}$	$67.5$
$0.020$	$68.8$	$\mathbf{68.8}$	$33.8$
$0.030$	$52.5$	$\mathbf{52.5}$	$\phantom{0}8.8$
$0.040$	$37.5$	$\mathbf{37.5}$	$\phantom{0}3.8$
$0.050$	$28.8$	$\mathbf{28.8}$	$\phantom{0}1.2$

Appendix

Table 29: Certified Layer-

0

top-

1

attention stability on a

d{=}16

h{=}2

model with

10

samples and

160

queries per row. MC+PGD : corner-biased sampling combined with PGD, providing an upper bound on the true stable fraction. CPZ-margin : direct scalar margin sign check via Theorem 1 , bypassing softmax. CROWN : auto-LiRPA backward CROWN on the bilinear

Q^{\top}K

score model. CPZ-margin matches MC+PGD across all

6

\epsilon

values, while remaining

7.5

–

44

pp tighter than CROWN across the sweep.

		Ranking (top-1)			Cross-head circuit
Model	$\epsilon$	MC	CPZ	IBP	MC	CPZ	IBP
Induction	$0.01$	$92.5$	$\mathbf{85.8}$	$79.2$	$85.0$	$\mathbf{71.7}$	$58.3$
Induction	$0.05$	$71.7$	$\mathbf{63.3}$	$44.2$	$48.3$	$\mathbf{35.0}$	$11.7$
$d{=}16$	$0.01$	$91.2$	$\mathbf{90.0}$	$57.5$	$82.5$	$\mathbf{80.0}$	$32.5$
$d{=}16$	$0.05$	$57.5$	$\mathbf{41.2}$	$\phantom{0}3.8$	$40.0$	$\mathbf{15.0}$	$\phantom{0}0.0$

Appendix

Table 30: Certified ranking preservation and cross-head circuit rates (%). Ranking preservation requires all pairwise orderings within the top-

1

set to be invariant; cross-head requires all heads to simultaneously certify top-

1

stability. CPZ dominates CROWN/IBP, with the gap widening at larger

\epsilon

Model	$\epsilon$	MC+PGD	CPZ	CROWN/IBP
Induction	$0.01$	$0.0183$	$\mathbf{0.0237}$	$0.0472$
Induction	$0.05$	$0.0924$	$\mathbf{0.1196}$	$0.2515$
$d{=}16$	$0.01$	$0.0052$	$\mathbf{0.0097}$	$0.0342$
$d{=}16$	$0.05$	$0.0260$	$\mathbf{0.0490}$	$0.1879$

Appendix

Table 31: Certified attention entropy interval width (Prop. 3 ). Smaller is tighter. The simplex-constrained CPZ bounds are

50

–

74\%

narrower than IBP, and track the MC+PGD reference width closely at small

\epsilon

Metric	Head 0	Head 1
Ablation accuracy drop	$0.0$ pp	$0.0$ pp
Input gradient norm $\\|\partial L/\partial x\\|_{2}$	$2.7{\times}10^{-6}$	$0.131$
Clean attention entropy	$1.69$	$1.58$
Attention mass on key token	$0.26$	$0.38$
Cosine similarity between heads	$0.81$

Appendix

Table 32: Empirical interpretability metrics on clean inputs of the induction model. All standard tools either find no difference (ablation) or point to the wrong pruning decision: gradient pruning would remove H0 (its norm is

{\sim}5{\times}10^{4}{\times}

smaller), but H0 is the content-responsive head whose attention tracks the duplicate. CPZ certification (Step 2) reveals this structural distinction.

$\epsilon$	H0 flipped	H1 flipped	Ratio	H0 entropy shift
$0.01$	$3.3\%$	$0.0\%$	–	$0.003$
$0.02$	$6.7\%$	$3.3\%$	$2.0\times$	$0.006$
$0.05$	$18.3\%$	$5.0\%$	$3.7\times$	$0.016$

Appendix

Table 33: Adversarial validation: PGD confirms CPZ’s stability prediction. The CPZ-responsive H0 shows

2.5

–

3.7\times

more attention flips under PGD than the CPZ-stable H1.

Disagreement seeds at $\epsilon{=}0.02$ (6/20)
Seed	42	2024	31415	271828	23	89	All-seed mean
CPZ-guided	100	90	100	100	100	100	$87.0$
Gradient-guided	90	60	90	60	90	90	$81.5$
$\Delta$ (CPZ $-$ grad)	$+10$	$+30$	$+10$	$+40$	$+10$	$+10$	$+5.5$

Appendix

Table 34: Per-seed adversarial accuracy (%) under CPZ-guided vs. gradient-guided pruning across

20

seeds, including the

\epsilon{=}0.02

disagreement block (the

\epsilon{=}0.05

block is in main-body Tab. 4 ). CPZ-guided pruning never underperforms gradient-guided pruning at either

\epsilon

	Layer 0		Layer 1
Method	$\epsilon{=}0.01$	$\epsilon{=}0.02$	$\epsilon{=}0.01$	$\epsilon{=}0.02$
MC+PGD	$2$	$2$	$13$	$9$
CPZ	$0.5$	$0.5$	$237$	$195$
PZ	$0.5$	$0.5$	$237$	$195$
CROWN	$0.5$	$0.5$	$6$	$6$
IBP	$0.3$	$0.3$	$2$	$2$

Appendix

Table 35: Per-sample verification time (seconds) on single CPU core, averaged over

5

samples. CPZ’s Layer-

1

cost is dominated by the encoder-layer CPZ propagation; the three certified queries add

<1

s overhead. The Layer-

1

CPZ time is non-monotone in

\epsilon

because the L-BFGS-B inner solver terminates earlier on the wider score-margin landscapes at larger

\epsilon

(per-sample times:

\epsilon{=}0.01

149/250/268/257/259

;

\epsilon{=}0.02

262/190/186/168/170

). Peak memory:

{\sim}120

MB (CPZ),

{\sim}80

MB (CROWN),

{\sim}30

MB (IBP).

Setting	Random samples	PGD restarts $\times$ steps
Synthetic $d{=}8$ Layer- $0$ / Layer- $1$	$500$ k corner-biased	$20\times 50$
4-layer synthetic (multi-layer)	$500$ k corner-biased	$20\times 50$
BERT-tiny SST- $2$ output verification	$2{,}000$	$5\times 30$
BERT-tiny / GPT- $2$ Layer- $0$ Q1/Q2/Q3	$1{,}000$ – $5{,}000$ corner-biased	$10\times 30$ – $50$
GPT- $2$ Layer- $1$ (Jacobian-zonotope)	$5{,}000$	$10\times 50$
GPT- $2$ next-token (full vocab + tail)	$2{,}000$	$10\times 50$ targeted

Appendix

Table 36: MC+PGD budgets per setting. “Random samples” includes corner-biased + uniform mix where applicable; PGD restarts

\times

steps targeted at top-

1

flips.

	P10	P25	P50	P75	P90
NN $\ell_{\infty}$ distance	0.072	0.093	0.106	0.119	0.134

Appendix

Table 37:

\ell_{\infty}

distance between BERT-tiny token embeddings and their nearest vocabulary neighbor. The minimum distance is

0.030

, so our

\epsilon{=}0.001

–

0.002

corresponds to

3

–

7\%

of the closest discrete token swap; against the median distance of

0.106

the same range is

1

–

2\%

. This is the regime where gradient-based adversaries operate.

Explore similar work

Towards Verifiable Transformers: Solver-Checkable Circuit Explanations
May 21, 2026Neel SomaniNeural Network Verification Transformer
Independent Researcher
Interior interpretability with attention rollout: contraction and propagation profiles in Transformers
Jul 24, 2026Umberto Biccari, Qian Huang, Enrique ZuazuaTransformer Interpretability Transformer
Align, Unify, Suppress, Route: A Coherentist View of Transformer Computation
Aug 22, 2026Nura Aljaafari, Andre FreitasTransformer Interpretability Mechanistic Interpretability
University of Manchester, United Kingdom · Idiap Research Institute, Switzerland

May 21, 2026J/K move · Enter open · S save

Towards Verifiable Transformers: Solver-Checkable Circuit Explanations

Neel Somani

Independent Researcher

Neural Network Verification Transformer Mechanistic Interpretability

Open paper AskPDF arXiv

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.

Abstract

Explore similar work

Towards Verifiable Transformers: Solver-Checkable Circuit Explanations

Interior interpretability with attention rollout: contraction and propagation profiles in Transformers

Align, Unify, Suppress, Route: A Coherentist View of Transformer Computation