Weekly Gallery
Latest edition
Sep 5 – 12, 2026
Directions: 7 · Updated this issue: 6 · Picks: 43
AI for Formal Math · Issue 5
After Fermat's Last Theorem: Readability, Soundness, and Verification Blind Spots
The aftermath of the formalization of Fermat's Last Theorem (FLT) became the main thread in the community this issue. Kevin Buzzard's first-hand account indepen…
Magenta: Closing the Loop Between Mathematical Reasoning and Lean VerificationMagenta explicitly models verification failure as an attribution problem: an error judge distinguishes mathematical errors from syntax errors, routing failures to re-derivation or local proof repair rather than simple retries; a statement judge explicitly prevents "fake certificates"—formalized statements that are unfaithful to the original problem yet pass Lean verification. Compared to Reward-Oracle MCTS from Issue 4 (treating the compiler as a pure scalar reward) and Process-Verified RL (training-based), Magenta is a training-free inference-time closed loop, and ablations show that the statement judge provides substantial gains in error certificate rate and feedback-guided correction on hard problems. Code and data are public, making it a significant increment in agentic proof search.- Beyond Solver Verdicts: Generative Reward Models for AutoformalizationThis work formalizes the "verification-preserving unfaithfulness" (VPU) failure mode—incorrect encodings can successfully execute and match solver decisions yet not be equivalent to the reference—and proves that purely decision-based heuristics are mathematically limited to random levels. Its increment lies in distilling an offline Z3 equivalence oracle into a reference-free, continuous generative verifier (GenV) that can detect unfaithful formalizations even when references are absent, and mechanism analysis shows that error localization emerges without explicit training. Compared to ShadowBench (bidirectional implication of shadow theorems) and Beyond Compilation from Issue 4, GenV directly attacks the solver's "decision blind spots," providing direct value for building trustworthy automated formalization pipelines.
- AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum MechanicsAxQM is the largest physics formalization proof synthesis benchmark to date: 1019 tasks, 479 entries, all from the Nielsen-Chuang textbook, 4.1 times the size of the previous largest physics benchmark. Its core increment lies in being a census of a single book rather than sparse sampling across sources, with tasks embedded in a custom finite-dimensional quantum mechanics Lean library, and all tasks guaranteed solvable (solution library kept secret to prevent leakage); it also explicitly audits and fixes semantic flaws in predecessors like Lean-QIT-Bench, such as quantifier order errors and unconstructed circuits. In the Mathlib fork, the generalization of MultilinearMap to multilinear maps has been submitted as an upstream PR, contributing practically to the Lean ecosystem.
Pretraining Data · Issue 5
Base Loss Optimal ≠ Post-Training Optimal: An Empirical Moment of Criterion Reversal
This issue brings the most direct empirical endorsement of the "post-training upper bound" criterion. One work, on a full 30B MoE training pipeline, found that …
Good Pretraining, Bad SFT: Checkpoint Quality Across the Training StackProvides direct evidence on a full 30B MoE pipeline that "base-loss-optimal checkpoints perform worse after downstream SFT," and identifies solution density as the true determinant of post-training performance. Relative to the toy board-game pretraining→RL scaling law in *Understanding Reasoning from Pretraining to Post-Training* (Issue 3), the increment is advancing "evaluating data recipes by post-training upper bound" to real-scale controlled validation, directly challenging default assumptions in base-loss-centric scaling laws and mixing studies.- Knowledge Distillation During Mid-Training Favors Reasoning over Factual RecallFirst systematic characterization of knowledge distillation's starkly different behavior in mid-training versus pretraining: forward-KL distillation sacrifices factual recall for reasoning gains during mid-training, and proposes Switch Distillation with teacher entropy as a routing signal to mitigate this trade-off at the token level. Relative to *Beyond Solvability* (Issue 4) and MIRA (Issue 3), which treat data selection as the lever, the increment is treating the distillation objective itself as a mid-training supervision source, with evidence covering a 1B student, 7B/13B teachers, 60B tokens, and full post-training (SFT+DPO+RLVR).
- Data Scarcity and Model Sparsity: Mixtures-of-Experts Overfit More to Repeated DataFirst explicit coupling of MoE sparsity with repetition harm, finding that MoEs overfit repeated data more severely than compute-matched dense models, that optimal repetition decreases with expert count, and that harm is driven by total parameters. Relative to the dense-model repetition scaling law in *Internal Data Repetition* (Issue 1), the increment is introducing sparsity as a moderating variable with mechanism analysis (early routing fixation, expert over-specialization), providing a new criterion for data-scarcity allocation decisions under MoE architectures.
MoE & Sparse Experts · Issue 5
Boundaries of Load-Balancing Enforcement: Soft Anchoring and Renormalization
The main theme of this issue is the boundaries of load-balancing enforcement: multiple independent works examine the cost of the default configuration of pushin…
Training-Free Halving of Activated Experts in Fine-Grained Mixture-of-Experts ModelsMust-read. For the first time, decouples the denominator (reference set) of MoE renormalization from the number of activated experts, proposing a k1/k2 dual-parameter scheme, proving that performance loss when reducing k mainly comes from gain mismatch rather than expert capacity loss, and finding that perplexity and downstream tasks have inconsistent optimal choices for k2. Compared to the routing-invisible subspace intervention in RARE from Issue 4, this paper directly operates on the renormalization denominator at inference time without training or parameter modification, offering a new alternative path for training-inference routing consistency, and reports routing statistics and dense baselines on Qwen3.6-35B and the 11× larger Qwen3.5-397B.- Router Prior Bias: Preserving Base Routing Structure in MoE Post-TrainingMust-read. Directly challenges the default practice of re-imposing auxiliary load-balancing loss during post-training: proposes soft router anchoring, pulling router logits toward the frozen base router's prior while keeping the router trainable, significantly outperforming re-imposed LBL on Moonlight-16B-A3B math post-training (45.77 vs. 31.91). Compared to routing replay in PR² and ReLibra from Issue 2, this paper systematically separates constraint strength from prior content using intervention controls (soft vs. hard, intra-community vs. inter-community shuffling), proving that community structure is a footprint of soft enforcement rather than a source of benefit, and provides a three-level preservation protocol with applicability conditions.
- When Load-Balancing Goes Too Far: Expert Pruning in Over-Dispersed Mixture-of-Experts ModelsWorth reading. For the first time, systematically characterizes over-dispersed routing (induced by λ_aux=0.9) as a unique mechanism for expert pruning: under this mechanism, perplexity and task accuracy decouple, global importance signals fail, and pruning metrics exhibit capability trade-offs between reasoning and knowledge tasks. Compared to Launch-Bound from Issue 3 and From Observation to Intervention from Issue 1, this paper uses routing entropy as a diagnostic tool and proposes a domain-aware minimax pruning method MESA for this mechanism, validating domain unfairness on gpt-oss-20B—a direct negative result of excessive load-balancing enforcement.
Efficient Sequence Modeling · Issue 5
Channel Specialization in Hybrid Architectures: Attention Retrieves, Recurrence Shapes Language
The strongest signal this issue comes from direct causal evidence on channel specialization in hybrid architectures. What Attention Recalls and Recurrence Contr…
What Attention Recalls and Recurrence Controls in Hybrid Language ModelsFirst to use split-prefill and state-swap, two cache-level interventions, to causally separate the functions of attention and recurrent channels in trained hybrid LLMs (Qwen3.5, Falcon-H1): precise retrieval survives only through the KV cache (64-98%), while output language/persona survives only through the recurrent state (70-80%). State-swap proves that answer values come from the KV side, while language comes from the recurrent side. Relative to Issue 4's 'Modern Transformers Are Implicit Hybrids' frequency-axis intervention, it advances the functional dichotomy to channel-level causal exchange and reveals that recurrent states produce associative and conjunctive false memories. Anyone doing prior research on hybrid architecture layer ratios or efficient attention optimization should read it.- Hierarchical Sparse Attention Done Right: Toward Infinite Context ModelingAdvances the chunk summary for block-sparse selection from mean-pooling to a learnable form aligned with the first-order Taylor expansion of LogSumExp chunk mass, and uses hierarchical softmax to make selection scores directly supervised by the LM loss, addressing the insufficient alignment between the indexer and the main attention distribution. Relative to Issue 1's MiniMax Sparse Attention per-group block-level top-k and Issue 2's COBS second-order cumulant selector, its increment is providing a mathematically aligned form for chunk summaries and making selection differentiably affect outputs. Provides compute-matched comparisons at 345M/1.4B/7B, degradation curves for 8K training with 4M extrapolation, and necessary ablations for HoPE/landmark.
- Kalman Delta Networks: Uncertainty-aware Associative MemoryReframes delta-rule linear attention as a linear-Gaussian state-space model, using covariance propagation to explicitly track memory uncertainty, so that write gains are derived from cumulative evidence and observation noise rather than current-token prediction. Diagonal/Isotropic scan-compatible approximations reduce the uncertainty recursion to Möbius maps. Relative to DeltaNet/Gated DeltaNet/KDA and Preconditioned DeltaNet, it is the first to add the missing confidence state variable to delta rules. Provides compute-matched comparisons at 750M/1.3B against KDA, Mamba-3, and GDN-2, plus RULER degradation curves—a new principle axis for hybrid linear attention design.
Coding Agents · Issue 5
Benchmark Hardening Lands: Leak Audits Evolve from Methodology to Executable Artifacts
The strongest signal this issue is benchmark validity advancing from "audit methodology" to "executable artifacts." SWE-Bench Pro Verified turns the findings of…
SWE-Bench Pro Verified: A Reliable Benchmark for Software Engineering AgentsThe first hardened benchmark that simultaneously applies anti-leakage and task correction to executable artifacts: repository reconstruction, test artifact hiding, metadata anonymization, and network blocking to close four leakage channels, plus correction of 102 broken instances. Paired evaluation shows GLM-5.2 dropping from 78.80% to 57.32% (-21.48pp), with 186 baseline passes flipping to failures versus only 15 in reverse, and 90.9% of flips attributed to removing hacks rather than breaking execution. Compared to Issue 3's ABA audit detection and Issue 1's HackDetect post-hoc attribution, it provides a directly runnable hardened benchmark and complete leakage channel audit—the most direct quantitative evidence that "pass rates on saturated benchmarks are inflated by leakage."- Vero: Can AI Agents Build Formally Verified Software Repositories?The first repository-level joint code-and-proof Lean 4 benchmark, with 43 multi-module instances, 743 APIs, and 2,705 specifications; the strongest configuration solves only 27/43, with failures concentrated on cross-module inductive invariants and lemma library organization. Its audit mechanism accepts machine-checkable negative evidence of "unsatisfiable specifications/incorrect reference implementations," converting latent benchmark defects into fixable findings; contamination disclosure (manual translation from source language, no public Lean 4 ground truth) meets hard standards. Compared to Issue 4's DeepSWE on conventional software engineering tasks, it elevates "correctness" to machine verification, marking a new milestone in long-horizon repository-level evaluation.
- HarnessDev: Can LLMs Create and Evolve Their Own Agent Harness?The first benchmark moving the evaluation unit from task outputs to runnable infrastructure, separating creator/executor, covering both Creation from weak seeds and Evolution based on downstream feedback, and measuring execution token costs and cross-executor transfer. Core finding is that evolution gains are unstable and transfer poorly (Opus's Self-Eval SWE-Pro score drops from 69.3 to 33.0 after switching executors), directly strengthening skeptical evidence that "harness update ≠ harness benefit." Compared to Issue 2's HarnessOpt-Bench which only optimizes a given harness, it adds the Creation stage and executor dependency dimensions; limitation is that evolution held-out uses only the SWE-Pro single benchmark.
Recursive Self-Improvement · Issue 5
Self-Assessment Signals Are Unreliable: Closed Loops Need External Grounding
The main theme of this issue is that self-assessment signals are unreliable. Multiple independent works converge on the same conclusion from different angles: t…
Can AI agents conduct open-ended AI research? Early evidence from two case studiesShould read. It directly addresses the measurement methodology of "self-improvement rate": using core research questions from unpublished papers as tasks, with original paper authors as reviewers, avoiding training data contamination while providing deep expert judgment—a third measurement path beyond blind review randomness and the narrowness of verifiable tasks. Both cases were explicitly rejected by the original authors, and five failure modes (poor judgment of publication thresholds, lack of creativity on design flaws, ineffective backtracking, poor resource awareness, instruction drift) and resource usage trajectories are systematically reported. Read it to understand the real boundary of current AI research automation: "engineering ability has been met, but research judgment has not."- S3Gym: Can LLMs Turn Self-Testing and Self-Judging into Self-Improvement?Should read. It advances self-improvement evaluation from comparing single mechanisms to explicitly measuring the coupling of three abilities—self-testing, self-evaluation, and self-improvement—comparing three paths (History ICL, Summary Memory, and parameter training) under a unified protocol, and using executable environment verifiers to separate self-evaluation from true rewards. The core negative result is that judgment-improvement coupling is near zero (ρ≈-0.010)—accurate self-assessment does not translate into improvement—and parameter training causes severe negative transfer on PvZ. Compared to PAST-Bench's cross-session experience retention in Issue 3, the increment is making "self-assessment reliability" itself an independent measurement object, with step-level reliability analysis on 116,117 transitions.
- Self-Authored Verification Is Unreliable in Heuristic Self-Improving AgentsShould read. It formalizes the "verifier-deployment gap"—where an agent controls both its policy and its tests, self-scores can remain near-perfect while deployment performance degrades—and provides an information-theoretic bound: endogenous gates alone cannot close this gap. SEAL uses a single-bit feedback external acceptance loop as the minimal intervention, validated across six models and three seeds, with ablations showing that "conservative rollback" and "external audit" each contribute differently. Compared to the longitudinal measurement of self-assessment bias in "When Do Agent Loops Mistake Stagnation" from Issue 3, the increment is making "external grounding" a falsifiable acceptance boundary, and providing a contrast for leakage audits—public number audits can become optimizable targets again.