Weekly Gallery
Latest edition
Oct 17 – 24, 2026
Directions: 9 · Updated this issue: 8 · Picks: 59
AI for Formal Math · Issue 11
Architectural Shift in Proof Search: From Local Repair to Global Coordination
The main theme of this issue is the architectural shift in agentic proof search: from "models writing proofs token by token" to "models only planning/coordinati…
Maestro: Agentic Formal Proof Development by CoordinationAdvances proof failure handling from "local repair" to "global coordination": workers return structured diagnostics (routes attempted, auxiliary facts needed, suspected counterexamples), and the coordinator, seeing the entire proof forest, chooses to retry, add lemmas, retract subtrees for replanning, or refute goals, and can arbitrarily edit the shared workspace (including discarding proven lemmas). Compared to Issue 10's Lean Graph Search (retrieval-augmented) and Issue 9's LEVER (goal-directed search on AND/OR graphs), the increment lies in explicitly modeling failure causes and allowing global-level replanning; the same framework extends to verified code synthesis (counterexamples sent back to the implementer for repair). Achieves 34/48 on arXivLean, surpassing the native agent's 19/48, with run logs and prompts publicly available. Note the baseline is a plain coding agent rather than the strongest specialized prover, and it relies on frontier closed-source models, but the ablation (naive decomposition) cleanly isolates the contribution of coordination.- SCOPE: Certified Theorem Proving with a Language Model as the Policy PlannerProposes a three-part architecture where "the model never touches proof text/numbers, only selects operators": the model does policy planning within a vocabulary of 194 operators, a symbolic execution engine handles arithmetic, and a compiler renders Lean text. Compared to Issue 7's LEAP (goal-directed search on AND/OR graphs, still with the model outputting concrete steps) and Issue 9's LeanPlan (agent generates code+proof, kernel verifies), the increment lies in making "the model does not write proof text" an architectural principle, and a 2×2 factorial experiment proves that "state visibility at decision time" is a first-order determinant of accuracy (53.7%→87.6% after correction), while also providing the error product law (Pass ≤ p^k) to theorize the structural causes of numerical generation failures. A 135M backbone achieves an 87.6% kernel verification pass rate, with a version-frozen verification pipeline plus independent rechecking and reverse verification, and artifacts are public. The problem domain is limited to constructive discrete mathematics, but the architectural paradigm is worth careful digestion.
- reuF2F: Benchmarking coding agents on formalized undergraduate research problemsThe first benchmark to systematically collect open conjectures from REU undergraduate research projects and formalize them in Lean 4 (244 problems), using a bidirectional prove/disprove protocol and dual kernel verification with Comparator+nanoda, and introducing a unified coding-agent evaluation framework, Leanimum-agent. Compared to Issue 10's Annals dataset (known theorem statements) and Formal Conjectures (community-interest problems), the increment lies in focusing on low-attention open problems to reduce leakage risk, and aligning open-problem evaluation with coding-agent workflows for the first time. Even the strongest models solve only about 40%, leaving clear room for end-to-end open-problem solving. Some results rely on frontier models, but the benchmark's reproducibility design makes it an important artifact for future evaluation.
Pretraining Data · Issue 11
Agentic mid-training recipe first disclosed: post-SFT performance as criterion
This issue's clearest signal is the progression of mid-training from 'corpus construction' to 'complete recipe + post-training ceiling criterion'. Priming Base …
Priming Base Models for Agentic Post-Training: An Open Midtraining RecipeFirst disclosure of a complete open recipe for agentic mid-training, advancing mid-training from 'corpus construction' to 'complete recipe + post-training ceiling criterion'. Achieves significant improvements on SWE-bench/DeepSWE after identical SFT on Nemotron 3.5 Lightning (500B tokens) and Super (280B tokens), explicitly distinguishing the ratio of natural software engineering data to agentic traces (traces only 10-15%, tool-response masking), and systematically ablating replay ratio and learning rate. Relative to issue 6's MiST synthetic mid-training corpus design, its increment is a reproducible complete recipe, and the authors explicitly report that base-model proxy metrics do not correlate with post-training results, instead using short fixed SFT as criterion, directly responding to this direction's shift toward 'post-training ceiling'. Limitation: data and code are not disclosed, RL evidence is thin, but as an open recipe its methodological contribution is worth reading.- Selecting Repetition Counts Across Model Scales in Data-Constrained PretrainingFirst to systematically show that under fixed target corpus mixed with generic data, the optimal repetition count r undergoes ranking inversion with model scale (at 50M, r=16 outperforms r=8; at 80M and 520M, order reverses), and proposes candidate-set pruning based on small-model loss curves as an alternative to exact point prediction. Relative to issue 9's 'What Is a Repeated Token Worth?' single-round geometric framework, its increment is advancing 'repetition value varies with scale' into explicit scale-dependent ranking inversion and an operational pruning procedure; relative to issue 3's 'Scaling Laws for Mixture Pretraining Under Data Constraints' r-h coupling law, its increment is validating the inversion on independent, complete configurations and providing candidate retention. For mixture decision-makers relying on small-model scans to determine repetition rates, this is key evidence that changes decisions.
- Scaling Multilingual Mixture-of-Experts: How Language Coverage Changes Capacity and Compute AllocationFirst to jointly model MoE laws with multilingual coverage laws, explicitly characterizing the interaction between expert count E and language coverage K, proving that 32 experts reduce the loss penalty from 12→200 languages by 83%, and revealing that broader coverage extends the computational advantage regime of expert-heavy configurations. Relative to issue 10's 'Scaling Laws for Multimodal Data Mixtures' unified three-modality mixture scaling law, its increment is making language coverage K an interaction design axis with expert count E, providing a repetition-aware joint law. Grid of 26,300 loss observations and 14 multilingual benchmarks align with preferences; limitation: max 1.15B, criterion still base loss.
MoE & Sparse Experts · Issue 11
Controlled Baselines Counter Dynamic Routing Methods
The main theme of this issue is "controlled baselines are countering dynamic routing methods." Two independent works have falsified the effectiveness of dynamic…
Don't Skip the Baseline: A Controlled Comparison of Dynamic Expert Skipping in MoEsMust-read. First controlled comparison of dynamic expert skipping methods: under budgets matched to measured compute (K_eff), compares four representative methods (NAEE, DiEP, MoDES, Ada-K) against a simple static top-k baseline, finding dynamic methods fail to consistently beat the static baseline, with calibrated K_eff deviating from measured K_eff by up to 6x. Compared to Issue 5's Training-Free Halving and Issue 6's ACE, this paper establishes "matching measured compute" as the burden of proof dynamic skipping methods must beat, reporting complete quality-compute frontiers across modalities on Gemma4-26B-A4B, Qwen3-30B-A3B, and Qwen3-VL.- TRACE: Rollout-Guided Quantization-Aware Training for FP4 Reinforcement Learning of MoE Language ModelsWorth reading. First to advance train-inference routing consistency from routing decisions to the quantization execution path: uses rollout-side FP4 quantization results to guide training-side rounding direction (selecting nearest adjacent codeword to rollout codeword rather than RTN), and caches only deep mantissa information to control communication overhead. Compared to Issue 10's Router Drift Control's response-level filtering and Issue 8's T1 routing replay, this is a new path for train-rollout alignment in the quantization domain, reporting full training dynamics with dense comparisons at 2.4T-scale MoE.
- 3D-MoE: Complementarity-Guided Hardware-Software Co-Design for MoE Decode on 3D-Stacked NMPWorth reading. First to use expert complementarity (offsetting fluctuations in decoding-step load trajectories) as an explicit signal for MoE decoding load balancing on 3D-stacked NMP: offline complementary grouping and locality mapping establish coarse-grained inter-group balance, with CMN hardware fast path handling intra-group residual hotspots. Compared to Issue 10's Afore's micro-batch-level demand prefetching and Issue 9's Zepp's communication shaping, this is the first to use complementarity as a grouping signal with hardware-software co-design, reporting full routing statistics with dense comparisons.
Efficient Sequence Modeling · Issue 11
The Unread Tail of Sparse Attention: Proxies, Certificates, and Phase Blind Spots
The strongest signals this issue revolve around a long-overlooked problem: how to handle the unread tail of sparse attention. Two works provide key increments f…
OpenAttention: One Percent Is Enough with Tail ProxiesFirst to systematically prove that at low read rates, folding the unread tail with a single count-aware mean proxy is better than random tail sampling, and provides a closed-form weight error bound: at low read rates, sampling nearly doubles the discarded weight error while the single proxy remains below it. Relative to CompKV's mean tail compensation in Issue 7 and FreeSolo's mean key routing in Issue 10, the increment is explicitly proving the proxy is better than sampling, and allocating budget by estimated weight error (ErrorGate) rather than centroid mass; on RULER-32K HARD, 1% read retains 99% dense accuracy, with compute-matched degradation curves across models/context lengths.- Periodic Weak Spots: Phase Sensitivity from Chunked KV-Cache CompressionFirst to systematically reveal that fixed-stride blockwise KV compressors cause periodic positional phase blind spots: the DeepSeek-V4 family shows retrieval accuracy fluctuations of up to 40pp with target phase at 128K context, and average needle-in-a-haystack scores are structurally insensitive to this. Relative to Issue 8's 'Counterexamples to Local Reconstruction Gain' which localizes failure to local reconstruction objectives, the increment is localizing to the specific mechanism of fixed-stride blockwise compression, and using from-scratch pretraining + causal interventions to prove phase specialization originates from training dynamics—any work claiming 'lossless' based on average NIAH should cite this as a warning at the evaluation protocol level.
- Certified Sparse Attention via Perturbed RetrievalFirst to advance sparse attention's error control from heuristics to per-query guarantees with finite-sample certificates: using Exp(1) perturbation to turn threshold retrieval into probability-proportional-to-size (PPS) sampling, paired with Horvitz–Thompson estimation and anytime-valid confidence bounds, effective at data-dependent stopping levels. Relative to Issue 4's 'Faster Than Flash' training-agnostic top-δ selection, the increment is providing provable per-head per-token error bounds with sample complexity independent of context length; on real KV caches, it eliminates tail errors, with 90th percentile error 4.6–7.9× lower than the lowest among 15 baseline families, and certificate failure probability ≤δ during generation.
Scaling Laws & Training Methods · Issue 11
New Axis for Optimizer Benchmarking and Theorization of Muon
This issue advances both main lines of the optimizer system by one step: one is to continue expanding the methodological axis of optimizer benchmarking, and the…
A Statistical Viewpoint on Adam, Shampoo and MuonFor the first time unifies Adam/Shampoo/Muon into the statistical framework of "whitened momentum methods," and provides a Bayesian interpretation that the Muon update direction is the MAP of a Matrix Langevin distribution. Based on this, it proposes MND and MND-Muon: jointly estimating the mean and Kronecker factors, extending polar decomposition to momentum in anisotropic whitening coordinates. On 124M/353M, MND relative to Shampoo and MND-Muon relative to Muon achieve final loss and stability gains, and report full learning rate grids and spike information. The unified perspective has the potential to replace the current state of analyzing each optimizer separately, and is an important reference for optimizer benchmarking and stability in this direction. The limitation is that it has not been compared with spectral-type optimizers.- ECHO: Efficient Causal Self-Recursion Beyond Auxiliary Multi-Token PredictionRefactors multi-token prediction from an auxiliary module into causal self-recurrence: reusing the backbone's last layer and output head to recursively predict future horizons, so that multi-horizon supervision directly acts on the backbone rather than being absorbed by the auxiliary module, and introduces dynamic depth sampling (DDS). At 10B MoE and 600B token multi-scale validation, depth 3 still shows continuous improvement (DeepSeek-style MTP has saturated). Compared to the latent-space variant of LoopMTP in Issue 3, this work elevates MTP from an "auxiliary objective" to a "parameter-shared self-recurrent main objective," and DDS provides a new low-cost approach for long-horizon supervision. Note that the benefits of DDS in the pretraining phase only appear after SFT, so trade-offs need to be considered.
- A Quadratic Lens on Muon's Polar Update: Benefits, Pitfalls, and the Role of Newton-SchulzFor the first time provides exact one-step and trajectory-level analysis of PolarGD (the core update of Muon) on matrix quadratic forms, proving that its implicit preconditioner is determined by the current iteration covariance rather than the Hessian, and revealing that finite Newton–Schulz behaves as damped polar decomposition near rank deficiency, thus converging faster than exact polar decomposition—reinterpreting finite steps from approximation error to a beneficial damping mechanism. Compared to the stability phase diagram of Muon Sublates the Edge of Stability in Issue 9 and the zero-cost spectral estimation in Issue 8, this paper provides an exact quadratic theory for polar decomposition updates. The limitation is that the scale stops at 90M diagnostics, and transfer to large scale requires self-assessment.
Coding Agents · Issue 11
Benchmark Maintenance Becomes a First-Class Engineering Concern: Clean-Mirror Rescoring and Black-Box Pollution Forensics
The strongest signal this issue is that benchmark validity is shifting from "one-time hardening" to "continuous maintenance." SWE-Bench Pro V2 turns benchmark m…
SWE-Bench Pro V2: A Cleaner, Harder-to-Game Coding BenchmarkSWE-Bench Pro V2 turns "benchmark maintenance" itself into a reproducible pipeline: agentic audits triage, 23 engineers adjudicate each case, blind reimplementation verifies every fix, and for the first time "clean-container rescoring" is adopted as a locking protocol—saving agent changes as patches, rerunning invariant verifiers on fresh images, thereby blocking vulnerabilities where sandboxed dependencies or binaries bypass patches. Compared to the static hardening of SWE-Bench Pro Verified in Issue 5, it upgrades fix verification from model trial runs to blind reimplementation, and quantifies that 66% of tasks require fixes or retirement; its defect taxonomy and cost attribution (scaffold changes cost, not accuracy) are directly reusable audit templates. Note that the main benchmark is saturated (frontier 99.4%), but the Hard split provides discrimination.- What the Specification Did Not Say: Specification-Oracle Gaps in Test-Graded Coding-Agent BenchmarksThis work advances the validity issue of test-scoring benchmarks to the "specification-oracle gap": the mismatch between formal natural language task descriptions and the implementation details required by reference tests, providing a static audit tool across five languages that classifies name/path/literal-level dependencies of each scoring test (held-out precision 89.2%, recall 92.9%). It proves that 25/98 milestones in SWE-Milestone are affected, with a build-unit failure rate of 1.67×. Compared to ABA's static task audit in Issue 3 and TestJack's trial-level evaluator evolution in Issue 9, it is the first to treat "underspecified interfaces" as a first-class audit object, directly responding to the hard standard that new benchmarks must disclose pollution sources and hackability audits.
- BenchChecker: Assessing the Credibility of Bug-Fixing Benchmarks for LLMsBenchChecker is the first to advance pollution detection from task-level static checks to model-level black-box membership inference: leveraging the observation that code LLM training sets include recent repository snapshots, it uses a two-stage forensics approach—repository existence test (Bernoulli hypothesis test on signature snippets) and patch existence test (similarity alignment + test suite validation)—to detect bug-fixing benchmark pollution from text output alone, with AUC≈0.9 across six benchmarks and three known training-set models, and a relative drop of 20%+ in top-10 pass rates after filtering. Compared to SWE-Bench Pro Verified's static leakage audit in Issue 5 and ABA's agentic audit in Issue 3, it shifts the audit object from "whether tasks leak" to "whether the model has seen the answer." Limitations: Stage I relies on verbatim reproduction, may fail for agentic long-trajectory fixes, and the main experiments use 15B-level open-source models.
Recursive Self-Improvement · Issue 11
Self-Improving Measurement Itself Begins to Be Measured
The main theme of this issue is "self-improving measurement itself is being measured"—the field is beginning to audit its own evaluation practices through large…
Auditing the Product, Not the Recursion: The Evaluation Evidence Behind Recursive Self-Improvement ClaimsShould read. It advances the measurement of "self-improvement rate" from single papers to domain-wide census: full-text coding of 114 RSI studies within a frozen arXiv frame, separating "product claims" from "process claims," quantifying that 90% report product evaluations but only 22% audit two or more reruns, and only 4 of 26 improver claims use matched budgets and identical starting points. Compared to Issue 10's community column structured audit of 13 systems, the increment lies in full-text coding at full-domain scale, three propositions explaining selection effects/shared evaluator errors/state changes, and a claim-indexed reporting standard binding each claim to required evaluation design. It is an anchor point for designing any self-improvement closed-loop evaluation.- SimHack: Predicting the onset of detectable reward hacking before RL trainingShould read. It makes reward hacking onset prediction a measurable pre-training target: a lightweight behavioral simulator learns prompt-level dynamics from a few reference runs, counterfactually simulating hacking trajectories and onset distributions for unseen recipes without executing the target RL run. Compared to Issue 9's CATCH full-training dynamic evaluation and Issue 7's Reward Hacking Challenges external behavioral evidence, the increment lies in advancing prediction from "detection during training" to "prediction before training," with generalization evidence across model scales, curricula, rollout counts, and learning rates (median onset relative error 11.3%, cross-recipe rank correlation 0.85). Its curriculum filtering application delays onset by 96.6%, making it a strong pre-training risk screening tool.
- Automating ML for Science: Can Frontier Agents Climb Scientific Hills in the Wild?Should read. It turns "scientific hill-climbing" into a standardized testbed across 11 domains and 20 benchmarks: starting from published SOTA, agents improve under fixed budgets, all benchmarks are surpassed by at least one agent, but gains come almost entirely from ML engineering tricks rather than research insights. Compared to Issue 10's Into the Unknown scientist standard formalization, the increment lies in a reproducible 25-task/20-benchmark testbed, full standardization pipeline (497→10 funnel, 98% rejection rate), and a three-stage evaluation protocol making evaluation gaming an explicit audit object, with plug-in skills raising Opus from 10.4% to 20.1%. Limitations: no invalid run determination criteria reported, no human researcher baseline.
Looped Transformers & Latent Reasoning · Issue 3
Training Methods Become the New Battleground for Recurrent Depth: The Truncation Debate and Progress Alignment
The most prominent signal this issue is that training methods for recurrent models are moving from empirical recipes toward verifiable science. The scaling stud…
PAR: Progress-Aligned Recurrence for Length Generalization in State TrackingDepth extrapolation shifts from running more iterations to giving each iteration explicit progress: the progress-aligned objective makes the k-th iteration predict the state after the first k operations, combined with RMS norm anchoring to keep the step mapping stable, achieving 16x length extrapolation on swap-S5 (compared to 0.8% for explicit CoT), with ablations proving both are indispensable. It also provides label-free prefix self-distillation and a learned halting criterion. The limitation is that it applies to sequential state-tracking tasks with clear intermediate states, but it is the clearest depth extrapolation training objective design to date in this direction.- Truncate or Not? A Scaling Study of Looped Transformers with Truncated BackpropagationThe first unified scaling law that simultaneously models forward and backward recurrence counts, using nearly 600 training runs to answer the truncation debate: when both model size and compute are freely selectable, full BPTT outperforms truncation, and two fully trained recurrences can approach the non-recurrent compute-optimal model with approximately 27–32% fewer parameters. Relative to Iso-Depth and Parcae, which fix the backward recurrence or tie it to T, this is a clear increment with direct guidance for training recipe design.
- Loop the Loopies!Proposes the layer-loop pattern—each layer iterates locally before moving to the next—and a compute-matched scaling recipe (halving storage layers, doubling micro-batches, reinvesting memory gains into width/depth), transforming recurrence from a parameter-saving device into a compute-matched scaling mechanism, validated at 0.1B–20B scale with released 20B-A2B and 6B-A0.6B models. Relative to Ouro/Huginn's model-loop, this is a new architectural degree of freedom, directly responding to the previous issue's debate about scaling parameters versus scaling recurrence.