Weekly Gallery
Latest edition
Nov 7 – 14, 2026
Directions: 9 · Picks: 58
AI for Formal Math · Issue 14
Prover training shifts toward agent-native data, verification becomes the new bottleneck
Last issue, we paused at the route divergence of "whether minimalist test-time scaling unconditionally dominates complex harnesses." This issue, the artillery o…
Reap: Uncovering Monte Carlo proof search with a lightweight modelImplements MCTS directly as a tactic in Lean 4, enabling training and inference to share the same search and replay verification, achieving 79.9% pass@32 on miniF2F with a 1.7B model; code and weights are open-sourced. Compared to NanoProof (factorized execution-guided search) in issue 12 and SCOPE (strategy planning) in issue 11, its increment lies in the observability design of Lean-native MCTS and the first systematic characterization of how RL reshapes proof search—later models tend to use structured macro-actions like have/suffices to compress search depth into fewer but more compound steps (search-interaction compression). This behavioral analysis is particularly valuable for designing training objectives and search strategies.- daVinci-Prover: Agent-Native Mid-Training for Formal Theorem ProvingThe first work to systematically introduce agent-native mid-training in Lean 4: in a 33.7B-token mid-training corpus, it explicitly injects decomposition, search, self-verification, and revision skill priors, along with environment-native agent trajectories to bridge the distribution gap between static training and interactive reasoning. Compared to NanoProof (publishing proof tree datasets and training pipelines) in issue 12 and OProver (65B mid-training but without agent-native trajectories) in issue 11, its increment lies in clear ablations: the gain from 8.4B agent-native tokens exceeds that from 25.3B general skill tokens, and the two are complementary. The harness design (7 tools, isolated workspaces, strict verification) and memory compression mechanisms are also worth borrowing; note that it relies on frontier closed-source models for data generation and code is not yet public, so results should be treated as relative signals.
- TCSExam: Evaluating Frontier LLMs on the Full Range of TCS ResearchThe first to unify theorem proving, solver engineering, construction, and open conjecture resolution into a single evaluation framework, with all tasks verified by the Lean kernel or executable checkers, and introduces the Lite subset (20 tasks) retaining strong rank consistency with Full using 80% fewer attempts (Spearman ρ=0.93). Compared to reuF2F (only open conjecture formalization) in issue 11 and the Annals dataset (only theorem statements) in issue 10, its increment lies in covering the full spectrum of TCS research output types and reporting independent verification progress on open conjectures like nine-dimensional Alon–Jaeger–Tarsi. The theorem proving track's bare/ladder/guided three settings and verification protocol are reusable for proof search evaluation; results partially depend on frontier closed-source models, so they should be treated as relative signals.
Pretraining Data · Issue 14
The value of data curation is explicitly priced: the distinction between advancement and acceleration
The clearest signal this issue is that "the value of data curation is explicitly priced"—gains are decomposed into two separable effects: advancement (endpoint …
Advancement or Acceleration? How Data Curation Improves LLM TrainingFor the first time, decomposes data curation gains into two separable effects—advancement (endpoint improvement) and acceleration (faster convergence)—and proves that advancement requires a correctable train–target gap, deriving the Δ-test diagnostic computable in advance from a single uncurated baseline run. Relative to Issue 8's Everything in Moderation and Issue 11's Learning from the Gap, which focus on coverage and pass@k gaps respectively, its increment is unifying contradictory findings like "unified mixtures are competitive" and "random selection is competitive" into a gap-dependent picture, with controlled no-gap and with-gap comparisons on 160M/1.1B. For mixture decision-makers, "run Δ-test first then decide whether to invest curation compute" is a directly usable judgment tool.- DataFlex-RL: An Evaluation Platform for RLVR Data PoliciesFor the first time, under the RLVR post-training setting, with 12 matched seeds and 13 configurations in systematic comparison, proves that three data strategy types—selection, reweighting, and adaptive mixing—under a unified GRPO recipe cannot yield reproducible gains (all paired 95% confidence intervals contain zero), and quantifies the impact of evaluation summaries on method rankings (math-heavy summaries and 12-benchmark summaries are negatively correlated at ρ=-0.33). Relative to Issue 9's What pass@k Cannot Measure, which focuses on post-training evaluation blind spots, its increment advances data strategy criteria from single benchmark scores to paired confidence intervals and evaluation sensitivity analysis. It is a strong negative baseline that any study claiming RLVR data strategy gains must compare against.
- SPT: Skills as Pre-Training Data for Agentic Language ModelsFor the first time, introduces public multi-file skill packages (human-written reusable tool semantics and workflows) as a mid-training corpus source, and proposes the Reference Insert citation-aware serialization strategy, outperforming general corpora and agent trajectory corpora across six backbone×SFT settings from 1.6B–7B. Relative to Issue 11's Priming Base Models for agentic mid-training recipes, its increment shifts data sources from trajectories/synthetic calls to human skill packages that do not require environment execution, and provides ratio evidence for a 20–50% skill ratio sweet spot (30% optimal; both endpoints worse than intermediate mixtures). Limitations include a single data source (ClawHub) and criteria based mainly on agentic benchmarks, but as a new data source and ratio sweet spot, it is worth reading.
MoE & Sparse Experts · Issue 14
In-Switch Replication and Eviction Rules: A System-Side Reassessment of Expert Parallel Serving
The main thread of this issue runs along two parallel lines: "system-side optimization of expert parallel serving and load balancing" and "new evidence on the s…
ISER-MoE: Dynamic In-Switch Replication of Hot Experts for Load Balancing in Expert-ParallelMust-read. The first to use NVLink switch in-network multicast (NVLS) for per-call weight replication of hot MoE experts, resolving the contradiction between fixed multicast members and per-layer changing demands via "fixed alignment groups rather than fixed replicas," and introducing SAMI multi-port broadcast to distribute injections to group member ports, hiding replication with a shared expert computation window. Compared to the point-to-point replication of MegaFlux in Issue 8 and UltraEP in Issue 4, this paper is the first to do per-call replication inside the switch, reporting end-to-end gains, full routing statistics, and dense baselines on GB300/Rubin hardware.- Fewer Expert Transfers Without Changing Routing: Expert Eviction for MoE OffloadingMust-read. Directly compares eviction policies with routing-changing policies under real CPU-to-GPU copy measurements, proving that Belady-style farthest-future eviction without changing routing reduces copies by 2.1x compared to LRU with zero quality loss, with 16-token lookahead recovering 96% of the gains, and disproving the common assumption that "fewer routing switches mean fewer copies." Compared to the runahead scheduling in Issue 13's Accelerating Offloading-Based MoE Inference, this paper focuses on the eviction rule itself without changing routing decisions, reporting full routing statistics and dense baselines.
- MoE Pretraining:Parallelism Layout Changes the Model, Not QualityMust-read. The first to show through controlled experiments that the parallelism layout (DP/EP combination) itself can cause routing drift close to seed-level differences: the layout does not change quality, but at the end of training, prediction differences reach about 80% of a new seed, with over 90% of routing decisions differing, and the root cause is traced to router near-ties (AUC 0.97–1.00), separating numerical effects from definitional effects. Compared to Issue 13's focus on inference-time/RL routing consistency, this paper is the first to establish a causal link between layout and routing drift in the pretraining phase, suggesting that layout should be a key recorded variable for routing replay and interpretability work.
Efficient Sequence Modeling · Issue 14
KV Cache Becomes a Translatable, Discretely Compressible Object
The most prominent signal this issue is that the KV cache has evolved from a 'compressed object' to a 'translatable, cross-model transferable object'. Translati…
Translating KV Caches Between Hybrid-Attention Language Models: MLA Latents, Linear-Attention States and Sparse-Attention IndexersFor the first time extends KV cache translation from GQA to all objects of hybrid attention models—MLA latent, KDA/GDN recurrent states, and sparse attention indexer keys—and provides capture/injection points and mechanisms for each object; its token identity decoding (recovering token identity from source layer-0 MLA latent) improves needle recall from 0.09 to 0.99 (2-32K) and 0.83-1.00 (64K). Relative to existing GQA layer-wise linear mapping and one-to-one state transfer, the increment is covering all cache objects of current hybrid models and providing complete evidence for bidirectional, multi-round, and indexer rehearsal. Must-read for those doing cross-model cache reuse and hybrid architecture KV translation; limitation: multi-round part is only single-seed.- Transformer-FSQ: Discrete Latents for Extreme KV-Cache CompressionFor the first time advances KV cache compression to a 'wide and low-bit' discrete finite scalar quantization (FSQ) bottleneck: compressing once on a shared residual representation, storing as bit-packed integer codes, without per-token metadata, codebook-free and search-free, end-to-end trainable, with closed-form initialization and fused decoding kernels. Relative to DCKV's trainable transform coding from Issue 12 and iS-KV's online low-rank from Issue 9, the increment is providing a VQ-collapse-free discrete bottleneck and establishing a retrieval accuracy frontier at 12×–97.5× extreme compression. Those doing trainable KV compression should read; limitation: long-context evaluation only up to 8K/32K.
- SinkState: On-the-Fly SVD of Recurrent States for Efficient Hybrid LLM ServingFor the first time reveals that q/k/v in linear attention layers concentrate in a stable low-dimensional subspace (linear attention sink), and accordingly proposes maintaining recurrent states throughout decoding with adaptive low-rank SVD: local SVD merges only top subspaces, asynchronous CPU merging, per-state variable rank, avoiding full state read/write each step. Relative to Shallow Encoding Emits Deep Memories from Issue 13 (state sink + low-rank storage), the increment is advancing low-rank maintenance from static/periodic compression to online adaptive serving systems, with evidence of end-to-end speedup across 4B–120B models (1.25× decoding, halved state memory). Those doing state representation on the hybrid inference side should read; but 16K NIAH is its long-context evidence upper bound and lacks compute-matched comparison with full attention.
Scaling Laws & Training Methods · Issue 14
The "Pathology" of Scaling Law Extrapolation Dissected: Pre-asymptotic Expansions and Negative Results under Data Constraints
The most prominent thread this issue is the further dissection of the reliability of scaling law extrapolation itself. Beyond the Log-Linear Frontier (https://a…
Beyond the Log-Linear Frontier: Pre-Asymptotic Analysis of Finite-Budget Neural Scaling LawsFirst to introduce Mellin–Barnes residue expansions and KKT dual water-filling methods into the pre-asymptotic analysis of finite-budget scaling laws: provides a third-order capacity expansion, pole-coalescence logarithmic corrections, Aitken delta-squared identification, and a variance identity for the drift of the compute-optimal allocation exponent, validated on Pythia, Chinchilla, and RegMix. Compared to Ambiguous Fits in Issue 12, which focused on the uncertainty envelope of fitting families, this paper provides an analytical characterization of 'why extrapolation deviates' from spectral geometry and identifiability analysis, directly addressing the core issue of scaling law extrapolation reliability. The limitation is that the theory is based on spectral assumptions and quadratic risk reduction, and quantitative transfer to real Transformers requires self-assessment.- When and How SignSGD Outperforms SGD: A Functional Scaling Law PerspectiveFirst to extend the functional scaling law of SGD to sign-based optimizers: rigorously derives the signal learning and noise forgetting laws for SignSGD in power-law kernel regression, revealing that gradient noise induces an effective preconditioner through the smoothed sign operator (transforming the effective Hessian from H to H^{1/2}), thereby achieving a faster data scaling exponent in the hard-task regime and a larger critical batch size in the easy-task regime, and provides an explicit phase diagram for when it outperforms SGD. Compared to the noise geometry analysis in When and How Does Muon Precondition from Issue 12, this paper generalizes the noise-induced preconditioning mechanism to sign operators and provides a complete batch-size dependence. The limitation is that the theory relies on diagonal feature and noise-curvature alignment assumptions, and LLM experiments stop at 0.1B.
- Factored One-sided Adam-Moment for Practical and Scalable SOAPFirst to provide a structural criterion for SOAP-class optimizers to retain the input-side Kronecker factor and discard the output-side factor (based on the Kronecker structure of the Hessian and the near-diagonality of the output side), reducing the SOAP state from 2mn+2m²+2n² to mn+2n²+m+n, maintaining a loss gap within 0.005 nats compared to SOAP/Muon on models from 124M to 1.56B, and reporting layer-wise Gauss-Newton alignment and K-FAC violation degrees. Compared to the unified framework in A Statistical Viewpoint from Issue 11, this paper provides the first rigorous theoretical basis for input-side priority and layer-wise alignment measurements. The limitation is that the scale stops at 1.56B, and no extrapolation residuals or training curve stability are reported.
Coding Agents · Issue 14
Repository context is the main variable of behavior
The strongest signal this issue is: repository context and existing state, rather than the base model itself, are the main variables determining agent output. E…
Coding Agents Propagate Vulnerabilities in Code BasesFor the first time, the security state of existing repository code is treated as a first-class independent variable. Paired secure/insecure context interventions prove that agents copy vulnerabilities from existing code: on C/C++ repository-level tasks, the average difference between secure and insecure contexts is 35.4%, and agents can identify the vulnerabilities they introduced (69.9%) yet still attribute their choices to "following existing code" (76.5%). Compared to BOBA in Issue 13, which used "verification state" as a control variable, this treats "context security" as the sole variable, directly hitting "harness updates ≠ harness gains"—following style prompts amplifies propagation, safety prompts can only narrow the gap but not eliminate it, and the public code and trajectories meet hard standards.- CoReMem: Cost-Internalizing Memory for Successive Coding Tasks with Prospective ValuationFor the first time, the value of cross-task memory is defined as the prospective value for unknown next tasks on inherited repository state. Anchor memories (location + executable checks) are induced from trajectories via segment-wise ablation, and then memory value is internalized as a training signal into the actor via provenance-gated credit. Compared to the delivery-level usage evidence of Delivered, Not Used in Issue 13 and the paired-replay compression evaluation of Compact-Bench in Issue 12, it upgrades memory from an evaluation metric to a training signal, and uses real repository chains from ChainSWE, paired on-policy groups (including misplaced memory controls), and cache-aware token costs for attribution, with M2/M3 ablations providing mechanistic evidence.
- Beyond the Model: Demystifying Harness Effects in Software Engineering AgentsFor the first time, the joint effects of model capability, harness complexity, and task type are separated on a unified three-dimensional matrix (3 tasks × 2 harnesses × 10 models), and NanoHarness is constructed for five-component item-by-item ablation. The core is cross-task non-monotonic evidence that "harness gains converge as model capability increases" (Qwen gap drops from 6.00pp to 2.67pp), and for the first time quantifies component-level negative effects of "context compression and general subagents hurting performance" on repository generation tasks. Compared to the VCR of When Agents Fail in Issue 12 and the component ablation of An Empirical Study of Harness Design in Issue 6, it provides cross-task non-monotonicity and convergence evidence, directly hitting "harness updates ≠ harness gains."
Recursive Self-Improvement · Issue 14
Self-improvement starts being tracked: costs, grounding, and verification
The main theme of this issue is that "self-improvement starts being tracked": cost, grounding, and verification three lines simultaneously push the closed loop …
LongTails: Automated Research in OptimizationShould read. It explicitly defines "improvement" as achieving a lower oracle-complexity bound under a fixed formal Setup, using Lean 4's Comparator to independently audit theorems and complexity bounds—agents cannot pass checks by adding assumptions, omitting oracle calls, or leaving proof gaps; it has achieved 100+ new results. Compared to existing formal verification work (CvxLean, AutoOPT), the increment lies in a unified Setup–Complexity abstraction that separates problem classes from reachable oracle budgets, scales across deterministic/random/composite/higher-order/zeroth-order settings, and reframes research as budget minimization under formal correctness constraints. Limitation: it doesn't disclose invalid run detection and failure rates, but as a reproducible, verifiable theoretical optimization discovery closed loop, it directly hits the 'self-improvement rate' measurement and component decomposition lines.- The RSI Tax: When Recursive Self-Improvement Is Not Worth the CostShould read. It explicitly makes the token cost of the self-improvement process a measurement object, decomposing it into verification/exploration/writing categories and tracking the cost share associated with subsequent usage states; verification accounts for 74.8% of Meta-Harness, 78.1% of EvoSkill, and 93.6% of RRSI's RSI Tax, and more than half of the verification cost corresponds to states never used by subsequent tasks. Compared to the unified budget protocol in Issue 7's Rethinking the Evaluation of Harness Evolution, the increment lies in making "self-improvement cost" itself an independent measurement object and providing a cost-performance trade-off perspective; its simple baseline SRN saves 65.6–71.0% of total tokens while matching or surpassing complex RSI methods' accuracy, serving as a strong negative result on "whether complex self-improvement is worth it." Limitation: only two models, single run, and cost attribution is descriptive rather than causal intervention.
- When Does Exploration Prevent Collapse? Three Regimes and the Path of the Reward in Self-Consistency TrainingShould read. It provides a three-region closed-form analysis of self-consistency training (TTRL) collapse, proving that when the exploration term is propagated throughout the reward path, learning rate and optimizer scaling do not move the stability boundary, while bypassing one step (e.g., adding a bonus after GRPO normalization) shifts the threshold by 2–3 times, and derives precise thresholds for majority rewards and rare-answer bonuses. Compared to previous empirical studies on collapse, the increment lies in making "the position of the exploration term in the reward path" a provable source of stability boundaries, directly addressing the direction's concerns on reward grounding and self-play collapse. It reports honest failure data such as F95e collapse rate and pass@1 trade-offs, and distinguishes what exploration can do (it cannot correct erroneous majority answers). Limitation: theory targets single-problem/single-state, but the framework can be directly transferred to any closed-loop evaluation that relies on self-consistency rewards.
Looped Transformers & Latent Reasoning · Issue 6
Loop Count Is Not a Compute Dial: A Contract View of Depth Reusability
The most central signal this issue is that "whether loop count is a reliable axis for scaling compute" is further tightened. Issue 5, There Is No Free Loop, alr…
Agreement rather than normalisation keeps depth reusable in looped language modelsFor the first time, on released weights, by precisely rearranging loop-boundary normalization (without changing the readout path, r=1 identity check), it proves that what breaks depth reusability is not state norm growth but the mismatch between loop topology and the readout head; and from-scratch training shows that training without boundary normalization extrapolates better beyond training depth, and readout refitting recovers only about one-third of the loss; full recovery requires retraining together with the last block layer. Relative to the negative results in Issue 5, There Is No Free Loop, and the recipe in Issue 4, Closing the Loop, this paper shifts focus from training recipe to the contract of normalization placement and readout calibration, and provides a methodological correction for comparing looped vs. stacked depth under equal overshoot (K/r0).- What Limits Recursive Reasoning Models: Optimization, Architecture and Test-Time ScalingThe first to isolate architectural and optimization factors of HRM/TRM/URM in a unified pipeline, systematically revealing that optimization (gradient paths, physical batching, state stabilization) matters more than explicit hierarchical structure, and giving a large improvement on a 13.6M model on arithmetic OOD (71.16% vs 36.2%). Relative to the truncation scaling study in Issue 3, Truncate or Not, the increment is simultaneously comparing gradient path placement and physical batching vs. gradient accumulation, and emphasizing state stabilization recipes. Limitations: very small model scale, no strict comparison with equal-compute non-loop models.
- Learning to Extrapolate in Depth with Looped TransformersFor the first time, provides a theory of the finite extrapolation window for looped transformers trained at fixed depth: training depth K converges to an effective parameter that trades off propagation and residual error; within the certified window, too few loops under-propagate, too many create spurious connections, and the certified depth gain grows exponentially with K−H. Relative to the mechanistic study in Issue 4, Beyond the Training Horizon, and the PAR training objective in Issue 3, this turns "help-then-hurt" into a provable window boundary with rigorous training dynamics. Limitations: restricted to linear attention, no softmax, no residual, graph-connectivity toy tasks.
Code Agent Trajectory Synthesis · Issue 5
Verifier Quality Becomes the Training Target: From Acceptance Gates to Predictable, Intervenable Mechanisms
The clearest signal this issue: the quality of verifiers and rewards themselves is shifting from an 'acceptance gate at evaluation time' to a 'research object d…
VerifierBench: Benchmarking the Generation of Executable Verifiers for LLM AgentsFirst systematic evaluation of the agent-generated executable verifier itself, rather than solver or test generation. Core finding: generated verifiers are far more reliable at rejecting invalid solutions than accepting valid ones (across 19 models, TNR generally above 80%, TPR generally below 70%), and most false rejections concentrate on all-reject verifiers—contributing 87.9%–96.0% of false rejections per model in archival records, a bias previously unquantified. Compared to SWT-Bench and TestGenEval which only test test/assertion generation, it extends verification from a single benchmark to three task types (tool calls, states, code) and proposes V4V six-item screening and a valid variants + attacks construction protocol. Provides empirical evidence for reward signal reliability in synthetic training pipelines; V4V screening and trace-level attribution are transferable to verifier quality control in SWE-smith/R2E-Gym-like environments; limitation: training gains not tested.- Verifier-Grounded Agentic RL for Provably Correct CodeAdvances verifier rewards from binary verdicts to dense, provably correct signals: uses verifier diagnostics (obligation ratio) rather than verdicts for scoring, and adds an integrity audit layer above the verifier that rejects any candidate rewriting specifications or assuming the conclusion. Compared to Re:Form/VeriGate which only reward verdicts, and test rewards lacking reliability guarantees, it validates on held-out benchmarks, including transfer to unseen verifiers/languages, controlled comparisons with binary outcome rewards and SFT, and frozen-expert ablations—attribution evidence fits this direction's taste. Limitation: focuses on formal verification rather than typical SWE-bench-style test tasks.
- Honesty Is a Race: Predicting When Verifiable-Reward RL Teaches a Model to BluffProvides the first testable, first-principles condition (p̃·r/b > 1+κ) predicting when verifiable-reward RL teaches models to bluff, derived from GRPO's group-mean advantage and gradient coupling, and introduces a 'race' mechanism and 'generous-then-cut' schedule to avoid collapse. Compared to prior empirical observations of reward hacking or abstention collapse, it offers a predictive threshold and causal control (lottery) to isolate the checker's role, and the 'race' mechanism explains why runs slightly below threshold may win while lottery cannot. Limitation: experiments on small models and synthetic/code tasks, not validated on full SWE-bench.