Weekly Gallery
Latest edition
AI for Formal Math · Issue 2
Issue 2: From "Can Prove" to "Trustworthy" — The Governance Layer and Bottleneck Quantification of AI Formal Mathematics
The most important signal this issue: the formal mathematics community is shifting from "can prove" to "trustworthy." Terence Tao's announced Palomar registry e…
LEAP: Supercharging LLMs for Formal Mathematics with Agentic FrameworksLEAP's increment lies in combining AND-OR DAG hierarchical memory with interleaved informal-formal planning, enabling a general LLM without specialized fine-tuning to achieve 100% solve rate on Putnam 2025, and on Lean-IMO-Bench improving a general model from <10% to 70%, surpassing the gold-medal-level specialized system Aristotle's 48%. The DAG structure supports lemma reuse and anticipatory lemma planning, mitigating the exponential complexity of Hilbert-style tree search; ablations clearly isolate the contribution of DAG memorization, and code and data are public, making it a must-read for agentic proof search architectures.- FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language ModelsFormalTCS is the first end-to-end benchmark targeting frontier TCS research (STOC/FOCS/SODA/COLT 2025-2026), decomposing the research pipeline into four stages and diagnosing bottlenecks at each stage. The key increment is the first quantification that "automatic formalization (NC2FT max 11.5) is a sharper bottleneck than theorem proving (FT2FP max 28.6)", and finding that "research taste" is another major obstacle to end-to-end autonomous research (only 6 of 64 generated claims passed expert evaluation); 175 expert-verified instances and open-source code make it a complementary benchmark close to real research scenarios.
- OProver: A Unified Framework for Agentic Formal Theorem ProvingOProver unifies retrieval, compiler feedback, and iterative repair into a single learnable policy, trained end-to-end via CPT+SFT+RL, with a co-evolution loop that feeds back proven proofs and repair trajectories into the corpus. The core increment is train–inference matching: the same state representation is used across rollout, SFT, and RL, making feedback-conditioned refinement a learned policy rather than a test-time heuristic; the OProofs corpus (with trajectory-level supervision including failed attempts, feedback, and repairs) and ablations are reproducible, achieving 93.3% Pass@32 on MiniF2F.
Pretraining Data · Issue 2
Issue 2: The Interval Where Repetition Has Negative Effects - New Criteria for Data-Constrained Mixing
The most noteworthy clue this week advances "repetition under data constraints" from "diminishing returns" to "the existence of a negative-effect interval." One…
Prescriptive Scaling Laws for Data Constrained TrainingProposes an additive overfitting penalty, modeling the benefits of repetition and the superlinear cost separately, and for the first time characterizes the interval where "repetition beyond a data-dependent threshold is harmful and compute should be redirected to model capacity" - a direct increment over Issue #1's "Bridging Compute- and Data-Optimal Pretraining" and Muennighoff et al.'s "diminishing returns" formulation. Its reanalysis shows that the popular advice of "smaller models, more epochs" stems from a mis-specification of the Chinchilla baseline, and provides cross-configuration prescriptions validated under both perplexity and downstream OLMES; the case where strong weight decay reduces the overfitting coefficient by about 70% explicitly links regularization strength to repetition tolerance. The limitation is that evidence stops at 1B and uses validation loss, but it is sufficient to change decisions on scale and budget allocation under data constraints.- Repetition Mismatch: Why Data Mixture Experiments Don’t Scale and How to Fix ThemIdentifies "repetition mismatch" as an independent confounder in small-scale mixing extrapolation: high-quality datasets are small, and their repetition rate drifts as the training budget grows, causing proxy experiments to predict the wrong optimal mixing ratio. Relative to InfoLaw and Internal Data Repetition in Issue #1, which treat repetition as a modeling term, this work's increment is to treat the repetition rate as a controllable variable; a subsampling method that preserves the repetition rate can reduce the mixing prediction error of a 757M model from 0.75 to 0.05 under a 1/16 token budget. The method is orthogonal to existing scaling laws, can be absorbed into any mixing pipeline, and is a low-cost, highly operable correction; the limitation is scale ≤757M and validation loss as the criterion.
- Explaining Data Mixing Scaling LawsProvides the first theoretical derivation of data mixing scaling laws, extending quantized models and linear regression models to multi-domain settings, explaining why mixing laws hold through two mechanisms - "capacity competition" and "noise suppression" - and pointing out that the optimal mixing ratio deviates from target weights due to data-dependent noise terms. Relative to empirical laws like Additive Law/RegMix, its increment is a functional form with fewer parameters that can extrapolate across scales using only small-scale proxies, and the code is public. The limitation is validation at 200M–1B and base loss as the criterion, but the theoretical contribution is sufficient to become a new benchmark for mixing research.
MoE & Sparse Experts · Issue 2
Issue 2: Route Replay Moves to the System Level, Expert Specialization Gains Positive Structural Evidence
This issue features two main threads: route replay upgrades from an algorithmic stability measure to a system-level load-balancing oracle, and evidence for expe…
ReLibra: Routing-Replay-Guided Load Balancing for MoE Training in Reinforcement LearningMust-read. Extends route replay from the algorithmic layer (last issue #1's PR² predictive replay) to the system layer: leveraging the property that routes are known before training in RL rollout-training, performing expert reordering across batches and expert replication within batches, matching hierarchical network bandwidth, and absorbing hot expert fluctuations at the microbatch granularity. Compared to PR²'s focus on training-inference consistency, ReLibra uses replay information for system scheduling, reporting full route statistics and dense baselines, with throughput improvements up to 1.6× over Megatron-LM and 1.2× over oracle-load EPLB—a significant increment in the route replay direction.- Beyond Geometric Complementarity: Coherent Overlap in Sparse Mixture-of-Experts RoutingMust-read. Uses ESSI and a prefix-controlled 2×2 factorial design to separate candidate quality, context opportunity, and their interaction, consistently finding the interaction to be negative across 39 factorial units—actual prefixes narrow rather than amplify the geometric advantage of selected experts. This is a positive structural complement to last issue #1's causal audit (From Observation to Intervention) and modular causal tests: "coherent overlap" shows geometric overlap coexists with functional value, providing key nuance for pruning and route design.
- Diagnosing Training Inference Mismatch in LLM Reinforcement Learning (VeXact)Isolates training-inference mismatch from the route decision layer, building the zero-mismatch rollout engine VeXact as a diagnostic baseline, proving that token-level numerical mismatch alone can independently cause RL training collapse, and revealing via zero-centered loss contribution analysis that it disrupts training through sign-imbalanced gradient distortion. Compared to last issue #1's PR² focusing on route staleness, this work addresses lower-level numerical implementation differences and serves as a calibration benchmark for evaluating all route replay/compensation algorithms.
Efficient Sequence Modeling · Issue 2
Issue 2: Theorizing Block-Sparse Selectors and Knowledge Transfer in Hybrid Architectures
This issue's efficient sequence modeling research elevates the 'selector quality' from an engineering problem to a provable theoretical one. COBS uses cumulant …
COBS: Cumulant Order Block Sparse AttentionFirst to use cumulant expansion to prove that first-order block selectors (NSA MLP, Quest) have a curvature blind spot due to discarding within-block covariance, proposing to estimate attention mass using compressed second-order statistics per block (low-rank covariance + subspace projection + FP4), improving NSA baseline from 0.2999 to 0.8195 on 32k RULER, approaching dense 0.9040, with only 1.21× KV read traffic. Relative to [#1] MiniMax Sparse Attention's per-group block-level top-k, its increment is elevating the selector from first-order to second-order cumulants and providing a cacheable compression scheme; NoPE ablation and rank scans are also high-quality scientific records.- Priming: Hybrid State Space Models From Pre-trained TransformersTurns hybrid architecture design from a pretraining problem into a knowledge transfer problem—initializing a pretrained Transformer into a hybrid SSM using layer selection, weight initialization, and short alignment, with less than 0.5% of the source model's pretraining budget, thus enabling the first controlled comparison of GKA/GDN/Mamba-2 under the same conditions, and proving that compressed decaying memory is more useful than a 4× larger sliding window. It provides compute-matched comparisons at 8B/32B and degradation curves on HELMET/MRCR/BABILong, with GKA also offering a new design axis of solver iterations adjustable at serving time.
- Does RoPE Prevent or Degrade Retrieval Heads? A Mechanistic Analysis Across Model FamiliesUsing paired seed protocols, layer clustering permutation tests, and causal head masking, it mechanistically tests whether RoPE base frequency prevents or weakens retrieval head formation: the prevention hypothesis is rejected, utility-retrieval associations are family-specific and opposite in direction, and the causal localization is to the RoPE frequency axis (low-frequency dimensions) rather than the norm utility axis. Relative to [#1] Rethinking the Role of Efficient Attention's 'lazy large window', it advances the optimization prior problem of efficient attention to the frequency axis of positional encoding, and provides NIAH dose-response curves rather than just needle-in-a-haystack scores.
Scaling Laws & Training Methods · Issue 2
Issue 2: Optimizers Become a First-Class Axis of Scaling Laws, Batch Scaling Law Gets a Closed-Form Solution
This week's leads elevate the "optimizer" from a training detail to a first-class axis of scaling laws. Hyperball replaces the implicit norm control of weight d…
Fantastic Pretraining Optimizers and Where to Find Them II: Hyperball OptimizationReplaces the implicit norm control of weight decay with explicit Frobenius norm constraints, turning the directional step size into an explicit design quantity. Across multiple scales from 130M to 1.2B, it reduces learning rate transfer drift from 2–4x to about 1.4x and boosts Muon's token-equivalent speedup to 20–30%. Instead of adjusting parameterization, it constrains the optimization trajectory, complementing muP/MSSP; worth a close read.- Towards Joint Scaling Laws with Optimal Batch Size SchedulesFor the first time, derives a closed-form solution for the optimal batch size schedule under any learning rate schedule from convex optimization theory, and proves it is decoupled from the peak learning rate and independent of model size/architecture/optimizer, forming a joint scaling law. It improves efficiency by 6–15% under fixed compute while maintaining universal dynamics, directly addressing the open problem of batch scaling laws.
- Practical Scaling Laws: Converting Compute into Performance in a Data-Constrained WorldAdds an independent training duration axis T and an explicit overfitting term c·N^γ/D^δ to Chinchilla, wrapped with a saturating baseline, achieving SOTA extrapolation residuals across four domains and five public LLM grids. Compared to last issue's Skaling coupled form, it adds the T axis and overfitting term, providing a more complete functional form for data-limited/single-epoch scenarios.
Coding Agents · Issue 2
Issue 2: Harness becomes the object of RL training, skeptical evidence and cost dimensions tighten simultaneously
The most notable shift this issue is that harness has transformed from a 'hidden variable being evaluated' to a 'first-class object of RL training'. Two infrast…
The Scaffold Effect in Coding Agents: Harness Choice as a Hidden Variable in Coding-Agent EvaluationA cross-harness controlled comparison with fixed base model, quantifying up to 40x token cost differences per solved task while pass rates differ only 0–8pp, and identifying harness-specific failure fingerprints reproducible across models (Goose's REASON, OpenCode's TIME/HANG). Compared to Issue 1's longitudinal version evolution study, this work independently replicates the core conclusion 'harness choice ≠ benefit' via cross-harness horizontal experiments, and incorporates cost dimensions and no-action turns supervision burden into the evaluation framework. Includes full configurations, raw trajectories, and aggregated snapshots, serving as another hard piece of evidence for harness engineering empiricism.- Agent Lightning v1.0: Towards Harnessed Agentic RLFirst systematic characterization of 'harnessed agentic RL'—where at deployment the harness owns the environment loop and the trainer only sees LLM request-response pairs—identifying key challenges such as retokenization, sample merging, advantage computation, and loss normalization that were previously left blank by proxy frameworks like verl Uni-Agent and AReaL 2.0, and proposing rollout-level advantage and loss normalization. With only 6K samples, it improves Qwen3.5-9B on SWE-bench Verified from 41.8% to 56.4%, and releases the full data cleaning and anti-reward-hacking pipeline. Note that gains are reported only on a single saturated benchmark without held-out controls; read with benchmark validity skepticism.
- LEGO-RL: Harness-Native Reinforcement Learning for Coding AgentsExplicitly formalizes 'faithful optimization' in harness-native RL: uses in-process proxy to capture exact tokens and MoE routing decisions (R3 replay), resolving rollout-training inconsistency caused by harness-side history rewriting, and pairs with sandbox reward integrity defenses and termination-aware trajectory filtering. Provides misaligned negative controls for MoE routing replay, maintaining rollout-training correlation above 0.99. Limitations: single model, single run, and only SWE-bench Verified without held-out, but as infrastructure its engineering contributions and ablations are solid.
Recursive Self-Improvement · Issue 2
Issue 2: Turning 'Whether Improvements Are Real' into Auditable Measurement
The main thread of this issue is turning "self-improvement rate as a measurement target" from a slogan into an audit discipline. Last issue we saw the implement…
Phantom Gains: Auditing Self-Improvement Against a Measured NullProposes "transfer-level audit": every statistic must be paired with a separately measured null, and enumerates seven measurement failure modes (F1–F7), each of which can reverse a reported conclusion in the absence of a control. The key increment is the observation that "checkpoint 0 is an independent evaluation of the untrained model," making the null nearly free, and replacing natural-threshold fixes with per-question exact tests (whose null is 0.058 rather than zero). Compared to last issue's [One Run Is Not an Idea] and [Beyond Final Scores], this advances from "implementation variance" to "systematic enumeration of measurement artifacts," and provides a separation between external distillation and self-training on rare problems. Read it when designing controls for any self-improvement closed loop.- AI4AI-Bench: Benchmarking LLM Agents in Algorithmic Design for Recursive Self-ImprovementThe first benchmark to isolate the "algorithm design layer" from the system/data layer: 10 frozen research repositories, 4 hours of exploration + 12 hours of clean reruns, with a fixed evaluator hidden from the agent. The core finding is a patch classification of execution-side vs. learning-side: 53.6% of submissions only modify the run side, submissions touching the learning side average 0.226 vs. 0.126, and inference effort mainly buys the willingness to "dare to modify the learning layer" (8%→64%). Compared to last issue's [One Run Is Not an Idea] separation of idea/implementation variance, this turns "modifying execution vs. modifying algorithms" into an inspectable measurement target, and explicitly reports the cause classification of 124/290 below-baseline and 19 zero-score runs.
- Rollout Cards: A Reproducibility Standard for Agent ResearchProposes treating "rollout records" rather than "reported scores" as the reproducible unit of agent research: rollout cards retain the full trajectory, declared views, reporting rules, and discard lists. A systematic audit of 50 repositories shows that no one reports failure counts, and documents 37 cases where reporting-rule differences can change scores by up to 20.9 percentage points or reverse model rankings. For self-improvement closed loops, it provides the evidence carrier for determining whether an improvement is real—if the reporting rules themselves can be audited, the determination of "invalid runs" becomes reproducible.