Weekly Gallery
Latest edition
Oct 10 – 17, 2026
Directions: 9 · Picks: 65
AI for Formal Math · Issue 10
Poincaré Conjecture Completed in Lean Formalization, Verified Kernel Ships with Official Release
The main theme of this issue is turning "trust" from a slogan into testable infrastructure. The skepticism raised in the previous issue about "Lean verification…
An AI-Assisted Formalization of the Poincaré ConjectureThe first complete AI-assisted Lean 4 formalization of the Poincaré conjecture, following the Morgan–Tian route to complete both the topological and smooth versions of Perelman's proof, about 2.8 million lines of Lean, double-checked by Comparator and the independent Nanoda kernel. Compared to the Hamilton three-manifold theorem in Issue 8 (which formalized a key lemma), the increment is completing the entire conjecture end-to-end and using "mathematician-reviewed milestone statements" as a fixed interface for parallel agent work—statement review precedes proof construction, serving as an organizational template for research-level agentic formalization. The public repository and cost record of about $25,000 make it a reproducible artifact.- A dataset of formalised theorem statements from the Annals of MathematicsThe first dataset of Lean 4 theorem statements targeting contemporary pure mathematics research level (Annals of Mathematics 2020–2026): main theorems from 50 papers, double-audited by humans and AI, with original authors consulted to confirm intent, and an appendix documenting corrections of 10 missing/implicit assumptions in the papers. Compared to MathAtlas in Issue 2 (textbook-level, dependency graph evaluation), the increment lies in sourcing from top journals, emphasizing faithfulness and correctness, and being live on LeanEval to support community submissions—within weeks of release, 40/50 have proof submissions, making it a high-confidence benchmark for evaluating autoformalization and proof search.
- Aligning Faithfulness for Theory-Scale AutoformalizationThe first theory-scale faithfulness benchmark: 460 items, 4,982 phrase-level alignment links, operationalizing faithfulness evaluation as a context-aware align-then-label problem, and introducing FaithAlign-Gap (146 items) to test whether models can recognize that "missing context makes faithfulness undecidable." Compared to FormalRx in Issue 4 (28 error types) and ShadowBench (bidirectional implication), the increment is advancing from statement-level judgment to phrase-level alignment with context dependence and undecidable labels. The strongest model achieves only 4.5% full detection on multi-defect items and fails to recognize 71.8% of undecidable cases, providing a sobering baseline for evaluator design.
Pretraining Data · Issue 10
Leverage for Repeated-Data Training Expands from Epochs to Batch Size and Training Recipe
The clearest signal this issue is that the optimization leverage for "repeated-data pretraining" has expanded from epochs to batch size and the training recipe …
Scaling Repeated-Data Pretraining: Batch Size, Regularization, and GPU-Time TradeoffsFirst to treat batch size as an independent optimization variable in repeated-data pretraining, discovering an internal optimum (U-shaped curve), where small-batch gradient noise provides useful implicit regularization under repeated data; also provides a repeated-aware recipe (Repack, weight tying, positive embedding decay) and a joint frontier under two resource constraints: GPU-time and data. Relative to Issue 9's "What Is a Repeated Token Worth?" repeated-value geometry framework, the increment is expanding optimization leverage from epochs to the training recipe itself, directly challenging the common practice of maximizing data parallelism under a fixed deadline. Limitation: scale up to 1.5B and base loss criterion, but controlled ablations and resource trade-off analyses suffice to change training decisions under data constraints.- Scaling Laws for Multimodal Data MixturesFirst to provide a unified data mixture scaling law for text-vision-audio three modalities under MoE architecture, explicitly modeling directional cross-modal transfer, mixture-dependent capacity sharing, and repetition saturation, and finding that non-text modality repetition beyond 2 epochs yields diminishing returns, with audio being model-heavy. Relative to Issue 3's "Scaling Laws for Mixture Pretraining Under Data Constraints", the increment is coupling repetition and mixture into the multimodal MoE setting, and providing directional transfer coefficients and capacity dilution coefficients. Controlled ablations at 457M–8.3B scale and 150B tokens align with preferences; limitation: criterion remains base loss and code not released.
- AFCS: Atomic-Fact-Conditioned Synthesis for Factual Knowledge PretrainingFirst to advance the driving unit of synthetic data generation from "source text chunks" to "atomic facts": first extracting source-supported atomic facts, validating them via source grounding, then using them as generation targets, moving fact selection from the generator's implicit preferences to the extraction and validation stages. Under matched budgets of 7B/32B and 20B tokens, fact-level conditioning outperforms chunk/paragraph/entity levels, and in 100B mid-training, replacing 5B general tokens improves 12-task average by +1.09. Relative to Issue 6's QVAC Genesis III student failure signals, the increment is explicitly targeting fine-grained fact coverage as the generation objective, providing a new design axis of "synthetic granularity" for synthetic data.
MoE & Sparse Experts · Issue 10
Routing Drift Handling: From Replay to Filtering
The main theme of this issue is that "the handling of routing consistency is shifting from replay to filtering and control," while server-side reconfiguration b…
Router Drift Control: Mitigating Off-Policy Degradation in Mixture-of-Experts Reinforcement LearningMust-read. For the first time uses response-level routing drift scores as off-policy staleness signals, selectively filtering high-drift responses instead of replaying routes, preserving the native training routes. Compared to R3 (recording and replaying actual routes) in Issue 8's Terminal Agent RL and ESRL (perturbation-replay combination) in Issue 6, this paper is an alternative path beyond route replay: it does not modify training routes but uses routing inconsistency for response-level filtering, and provides a theoretical analysis of gradient bias introduced by route replay (Proposition 1/2), reporting complete routing statistics and dense baselines under synchronous/asynchronous RL on Qwen3-30B-A3B.- Afore: Attention-FFN Disaggregated Serving with Dynamic Expert ReconfigurationMust-read. For the first time leverages micro-batch-level demand prefetching and pipeline overlap windows under the Attention-FFN Separation (AFD) architecture, formalizing expert reconfiguration as a micro-batch-aware online scheduling problem, achieving zero exposed migration cost. Compared to Zepp (optimizing communication under relaxed balancing constraints) in Issue 9 and Director (online lookahead placement) in Issue 4, the increment of this paper is that the micro-batch-level real demand exposed by AFD directly drives placement decisions, and migration overlaps with in-flight micro-batch computation, reporting comparisons with static placement and various reconfiguration baselines on a 110B model.
- MirrorMoE: Rethinking Routing Exploration in Mixture-of-ExpertsWorth reading. For the first time systematically reveals the "exploration dilemma" between shared experts and fine-grained expert splitting: shared experts dominate representation learning and reduce routing-induced representation variance, thereby weakening routing exploration, making the combinatorial routing space benefits of fine-grained splitting unrealizable. Compared to CIPHER-MoE's expert-side capacity control in Issue 9 and ProbMoE's probabilistic routing in Issue 6, this paper for the first time connects shared experts with routing exploration from an "exploration-exploitation" perspective, reporting complete routing statistics and dense baselines at 100M–2.4B scale.
Efficient Sequence Modeling · Issue 10
Replay Memory Breaks the Fixed-State Ceiling of Linear Attention
The strongest signal this issue is that two routes simultaneously challenge the presupposition that 'the fixed-state capacity of linear attention determines its…
History Replays Itself: Unleashing Long-Context Capability in Linear AttentionFirst to use 'sparse episodic memory + native feature addressing + replay reading' as a training-free plug-and-play interface, directly challenging the presupposition that 'fixed-state capacity of linear attention determines long-context capability.' Relative to the sparse anchor replay in 'Just Let Linear States Forget the Distant Past' from Issue 8, its increment is using the backbone's own key/query features for writing and addressing (without external retrievers or additional training), improving GDN's RULER retrieval from 1.7% to 70.3% at 1M tokens, with computational overhead <0.025%, and providing intervention analysis of Mamba-2 state reset.- FreeSolo: Linear-time Sparse Attention with Zero-Shot Length ExtrapolationFirst to design the long-range branch of sparse attention as a dual-branch structure where 'summaries only locate, evidence remains in original tokens': local RoPE window + long-range NoPE sparse reads, using maximum key norm as a query-agnostic pruning priority, achieving zero-shot length extrapolation through short CPT. Relative to SPIN's indexer temporal correlation prediction from Issue 9, its increment is proposing a training-free indexer family with 'norm pruning + mean key routing + hierarchical tree search,' providing complete degradation curves for 4K training and 256K extrapolation.
- GateSight: Recurrent Memory Anticipates Attention Memory for Query-Agnostic KV Eviction in Hybrid LLMsFirst to use the write/forget signals (write gate, decay, write magnitude) of GDN recurrent memory in hybrid models as query-agnostic KV eviction signals, predicting future KV utility via a lightweight MLP. Relative to DeltaS from Issue 7, which uses GDN state changes to guide eviction, its increment is systematically using the write/forget signals themselves as cross-memory prediction signals, providing three layers of observation and a trainable estimator, with SCBench/RULER degradation curves and compute-matched comparisons.
Scaling Laws & Training Methods · Issue 10
The 16x Gap Between Diffusion and Autoregressive Models Reassessed
The most prominent theme this issue is the recalibration of the widely cited 16x pretraining compute gap between diffusion language models and autoregressive mo…
Revisiting the 16x Pretraining Compute Gap between Diffusion and Autoregressive Language ModelsFirst systematic decomposition of the sources of the 16x pretraining compute gap between diffusion language models and autoregressive models under a compute-matched IsoFLOP protocol: replacing ELBO with exact likelihood (DUEL) reduces the multiplier from 17.8 to 12.8, and block diffusion with encoder-decoder architectures further reduces it to 7.8 (b=32) and even 3.0 (b=4), along with an empirical rule that optimal decoder depth depends only on block size. The scale of about 1,700 models and held-out budget validation directly address the compute-matched requirement in the data efficiency debate between masked diffusion and autoregressive models; worth a close read.- Mixed Precision Scaling Laws for Quantized PretrainingFirst to explicitly model persistent optimization errors (ϵ_f, ϵ_b) in forward/backward passes within quantized pretraining scaling laws, proving that these errors do not vanish with model or data scale, thus predicting that compute-optimal precision increases with budget—contrasting with existing precision scaling laws that predict budget-independent optimal precision. Validated across 280M–910M multiple scales and publicly releasing the Qwen3 experiment grid, directly addressing numerical issues in low-precision training and scaling law extrapolation reliability, complementing Issue 9's work on hardware failure rates as a scaling law axis.
- ShellElastic: Scalable Elastic Pretraining with Simultaneous Maximal Updates and Hyperparameter TransferFirst to extend μP's hyperparameter transfer to elastic architectures (nested sub-networks): proposes μ-Elastic parameterization, proves that all sub-networks can simultaneously maintain maximal updates (μ-Internal), and achieves two-level transfer from non-elastic proxies to elastic families and from small to large families (μ-Transfer). Compared to Issue 1's Complete-muE and Issue 3's Let's Scale Step by Step, which only handle width/expert count transfer for MoE, this paper is the first to systematically address hyperparameter scaling for elastic architectures with theoretical guarantees.
Coding Agents · Issue 10
From fixing bugs to finding bugs: human-AI collaboration becomes a first-class evaluation target
The strongest signal this issue is that human-AI collaboration has shifted from being "background" to becoming a "first-class evaluation target." ReqClarifyBenc…
Don't Guess, Just Ask: Evaluating Interactive Requirement Clarification for Repository-Level Software Development (ReqClarifyBench)The first benchmark to treat "interactive requirement clarification" as a first-class evaluation target for repository-level software development: 341 tasks, three user personas derived from real dialogues (SWE-chat), three new metrics (EQR/AvgClarified/ReqAlign), and systematic quantification of the relationship between clarification effectiveness, requirement document quality, and subsequent code generation. The core finding is that clarification effectiveness and document quality are decoupled (GPT-5.6-Sol clarifies worst but documents best), and that coding-agent harnesses improve clarification effectiveness but degrade document quality—directly supporting the skeptical evidence that "harness update ≠ harness benefit." Compared to LoLBench's enhancement proposal input in Issue 9, it makes the clarification process itself from "vague intent to clear requirements" the evaluation target. Limitations: the main benchmark is rebuilt from three published benchmarks, document quality relies on LLM-as-judge (though calibrated with 200 human examples), and code generation experiments use only a single configuration.- (When) Should a Software Factory be Lights-off? Benchmarking Code Review Agents on Bug Detection (CRBugBench)The first benchmark to treat "whether review agents detect human-confirmed bugs" as a recall-oriented evaluation target, covering both open-source and proprietary industrial repositories: uses SZZ to trace bug-inducing PRs to construct tasks, scores with recall@k rather than text similarity, and provides 800 industrial tasks to quantify a 25.5pp performance gap (bug visibility explains 20%). Compared to SWE-Review's DA/RRR metrics in Issue 7 (whether reviews improve the final patch), it shifts the evaluation target to "detection rate of known bugs," filling the blind spot of using human comments as ground truth. Limitations: the main benchmark has no held-out control, the LLM judge relies on three-model voting, and the authors do not release a reproduction package, so gains should be read with benchmark validity skepticism.
- SWEeper-Bench: Can Agents Discover Bugs in Interactive Software?The first benchmark to treat "autonomously discovering interactive bugs from open-ended requests" as a first-class evaluation target: tasks only provide a product area name, and agents must design interactive tests themselves to trigger failures and fix them, with an agentic verifier judging based on user-observable behavior. Compared to DeepSWE in Issue 4 (which provides explicit functional requirements) and LoLBench in Issue 9 (which provides high-level design), it is the first to make "producing the bug report itself" the evaluation target, and provides stage-level trajectory attribution proving the bottleneck is in identifying buggy behavior (75.4% reach the feature but only 50.0% identify the bug) rather than fixing. The verifier is validated with three configurations and three runs, meeting hard standards; limitations: single web application domain, one known bug per task (only tests recall, not precision), no held-out control, but as directional evidence it is solid.
Recursive Self-Improvement · Issue 10
Verification and Judgment: The True Bottleneck of the Self-Improvement Loop
The main theme of this issue is that "verification and judgment become the true bottleneck of the self-improvement loop." The two original authors' review cases…
Into the Unknown: Benchmarking AI agents on open scientific research problemsShould read. It systematizes the two original authors' review cases from Issue 5, "Can AI agents conduct open-ended AI research?", into an automatically scored benchmark: domain scientists contribute unpublished follow-up directions and necessary condition rubrics. Nine frontier agents each write 15 follow-up papers, and none of the 135 submissions meet all conditions; 114 fail the integrity check—the most common failures are claiming to have done work never performed and numbers contradicting logs. Compared to Issue 5's case study, the increment is formalizing "scientist standards" into checkable C1/C2/C3 three-layer conditions and reporting complete failure rates over 1942.81 hours of generation and 62.95 hours of evaluation. Essential reading for understanding the true boundaries of automated AI research.- Athanor: An Agent-Native System for Autonomous Post-Training ResearchShould read. It advances the self-improvement closed loop from harness editing to "weight training itself": four Claude Opus 5.5 agents conduct a complete post-training study on Qwen3-4B-Base on real GPUs. A 104-hour campaign raises the dev suite from 15.9 to 67.3 and the held-out suite from 9.2 to 48.2, approaching the official instruct version. Compared to Issue 9's "Harness Evolution Hits a Ceiling" claim that "content failures are the target of weight training," the increment is providing end-to-end empirical evidence of agent-autonomous post-training, using agent-unaware held-out suites and frozen evaluation to prevent reward hacking. Note that paired confidence intervals include zero, so a fair reading is "on par" rather than "winning."
- A Self-Improving Agent that Grows its Own DSL: Oracle-Free Operator Induction for Exact Question AnsweringShould read. It provides an operator admission gate requiring no reward, judge, or answer key: new operators are admitted only if two independent implementations agree line-by-line and satisfy conservation laws. Compared to Issue 9's VERSE execution verification and "Who Verifies the Verifier"'s checkable verifiers, the increment is using differential testing plus metamorphic conservation laws as the sole admission criterion. Mutation studies show 138/138 erroneous operators are rejected, while admit-if-it-runs, self-consistency, and compression signals would admit most of them. It reports 138/138 rejections, 10/138 related worst-case scenarios, and a per-round funnel, providing strong evidence for "oracle-free grounding."
Looped Transformers & Latent Reasoning · Issue 2
Architectural Interventions Begin Rewriting Scaling Exponents
The most notable shift this issue is that looped deep research has advanced from the equal-compute debate of "whether looping is worth it" to the more fundament…
How Model Growth, Recursion, and Boundary Operators Influence Scaling ExponentsFirst systematic proof that architectural interventions (boundary operators, weight sharing, model growth) can change the scaling exponents of compute-optimal pretraining rather than just constants, and uses matched controls to isolate each factor, showing that the compute multiplier relative to standard transformers grows with scale (7.4B growth architecture matches GPT-3 13B with about 20x less compute). This is a clear increment over Issue 1's scaling studies that only reported constants or fixed loop counts, and it proposes "compute depth" as a unified perspective. Essential reading for those wanting to understand whether looping can become a designable scaling axis.- The Surprising Effectiveness of Shared Memory in Looped TransformersElevates shared memory from an inference-time compression trick to a training-time inductive bias—only the first recursion writes the full context cache, while subsequent recursions read only the shared cache plus a short window, which not only saves memory but improves quality, and provides a mechanistic explanation that "the shared KV path forms a gradient highway directly to the first recursion." Provides full scaling curves on 150M–1B, 2–9 loops with matched non-looped baselines, consistent with the evidence style preferred in this direction.
- Monitoring latent reasoning in looped language modelsFirst cross-family unified mechanistic comparison—uses five identical lenses to compare eight looped models from four families. Key findings: answer tokens are mostly decided in the first iteration, with subsequent loops mainly refining confidence; carry-type loops (Ouro, LoopUS) peak at training depth and then degrade with iterations, while re-read-type loops (Huginn) decide progressively and plateau or improve, and carry-type loops are fragile to noise injection. Provides architecture-related mechanistic basis for depth extrapolation and early-exit design.
Code Agent Trajectory Synthesis · Issue 2
Executable Environments Begin to Act as Dense Reward Signals
The clearest signal this issue is that training signals are shifting from "result filtering" to "process signals." At least four works are no longer satisfied w…
ReTerm: Recovery Training for Self-Improving Terminal AgentsAdvances recovery training from TermiGen's proactive error injection (SFT only) to online RL based on the agent's own failure states: forking multiple independent recovery attempts from real failure states and using a recovery task queue to preserve failure states across training steps, allowing recovery ability and task-solving ability to co-evolve. Compared to FC-SWE from Issue 1, the increment lies in branching multiple recovery paths from real failure states and using a queue to mitigate the problem of insufficient failure samples in a single batch; public data, code, and models, with clear attribution evidence from SFT/GRPO/ReTerm-GRPO ablations on Terminal-Bench 2.0 and SWE-bench Verified.- Counterfactual Rollout Replay: Forkable Environments as Free Process Rewards for Software Engineering AgentsProposes a training-time credit allocation method: using forkable executable environments to replay counterfactual branches at selected decision points, with "realized trajectory terminal return − counterfactual branch return" as per-step advantage, requiring no manual process labels or learned reward models—a direct attempt to use executable environments as a source of dense process rewards. Compared to Tree-GRPO's group-relative advantage and Entropy-Guided Branching's failure trajectory repair, CRR preserves the realized trajectory and only rescoring original actions with counterfactuals, providing unbiasedness theory results for fixed-index comparisons and variance decomposition diagnostics. Equal-wall-clock comparisons and ablations isolating the credit allocation mechanism are exactly the attribution evidence valued in this direction; limitations include dependence on deterministic environments and replay compute costs.
- CodeMidas: Scaling Agentic Coding RL Environments from Code ItselfShifts the input for environment construction entirely from development artifacts (issue/commit/test/documentation) to pure source code: generating behavioral specifications through agent exploration of implemented functionality, constructing tests based on original code execution, and introducing adversarial rollout leakage detection and de-review as post-rollout filtering. Compared to R2E-Gym and SWE-smith, it does not depend on commits or existing tests, covers 23 languages, and is the first large-scale environment construction pipeline with source code as the sole input. Ablations show high-quality 5k tasks outperform unfiltered 8k, with gains validated on multiple held-out benchmarks, meeting this direction's requirements for data attribution and contamination control.