Formalizing Hopfield Networks and Boltzmann Machines in Lean 4

This episode examines "Backprop as Functor," which argues that gradient descent on a whole network equals the composition of the gradient-descent learners of its parts. It defines a learner as four pieces: a parameter space, an implementation, an update, and a "request" function. The request tells an upstream module what input it should have received, and this supplies the missing intermediate training target. The discussion explains the categorical machinery in plain terms (categories, functors, monoidal structure, and the Para and Learn categories). It presents the main theorem: a faithful, strong symmetric monoidal functor sends parametrised functions to gradient-descent learners, with the request given by backprop. The episode compares this to difference target propagation, which only approximates backprop, and to lenses and open games, where the request plays the role of the backward "put". It notes that the paper has no experiments and asks whether the formalism does more than restate the fact that the chain rule is functorial. It then starts a worked quadratic-error example showing why the composite update matches plain gradient descent. Listeners get a clear view of what a compositional treatment of backprop does and does not buy.

This episode explores a 2021 formal proof, in the Lean theorem prover, that decision stumps (one-threshold classifiers) are PAC learnable. It starts from a simple learner that places its threshold at the largest positively labeled training point, so it can only err by calling true positives negative. The discussion explains why formalizing this on the real line is hard. Probability over uncountable spaces needs sigma-algebras and measurability, which textbooks skip, and the Giry monad lets the formal statement stay close to the pencil-and-paper one. It also compares this work with earlier formal ML efforts, including Certigrad's proof of unbiased stochastic backpropagation gradients in Lean, Coq-verified Hoeffding bounds for finite hypothesis classes, and VC-dimension theory, which the paper deliberately leaves out. The episode also sets up the claim that a step in the standard textbook proofs doesn't hold as stated. That claim should interest anyone curious about what machine-checked proofs reveal about familiar learning-theory results.

This episode explores a 2024 paper that tries to turn mechanistic interpretability into formal guarantees. The idea is to reverse-engineer a small transformer into an algorithm, then use that algorithm to write a much shorter proof of a lower bound on the model's accuracy. The test case is a one-layer, attention-only model trained to output the maximum of four integers. The discussion contrasts this approach with local-robustness verifiers and PAC-Bayes bounds. It also sets out the two trivial extremes: brute-force enumeration of about sixteen million inputs, and a vacuous accuracy bound of zero. The interpretation finds that the model attends to larger tokens, copies what it attends to, and barely depends on position. Treating everything the interpretation leaves unexplained as worst-case yields a "cubic" proof that cuts the compute roughly four-million-fold, at the cost of certifying about 95% accuracy instead of the true 99.9%. Listeners get a clear look at how a better mechanistic understanding could make guarantees cheaper, along with the caveat that the evidence comes from a single tiny model.

This episode explores the Saxe, McClelland, and Ganguli paper on exact learning dynamics in deep linear neural networks. It explains why these networks are worth studying even though they collapse to a single linear map: their gradient-descent dynamics are still coupled and non-convex, and they show the long plateaus followed by sudden error drops seen in real deep nets. The discussion covers the Baldi and Hornik result that every critical point is a saddle except the best low-rank solution. It then covers the "decoupled invariant manifold," where each input-output mode evolves independently. The mode-strength equation, whose growth rate is proportional to its own value, explains why small initial weights produce long plateaus. The episode argues that depth need not slow learning if the initial conditions are chosen well, and ties this to unsupervised pretraining and to random initialization. Listeners get a clear, step-by-step derivation of why training time depends on the starting point.

This episode examines "Verifying Peephole Rewriting In SSA Compiler IRs," which uses the Lean proof assistant to give MLIR-style compilers a push-button workflow for proving small rewrites correct, without the cost of a fully verified compiler. It explains peephole rewrites and why SSA def-use chains let a matcher catch patterns that straight-line matching misses. It then compares the approach with Alive and Alive2, which rely on SMT solvers, and with CompCert-style end-to-end verification, which takes years of expert effort and is tied to one IR. The discussion covers MLIR dialects and regions, and why a ring-aware prover helps for domains like fully homomorphic encryption, where an algebraically trivial rewrite becomes a heroic proof at the LLVM level. It also covers refinement semantics with poison and undefined behavior. The episode adds a caveat from Csmith's results: proving local rewrites correct does not cover bugs in parsing, lowering, or pass ordering. Listeners get a clear picture of where formal compiler verification can reach into new domain-specific IRs and where it stops.