Certified Grokking: a machine-checked certificate for the Nanda et al. modular-addition transformer
Neel Nanda, Lawrence Chan, Tom Lieberum, Smith, Jess, Jacob Steinhardt · arXiv (Cornell University) · 2023
A machine-checked, independently verifiable certificate chain for the modular-addition “grokking” transformer of Nanda et al. (arXiv:2301.05217). The checkpoint is theirs, unmodified and sha-pinned — state_dicts[400], epoch 40,000 — and the certified object is the exact-real function obtained by reading its published float32 tensors as exact dyadic rationals. Three links. A — Model == Task: the target logit exceeds every other class logit with a certified positive lower bound on all 113² = 12,769 inputs (minimum margin +9.2147), re-derived bit-identically by a torch-free checker. B — Ideal circuit == Spec: the ideal positive-weight cosine decoder computes (a + b) mod p, kernel-checked in Lean 4 with Mathlib, zero sorries, axioms exactly propext, Classical.choice, Quot.sound, and instantiated at the extracted circuit's exact coefficients. C — Circuit == Model: certified decision agreement, a certified residual audit, and certified decision transfer across the full domain. The headline finding is a negative one, reported in full: the extracted clock circuit is decision-complete but not margin-dominant. It accounts for every one of the model's 12,769 decisions, but the stronger uniform margin-dominance property we initially targeted is certified false for this checkpoint under the published five-mode Fourier-clock contract. The centred logits contain a small, structurally non-clock component that moves margins without changing decisions. This is a quantified statement about where an idealised interpretation and a real model part ways, published rather than quietly dropped. This is the second repository of three, continuing verified-circuits and continued by certified-inference. This record archives the repository as of 11 August 2026. The work was first made public on 2 July 2026; the DOI was minted later, so the archive date and the original publication date differ.