Weekly Gallery
Latest edition
Oct 24 – 31, 2026
Directions: 9 · Updated this issue: 4 · Picks: 30
AI for Formal Math · Issue 12
A Cold Shower for Complex Harnesses: Minimal Loops Are Winning in Theorem Proving
In the previous issue, we summarized the architectural shift in agentic proof search as "the model only plans, while execution is left to tools and the kernel."…
h1: A Taste of the Bitter Lesson in Automated Theorem ProvingDirectly challenges the belief from Issue 11 that complex harnesses (Maestro's global coordination, SCOPE's policy planning) are indispensable: under matched model and inference cost, a minimal test-time scaling loop matches or Pareto-dominates these complex specialized workflows, providing reproducible cost-success curves and ablations. Its increment lies in the first systematic comparison of different simple harness efficiencies (tool interfaces, context reuse) and demonstrating that persistent single attempts (pass@1) outperform repeated attempts (pass@k) on open problems. A sobering contrast for researchers who treat harness complexity as the default path.- Agentic Algorithm Design: LLMs that Propose, Formalise, and Prove Runtime Bounds for Evolutionary Algorithms in LeanThe first automated pipeline that lets LLMs design black-box optimization algorithms and machine-verify their expected runtime bounds in Lean, without empirical evaluation throughout. Compared to Maestro/SCOPE from Issue 11 (proof search and textual planning), its increment lies in formalizing randomized runtime analysis (drift certificate) for LLM-proposed algorithms, and achieving exponential improvement over (1+1) EA on CycleUncover; the staged pipeline using Lean guards to filter defective designs is directly transferable to trustworthy agentic proof systems. Limitations (only frontier models, simplified drift theorems) are clearly stated in the paper.
- Scaling Lean Theorem Proving for Real-World Code VerificationTransforms competitive programming problems into Lean verification tasks with implementation-level obligations, producing 11,553 candidate specifications and 2,045 differentially verified Rust–Lean programs, far from saturation (52.7% solve rate vs. near-saturated 99.6% on PutnamBench). Compared to ITPEval (cross-ITP translation) and reuF2F (open conjectures) from Issue 11, its increment lies in automatically generating tasks with implementation-level obligations such as fixed-width arbitrary arithmetic, explicit failures, generative loops, casts, and functionalized mutations, and providing negative labels through counterexamples—something pure proof loops cannot do. The engineering insights of EasyProver (recursive agent, isolated context, InfiniLean stateless elastic elaborator) are also valuable; note its lack of component ablations and use of untrained off-the-shelf frontier models; the benchmark itself is a more lasting contribution.
MoE & Sparse Experts · Issue 12
The Value of Dynamic Expert Pruning Is Budget-Dependent
This issue's main thread continues the discussion on 'controlled baselines' from the previous issue and advances the conclusion one step further: the value of d…
You Only Need 2/3 of the Chosen Experts: An Empirical Study of Dynamic Expert Pruning in Fine-Grained MoE LLMsMust-read. Extends the measured compute matching burden of proof from Issue 11's 'Don't Skip the Baseline' to fine-grained MoE: with uniform truncation of ⌈2K/3⌉ as baseline, it retains an average of 98.8% performance, and dynamic rules under conservative budgets differ from uniform truncation by only +0.06 points; advantages appear only under aggressive pruning (≤1/2 of native K), with gains up to +3.0 points and rotating winners. Compared to Issue 11, this paper adds task family (generation vs. likelihood) and model attribute (thinking/scale/multimodal) decompositions of pruning sensitivity, advancing the value of dynamic allocation from binary to budget-dependent judgment, reporting complete routing statistics and dense comparisons across nine architectures and twelve checkpoints.- Overcoming Data Imbalances with Expert Selection BiasesMust-read. First to reuse the per-expert bias mechanism without auxiliary loss from load signal to class-conditional capacity allocation: preferred expert share (r_c=q_c/p_c) explicitly exposes the class-specific expert pool size independent of data share as a knob, with soft bias during training and removable at inference. Compared to Issue 10's ProbMoE and Issue 9's Structuring MoE, this paper switches bias from load to class signal, reports complete routing statistics on a 10.6B-scale multilingual/multimodal/domain mixture, and provides qualified causal evidence for expert specialization via functional modular intervention (disabling Swahili-specified experts causes +107% loss vs. +9.3% baseline).
- Rimuru: Unified Memory Management for Modern LLM Serving via Elastic Expert OffloadingMust-read. First to unify expert caches with KV/SSM states in a shared page pool: multi-view memory layouts let each tensor type use its own page size and page table to interpret shared space, a multi-level allocator enables cross-type elastic capacity reuse, and page-table-aware fused MoE kernels directly consume non-contiguous expert weights to avoid copying. Compared to Issue 6's VAMP dynamic HBM repartitioning, this paper's increment lies in explicit multi-view abstraction and execution-time zero-copy, reporting complete routing statistics and dense comparisons on Qwen3.5-35B/122B, a new system-level path for elastic expert caching in serving.
Efficient Sequence Modeling · Issue 12
Competitive Learning: Division of Labor in Hybrid Architectures Emerges During Training
The biggest signal this issue pushes a long-standing question in this direction—how efficient attention as an optimization prior affects the formation of retrie…
Competing Learning in Hybrid ArchitecturesFirst to study the 'division of labor' formation for retrieval in hybrid architectures as training dynamics itself: due to short-range inductive bias, the recurrent layer (KDA) learns retrieval first, suppressing the attention layer from developing this ability, resulting in suboptimal division of labor; accordingly proposes the BLD training procedure, freezing the recurrent layer early to cede the first-mover advantage to the attention layer, validated across KDA/GDN/GLA with compute-matched comparisons and degradation curves. Relative to Issue 5's 'What Attention Recalls' channel-level causal separation, its increment is providing gradient evidence for the competitive learning mechanism and an actionable training intervention—this is a direct negative result of efficient attention as an optimization prior affecting retrieval heads, and anyone doing layer-wise ratios in hybrid architectures should read it.- DCKV: Learned Transform Coding of the Prompt KV Cache in Hybrid Language ModelsFirst to make the prompt KV cache an end-to-end trainable codec: the transform, quantizer, and entropy model are jointly rate-distortion optimized against the frozen language model's output, with a conditional entropy model exploiting prompt tokens and decoded neighbors (checkerboard two-pass), skipping prior heuristic/fixed probability models. On Qwen3.5-2B, it loses AT at about 55–100× byte compression, using 72% fewer bytes than KVTC at the same score; relative to Issue 10's AbridgeKV for model-generated content compression, its increment is providing a trainable rate-distortion trade-off framework aligned with the output distribution, and anyone doing KV compression in hybrid architectures should read it. Limitation: validated only on the Qwen3.5 family.
- ParaTTT: Parallelizing Test-Time Training Layers with Deep MemoriesFirst to advance the parallelization of TTT-like nonlinear memory from block approximation to iterative refinement fixed-point solving of the inner-loop gradient trajectory: the exact online recurrence is the fixed point of the iteration, a two-layer variant provides a geometric convergence proof, and decoding requires no iteration. At matched error, it is 32× faster than TTT-MLP, 4.9× faster training for a 340M model, and superior in recall to GDN/Mamba-2; relative to Issue 10's Latent Compaction with Test-Time Training's per-document gradient descent, its increment is making the evaluation of nonlinear memory itself a provably convergent parallel bad path, and anyone doing hybrid linear attention or TTT layers should read it.
Scaling Laws & Training Methods · Issue 12
Same Scaling Law Fits, Radically Different Extrapolations
This issue brings two threads together into one question: to what extent can we hold accountable the "laws" we believe we have established. The first thread tar…
Ambiguous Fits: The Rashomon Effect and Challenges in Scaling Law EstimationFor the first time treats the scaling law fitting stage itself as the object of study: using a deterministic branch-and-bound algorithm to provide provable lower bounds on global near-optimality, and systematically mapping the Rashomon effect of the near-optimal fitting family—parameter regions where fitting loss is nearly identical but extrapolation predictions differ dramatically (on real multi-scale data, cross-extrapolation efficiency gaps can reach 74.6× or even 146×)—providing strict upper and lower bounds on the prediction envelope. Compared to Issue 8's ScAn-Bench fitting methodology evaluation and Issue 10's SLDBench v2 active experimental design, this is the first work providing verifiable fitting loss lower-bound certificates and quantifying extrapolation uncertainty, a first step from "reporting a single optimal curve" to "reporting a family with guaranteed envelopes." Limitation: strict envelopes for the five-parameter law are computationally expensive; only the three-parameter law is practical.- The Role of Quantization in Loss SpikesFor the first time advances the cause of loss spikes to the hidden mechanism of "Adam-induced logit mean drift amplifying finite-precision quantization errors in the LM head": mean drift is harmless under exact arithmetic but amplifies quantization errors; lower precision accelerates time-bomb spikes while higher precision stabilizes training, and unifies z-loss, μ-centering, and LM head SGD-M as suppressing quantization errors. Compared to Issue 3's Grokking or Glitching attributing spikes to the Slingshot mechanism of cross-entropy numerical artifacts, this paper focuses on the interaction between Adam preconditioning and quantization errors, reporting stability and quantization error curves across 28M–1.4B scales. Limitation: scale stops at 1.4B, spikes are artificially induced by high learning rates; extrapolation to natural large-scale spikes requires self-assessment.
- Does LLM Pre-Training Typically Occur at the Edge of Stability?For the first time systematically characterizes two failure modes of the quadratic approximation at LLM pretraining scales up to 787M: divergence due to negative curvature, independent of learning rate (Edge of Convexity), and generalized Edge of Stability under stochastic adaptive optimizers, providing a scalable detection algorithm with theoretical guarantees that reduces to Cohen's full-batch EoS while additionally identifying EoC. Compared to Issue 9's Muon Sublates the Edge of Stability focusing on Muon's stability phase diagram, this paper targets AdamW and quadratic approximation failure modes, and reveals that EoS depends on critical thresholds of batch size and learning rate schedules, providing direct guidance for scheduling and batch selection. Limitation: scale stops at 787M; scalability to larger scales requires self-assessment.