Compact Proofs of Model Performance via Mechanistic Interpretability

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 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 PASTA, a method that lets users highlight part of a prompt and has the model attend to it more strongly, without changing any weights. It covers why markup like asterisks may not work as emphasis for LLMs. It then places PASTA against instruction tuning, activation steering (ActAdd, CAA, Inference-Time Intervention) and knowledge editing (ROME, MEMIT, REMEDI). The key difference is that PASTA changes where selected attention heads read, rather than what they output. The discussion explains the mechanism: scores outside the highlighted span are scaled by a small alpha (0.01) and renormalized, which is equivalent to a roughly hundredfold relative boost on the span. The hosts also raise questions about head selection and evaluation, including the absence of comparisons against the neighboring steering methods. Listeners interested in controllability, long-context failures and conflicts between a prompt and a model's memorized knowledge will find it useful.

This episode examines MEMORILLA, a Stanford-led preprint in which a small trained module reads a whole store of pre-embedded documents and hands a frozen language model just 16 soft-token vectors, instead of pasting retrieved text into the prompt. It motivates the design with a personalization scenario. An old, unrelated chat reveals a preference for blunt feedback, so similarity search may miss it, and the signal is spread across many chats that top-k retrieval can't integrate. The discussion contrasts this approach with full-context prompting, agent memory systems (MemGPT, Mem0, MemoRAG, A-MEM), question-blind compression methods (ICAE, xRAG), and per-corpus cache training (Cartridges). It also traces the design's lineage to Perceiver, BLIP-2's Q-Former and prompt tuning. Listeners get a skeptical framing of the headline claim, including whether gains come from reading the store or from training on the benchmarks, and whether comparing against baselines that weren't trained on them is fair. The evaluation covers personalization, long-document QA, knowledge-intensive QA and a TextWorld agent.