Weekly Gallery
Latest edition
Aug 22 – 29, 2026
Directions: 7 · Picks: 52
AI for Formal Math · Issue 3
Issue 3: The Kernel as the Trust Chain — AI Attacks the Lean Kernel and the Rise of Open-Weight Proof Engines
The most central signal this issue comes from the very bottom of the "trust chain": the Lean kernel itself. Leonardo de Moura's postmortem report on the kernel …
MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided RefinementMathForm's increment lies in integrating Mathlib knowledge retrieval and verification-guided iterative refinement into a closed-loop automated formalization data pipeline, and explicitly quantifying the contribution of subsequent refinement rounds to data volume (31%), separating the gains of retrieval and feedback via controlled ablations. Compared with prior retrieval- or feedback-based works (such as DRIFT, ReForm), its core distinction is treating both as complementary components of a data construction pipeline rather than using them only at inference time or for single-round generation. The constructed FormalVerse dataset (approximately 367,000 verified samples) and the significant improvement of an 8B model on FATE-H/X validate the critical role of data quality for semantic faithfulness; code and data are public, making this a must-read for those working on automated formalization data construction.- FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal EvidenceFaithSieve introduces a Lean-assisted framework for locating the first error in natural language proofs, handling both types of mismatch: locality (decomposing coarse-grained steps into EdgeUnits of the proof state tree) and semantic faithfulness (gating formal evidence with semantic alignment scores). Its substantive increment over Pistis from the previous issue (#2) is that Pistis enforces faithfulness in formalization but does not use it for proof error localization, whereas FaithSieve systematically uses type-checked obligations and faithfulness-gated formal evaluation agents for fine-grained proof auditing—Lean is not used as a direct judge of the whole proof, but as a structured evidence source gated by semantic alignment. The ProofLoc dataset and ablations clearly separate the contributions of local decomposition and semantic gating, providing an actionable complement connecting LLM mathematical reasoning with formal verification.
- The set of primes is supernatural: a Lean formalization of the statement of the conjectureThis work provides a complete, sorry-free Lean 4 formalization of Mayeux's conjecture that "the set of primes is supernatural": every definition, example, remark, numbered result, and experimental table row in the paper has a machine-checked counterpart, and the central conjecture is precisely stated as a named open problem, with extensions to Knuth arrows, factorial, and truncated subtraction, using kernel-verified Lucas certificates for large primality assertions. Compared with benchmarks such as MathAtlas and Formal Conjectures that only cover statements, it provides a self-contained, kernel-verifiable open proof target through exhaustive coverage of a single paper, making it an ideal artifact for testing proof search systems.
Pretraining Data · Issue 3
Issue 3: Repetition Tolerance under Mixed Ratios and Post-Training Ceiling
Under data constraints, a core conclusion that may rewrite mixing ratio decisions emerged this week: mixed training has a much higher tolerance for repetition t…
Scaling Laws for Mixture Pretraining Under Data ConstraintsFirst to explicitly couple target domain weight h and repetition factor r into data-constrained mixture scaling laws. Core finding: general data as a regularizer allows mixed training to tolerate 15–20 repetitions (far exceeding the single-source <4 rule of thumb), and provides functional forms to predict optimal target weight from data volume and compute. Relative to #2 issue Scaling Domain Data Repetition (only studies domain-level repetition, not mixing weights) and #1 issue InfoLaw (models repetition as an independent term rather than a function of mixing ratio), the increment is the coupling of r and h and the mechanistic explanation of "general tokens never saturate." Evidence covers multilingual/domain/quality-filtered mixtures across 2000+ runs, but stops at ≤805M and uses validation loss as the criterion; needs cross-reading with larger-scale validation.- CuraWeb: Joint Optimization of Quality, Redundancy, and Diversity for Web-Scale Pretraining DataAdvances web-scale corpus construction from single quality filtering to joint optimization of quality-redundancy-diversity: domain-aware thresholds (STEM/code priority bypass) respond to #1 issue A Bitter Lesson's "more filtering is better" challenge, but implement via in-domain recalibration rather than global removal; soft semantic deduplication reduces the false deletion rate in the highest similarity interval from 37.5% to 28.03%. At 3B scale, 200B–1T tokens, with per-component ablations, evidence strength exceeds most corpus papers; limitation is that it still uses base benchmarks as the criterion and the corpus is not public.
- MIRA: Mid-training Rubric Anchoring for Source-Aware Data SelectionAdvances mid-training data selection from fixed rubrics to "source-aware rubric discovery": automatically induces quality criteria per source group, distills them into scalable scorers, and pairs with source-conditional reliability masks and group-wise retention thresholds. Relative to #2 issue MidTool's content heuristics, the increment is making "what to evaluate" itself an empirical product, with evidence at 14B scale and half token budget; limitation is that the code-oriented setting limits generality.
MoE & Sparse Experts · Issue 3
Issue 3: Causal Decomposition of Routing Drift and Scaling Evidence for Sparsity and Granularity
This issue features two main threads: one provides a causal-level decomposition and counterintuitive negative results on "routing drift," and the other delivers…
Slicing and Dicing: Configuring Optimal Mixtures of ExpertsMust-read. The most systematic decoupling of sparsity and granularity to date: 2000+ pretraining runs (up to 6.6B total parameters) jointly exhaust expert count, granularity, heterogeneous pools, and shared experts. With FLOPs matched, performance improves monotonically with total MoE parameters (even at s=128 extreme sparsity), optimal granularity depends only on activated parameter count, and heterogeneous/shared experts offer no gain over well-tuned homogeneous MoEs. Directly corrects prior scaling-law conclusions about fixed optimal activated-expert counts and the necessity of shared experts, and provides new empirical baselines for sparsity and granularity research.- Launch-Bound and Substitutable: Why Three Inference Optimizations Fail to Pay Off in Mixture-of-Experts ModelsMust-read. Uses causal routing replay interventions to separate routing changes from weight errors: INT4 changes 0.53/8 experts per token on average, but replaying quantized routing on full-precision weights reproduces only 2.7% of quality loss—experts are substitutable, not specialized. Exempting the router from quantization reduces drift by 20% yet increases loss, proving routing fidelity and output quality are separable. Also reveals the model is launch-bound rather than arithmetic-bound: eliminating all graph breaks makes it 3× slower. Directly challenges the premise of routing-replay/compensation methods.
- Routers Learn the Geometry of Their Experts: Geometric Coupling in Sparse Mixture-of-ExpertsMust-read. First to show from a gradient-structure perspective that routers and their selected experts accumulate gradients along the same input direction (geometric coupling), and that auxiliary load-balancing losses break this coupling by injecting input-direction gradients into all router weights (directional cosine similarity increases nearly 3×). Provides a mechanistic explanation for why bias-only balancing preserves specialization without auxiliary losses. Compared to last issue's #1 From Observation to Intervention (token-level causal auditing) and #2 Beyond Geometric Complementarity (geometric overlap and functional value), this paper offers a gradient-level mechanism and theoretical grounding for auxiliary-loss-free balancing.
Efficient Sequence Modeling · Issue 3
Issue 3: The Ceiling of Selectors and the Audit of Evaluations
The most noteworthy signals this issue come from the evaluation and audit side: the "ceiling" of selectors has been quantified for the first time. Trust the Mas…
Trust the Mass: Forced Weights in KV-Cache EvictionFirst to systematically quantify the "selection ceiling" under forced weight renormalization: enumerating optimal subsets over 168k attention rows proves top-mass selection is near-optimal (only closing a median gap of 2-5%), and decomposes gaps among published eviction methods into memory accounting artifacts (mask storage occupying cache) and query visibility leakage (87.6 points of retrieval gap attributable to the ordering of visible questions). Relative to [#2] RestoreKV and [#1] How Query Visibility, it provides an upper bound for any selector improvement and proves that many published gaps are measurement artifacts rather than algorithmic gains; ContourKV's allocator is a minor contribution, but the measurement framework and negative results are essential reading.- Massive Activations in Hybrid Linear Attention Large Language Models: Pre-Attention Spikes and Inter-Spike PlateausFirst to systematically characterize the layer-wise organization of massive activations in hybrid linear attention: identifies pre-attention spikes and inter-spike plateaus, both aligned with full attention layer positions, and explains their continuous spectrum with the mixing ratio via a unified lifecycle of write-sink-cancel and delayed cancellation. Relative to [#1] Rethinking's "large-window laziness" and [#2] RoPE frequency axes, it advances the optimization prior of efficient attention to the layer-wise organization and cancellation timing of massive activations, providing causal evidence through controlled pretraining and output gating interventions.
- When Do Attention Circuits Form? Developmental Trajectories of Capability and Attention-Sink EmergenceFirst to construct a developmental panel tracking attention sinks and induction circuits across 30 checkpoints: proves that induction circuits and BOS-attractors form in two independent phases (with a 10-20× difference in token count) and that the L0/L1 zero BOS floor is an architectural property, not a learning outcome. It provides direct constraints for architectures that deliberately avoid sinks and transforms "when sinks form" from a static observation into an intervenable training-phase question.
Scaling Laws & Training Methods · Issue 3
Issue 3: Mechanistic Localization of Low-Precision Numerical Channels and Muon Spectral Scaling Laws
This week's low-precision training leads show a notable convergence: two independent works recharacterize "loss spikes / training collapse" from optimization dy…
One QK Channel, Many Sources: Guarding Low-Precision Attention CollapseReframes low-precision training collapse from "source-by-source fixes" to "single-channel blocking": proves that different bf16 failure sources such as streaming-softmax accumulators and weight gradient quantization all converge to the same QK spectral runaway channel, with the entry determined by temporal sign consistency of per-head errors rather than aggregate magnitude. QK-Guard uses parameter-free QK normalization for triggered blocking at the QK site, matching always-on QK-norm within 60k steps, and reproduces across architectures and a second GPU. A mechanism-level rather than patch-level contribution to low-precision training stability.- Let's Scale Step by Step: Compute-Efficient Hyperparameter Transfer for Large-Scale Mixture-of-ExpertsOn the muP-for-MoE line (contrast with MSSP and Complete-muE in Issue 1, which only handle width/expert-count transfer), this work is the first to include the token dimension in the same framework: first adapt μP to MoE (including MLA and Muon) to validate width transfer, then use EMA weights to extract optimal learning rates at multiple token budget points from a single short-budget run, fit a log-log linear law extrapolated to 10T tokens (R²=0.95), and validate on 155B/17B. The increment lies in the EMA trick and the token-dimension learning rate scaling law, but the extrapolation span from 255B–500B to 10T is large; readers should assess the risk themselves.
- Grokking or Glitching? How Low-Precision Drives Loss SpikesProvides a mechanistic proof of Slingshot loss spikes: they are not intrinsic optimization dynamics but numerical artifacts of finite-precision cross-entropy computation. When the difference between the correct-class logit and the rest exceeds the absorption error threshold, the correct-class gradient is rounded to zero, breaking the gradient zero-sum constraint, forming a positive feedback between classifier mean and feature mean (Numerical Feature Inflation), driving exponential norm growth and spikes. Recharacterizes loss spikes from an "optimization problem" to a "numerical problem" and offers a testable intervention (restoring the zero-sum constraint).
Coding Agents · Issue 3
Issue 3: Harness Security Becomes a First-Class Research Subject, Skeptic Evidence and Long-Horizon Transfer Benchmarks Tighten in Tandem
The most notable shift this issue is that harness security has been elevated from a "hidden variable being evaluated" to a "first-class research subject." Two w…
EVOMAL: Self-Poisoning in Self-Evolving Coding AgentsThe first work to characterize 'create-path self-poisoning' of self-evolving coding agents as an independent vulnerability class: after retrieving an implanted skill, the agent writes and stores a malicious skill itself, turning a single retrieval into a self-propagating worm that persists even after the seed is removed. It adds a 'security' dimension to the 'capability' discussion of self-evolving harnesses since Issue 1, and provides counter-prompt defenses and clear metrics. Essential reading for anyone engineering or auditing self-evolving/self-improving harnesses.- When Context Gets Root: Privilege Escalation in LLM HarnessesProposes 'instruction privilege escalation' as an independent attack paradigm: unlike prompt injection (content stays at original level) or role confusion (model misinterprets role), the harness itself elevates tool-level content to user/system-level messages (sub-agent delegation, persistent goals, scheduled tasks, custom subagent installation) during context reconstruction. Systematically evaluated across six coding-agent harnesses and 13 attack targets, proving it bypasses the working agent's instruction hierarchy and automatic permission review. This is a security-critical complement to Issue 2's harness effects and reward hacking themes, providing actionable context reconstruction design constraints for harness builders.
- Rethinking the Evaluation of Harness Evolution for AgentsProvides the cleanest budget-matched comparison to date: under matched feedback and inference budgets, compares automatic harness evolution against test-time scaling baselines like parallel sampling and sequential refinement, and evaluates on held-out tasks. Conclusion is that evolution does not consistently outperform simple test-time scaling, and evolved harnesses overfit the search set (held-out average only +0.6pp). Compared to Issue 1's 'Don't Blame the LLM' and Issue 2's 'Scaffold Effect,' it advances gain attribution to the level of 'is it harness design or just search budget.' Limitation is single benchmark (Terminal-Bench 2.1) and lack of code-level failure analysis, but the protocol itself is a template for fair evaluation.
Recursive Self-Improvement · Issue 3
Issue 3: The Loop Breaks at Self-Evaluation — Failure Localization and Self-Evaluation Adoption
The main thread this week: where does the loop break? Last issue, we turned "self-improvement rate" into an audit discipline (migration-level, algorithm-design-…
How Do Agents Fail on AutoResearch: End-to-End Diagnostic Evaluation on 100 Real-World Frontier Research TasksMust-read. It localizes "where the self-improvement loop breaks" to a specific stage: AutoResearchEval provides 100 real frontier research tasks and 800 trajectories; ARFT induces 45 empirically grounded failure modes, with the core being "F.4 uncorrected self-awareness" — in 82.5% of analyses, agents correctly diagnose fatal flaws during self-evaluation yet still deliver unchanged, directly quantifying that "self-evaluation is just more text; nothing in the system requires review to change the report." Compared to last issue's [Rollout Cards] auditability of reports and [AI4AI-Bench] execution/learning-side patch classification, this moves failure diagnosis from trace-level to artifact-level (judge reads the full run directory to find failures invisible in the report). Limitation: 45 modes from a single preprint; judge validation not stratified by mode; no test of whether orchestration intervention can fix the flaw.- When Do Agent Loops Mistake Stagnation for Progress? Self-Evaluation Bias and Externally Grounded Verification in Long-Running Autonomous LLM Agent LoopsDirectly hits "self-improvement rate" measurement: over 54 loop rounds, agents claim improvement every round, but 56% of rounds have measured delta at zero or negative; self-evaluation gating degrades to accept-all, eroding best performance by 19%; even the strongest in-band judge (reading full text, diffs, and its own adjudication history) accepts 44% of true regressions and rejects 38% of genuine improvements. Compared to last issue's [Phantom Gains] transfer-level auditing and [One Run Is Not an Idea] implementation lottery, this provides longitudinal measurement of self-evaluation bias and proves that "progress illusion" depends on the information channel available to the evaluator, not its quality. Limitation: full text unavailable; author signals weak; methodological rigor cannot be fully assessed, but the concrete numbers and focus make it worth reading.
- Recursive Experiential-Working Memory Evolution for Long-Horizon Agent HarnessesA strong sample of component-decomposed self-improvement: decomposes memory into EM/WM/call-policy/inspector four components, uses trace to localize failures to specific components, then applies verification-gated local patches; trace-based localization achieves 64.8% vs 13.0% for outcome-only inspection. Compared to last issue's [EvoMem] write/read two-stage and [Harness Continual Learning] four-component gating, the increment is an explicit four-component patch space with double separation — key memory components vary by domain, supporting trace-driven rather than design-time allocation. Reports gated rejection of 18 candidates, invalid run determinations (e.g., Run B round-4 never invoked), and cross-model transfer. Read it for trace-driven failure localization protocols and what gating discards.