Kernel-checkable mechanistic circuits for learned transformers.
▶ Start here: the explainer notebook — an executed, figure-rich walkthrough (trained model → extracted circuit → the mechanism made visual → the certificate running → the Lean theorem → the trust story → verify it yourself). Reads top-to-bottom on GitHub with all outputs inline.
Train a tiny transformer on a complete finite task, reverse-engineer it into a human-readable symbolic circuit, and ship independently-checkable evidence that
Spec == Circuit == Model over the entire input domain
— not on sampled prompts, but on every input, with a positive decision margin, backed by a kernel-checked proof of the circuit↔spec half.
We take a tiny transformer, trained from scratch on a complete finite language task — bracket matching over every input up to length 16 — and close the full chain of guarantees around it. A machine-checked Lean proof shows that the symbolic circuit we extracted computes the task's specification for all lengths, and a rigorous interval-arithmetic certificate shows that the circuit reproduces the trained model's decision on every one of the 65,536 inputs. Both halves are re-checkable by anyone, from the artefacts alone, without trusting our code or any machine-learning library.
Why it matters: interpretability claims are usually sampled and statistical — "the model does X on the prompts we tried". This is a working demonstration that, in the right setting, such claims can instead be theorems and certificates: statements that hold over the whole domain and that a sceptic can verify for themselves.
Said plainly and honestly: the model is deliberately tiny and the task deliberately simple. The contribution is not scale — it is the complete, checkable chain from specification to circuit to trained weights, with each link's trust level named.
Recent work pairs mechanistic interpretability with formal guarantees — Gross, Agrawal et al. (NeurIPS 2024) prove compact performance lower bounds; Hadad, Katz, Bassan (2026) certify circuit robustness / minimality. Neither ships a kernel-checked circuit-to-spec equivalence for a learned algorithm over the whole finite domain, as a reproducible artefact a skeptic can verify without trusting our Python. That is the gap this repo targets.
The same approach was subsequently carried over to a model we did not train: the published Nanda et al. modular-addition "grokking" checkpoint. There it produces a full-domain certificate over the model's decisions, a Lean theorem for the ideal clock decoder, and an empirical finding about where the celebrated "clock" interpretation actually ends — it is decision-complete but not margin-dominant. The two efforts are complementary: this repo is a length-generic Lean induction on a self-trained model, giving the cleanest fully end-to-end chain; certified-grokking takes an unmodified, widely studied external checkpoint and reports a new empirical finding on it.
| Milestone | State |
|---|---|
| A1 — a tiny transparent transformer learns the task to exact 100% over the full domain, positive margins | ✅ done (Dyck-1, n=10 & n=12, all seeds) |
A2 — extract a symbolic circuit; certify Circuit == Model argmax on every input |
✅ done (mechanism probed; rigorous rational margin ≥ +6.3957 on all 1,024 inputs) |
B — Lean 4 proof ∀ s, Circuit.valid s = Spec.isValid s (by induction) |
✅ done (kernel-checked, Lean core only; axioms [propext, Quot.sound]) |
| Scale to n=16 (headline domain, 65,536 inputs) | ✅ done (exact 100%; Circuit == Model rigorous margin ≥ +8.0950 on all 65,536) |
See docs/PROGRESS.md for results and docs/design.md
for the full plan.
Dyck-1 / balanced parentheses, fixed length n. Tokens (=0, )=1. A string
is valid iff its running depth never goes negative and ends at 0 — i.e. it
genuinely requires the order check, not just a parenthesis count. The spec is
vcirc/dyck.py (verified against the Catalan numbers).
vcirc/ # the package:
# dyck.py (spec) · model.py (TinyTransformer) · train.py
# circuit.py (extracted symbolic circuit)
# certify.py (Circuit == Model: v1 evidence + v2 proof)
# exact.py (torch-free rigorous interval-arithmetic core)
# export_weights.py (exact float.hex() weight export)
models/ # exact trained checkpoints (tiny; committed for reproducibility)
tests/ # pytest: spec vs Catalan; model exact; circuit == model certificate
experiments/ # activation cache + probes (depth/violation/aggregation)
docs/ # design.md (plan + relation to prior work), PROGRESS.md (results)
proofs/ # (B) Lean 4 project: Circuit == Spec (proved; `lake build` green)
certificates/ # (A2) emitted certificates + check.py (standalone re-verifier)
pip install -e . # torch (CPU) + this package
pip install -e '.[notebook]' # extra: matplotlib + scikit-learn + jupyter (to re-run the explainer)
python -m vcirc.train --n 10 --seeds 6 # train; saves an exact model to models/
python -m pytest # spec correctness + saved model is exact
# A2 — certify Circuit == Model over the whole domain
python -m vcirc.certify --rung v1 # exhaustive float32 evidence
python -m vcirc.certify --rung v2 --jobs 4 # rigorous rational margin bound
python certificates/check.py \
certificates/dyck10_exact_seed0.v2.cert.json # torch-free re-verificationThe end-to-end claim Spec == Circuit == Model is three links at three
different trust levels. They are not equally strong, and "kernel-checked" applies
to exactly one of them — we name all three so a sharp reviewer doesn't have to ask.
| Link | How | Trust level | Scope |
|---|---|---|---|
Circuit == Spec |
Lean 4 theorem, by induction | kernel-proven (Lean kernel + propext, Quot.sound) |
all lengths |
Circuit == Model |
rigorous interval-arithmetic certificate | machine-checked rational bound (stdlib + ~390-line interval core) | per-input, n=10 & n=16 |
| Lean/Python defs ↔ same algorithm | faithful transcription | corroborated, not proven | binary {(, )} alphabet |
Circuit == Spec(Milestone B).∀ s, Circuit.valid s = Spec.isValid s, proved by structural induction (not enumeration), so it holds for every length — n=16 and all others.#print axiomsreports onlypropext, Quot.sound(nosorry, nonative_decide, no Mathlib — Lean core only), so a skeptic trusts only the Lean kernel. Reproduce:cd proofs && lake build. (Mathlib-free is a speed/reproducibility/auditability choice, not a soundness one — the kernel checks Mathlib just the same.)Circuit == Model(Milestone A2). We certify the deployed model directly: float32 weights are exact dyadic rationals and inputs are integers, so there is no "rounded model" to bridge to. The exact-real function the weights define hasargmax == Circuit.eval(x)with a strictly positive decision margin on every input — rigorous interval arithmetic (rational endpoints, directed/outward rounding; the only transcendental,expin the two attention softmaxes, enclosed by a Taylor+remainder bound; scale1/√dh = 1/4exact). Rational margin lower bound ≥ +6.3957 fordyck10_exact_seed0;certificates/check.pyre-verifies it from the weight export alone (Python stdlib + the ~390-linevcirc/exact.pycore; no torch, no training/extraction code). The literal float32 run is corroborated exhaustively by the v1 certificate. Certified at n=10 (margin ≥ +6.3957) and the headline n=16 (full 65,536-input domain, rigorous margin ≥ +8.0950, endpoint bits ≤ 108 at 96-bit precision).- Lean/Python defs ↔ the same algorithm (the transcription). The Lean
Spec/Circuitare faithful images ofvcirc/dyck.py/vcirc/circuit.py— but this link is corroborated, not formally proven (Python is not a formal object, so it cannot be). The corroboration is strong and multi-pronged: (1) the Lean spec reproduces the Catalan numbers[1,0,1,0,2,0,5,0,14,0,42]— it is validated against what Dyck-1 mathematically is, independent of anydyck.pybug; (2) circuit == spec on every string up to length 12; (3) an independent line-by-line audit (Codex / GPT-5.5) against cited Python line numbers; (4) each Lean definition cites the Python lines it mirrors. Scope: the model's binary{(, )}token alphabet (proofs/README.md§Scope).
Stated honestly: we do not claim "we proved a neural network is correct" unqualified. The circuit↔spec equivalence is kernel-proven for all lengths; the exact-real function these weights define provably makes the circuit's decision (margin > 0) on every input [n=10 and n=16, portable, rigorous], with the float32 execution corroborated exhaustively; and the one unavoidable soft seam — that our Lean and Python transcribe the same algorithm — is corroborated, not proven. The novelty is the mechanism + exact checkability, not the accuracy number.
See docs/FAQ.md for the full reviewer FAQ — how to self-verify,
the three corroboration claims, how it differs from Gross et al. / Hadad et al., and
honest limitations.
This repository was executed AI-first: Claude (Anthropic) operated as the researcher-engineer in an agentic loop — selecting the approach, writing the code and the Lean proofs, and drafting the write-up — with GPT-5.5 (OpenAI Codex) used for adversarial review passes at the design gates. Brian Naughton directed the project, made the judgement calls, reviewed the outputs, and takes responsibility for the repository. The point of naming all this is that the claims above are meant to be judged by the reproducible artefacts — the Lean kernel, the exhaustive certificate, the independent checker — and not by trust in any model-generated text. None of the adversarial review here is a substitute for human peer review.
Peer review is genuinely invited. If you find an error — in the mathematics, the code, the Lean statements, or the framing — please open an issue; corrections and failed replications are the most useful contributions this project can receive.
I am also looking for AI research and engineering roles: Brian Naughton on LinkedIn.
MIT — see LICENSE.