We revisit exploration collapse in reinforcement learning with verifiable rewards (RLVR), from the perspective of the candidate distribution for next-token prediction. We formally show that as probability concentrates on the top-1 candidate, the expected number of distinct responses collapses to one regardless of the sampling budget K. This theoretical implication is further verified by our empirical tracking of top-N candidate probabilities during training, where the top-1 candidate progressively dominates while plausible alternatives are suppressed. These findings suggest a key desideratum for effective exploration: preserving non-negligible probability mass on the top-N candidates. To this end, we propose Candidate-aware Support Preservation (CaSP), with two complementary designs. Specifically, CaSP redistributes positive gradients among top-N candidates for correct responses, and applies a stronger penalty to the top-1 candidate for incorrect responses. Unlike many exploration-oriented methods that improve pass@K at the cost of pass@1, CaSP improves pass@K across the full K spectrum. These gains generalize to 6 math, 2 logical-reasoning, and 2 coding benchmarks, and scales to 32B-parameter models and sampling budgets up to K=1024, positioning it as a principled, candidate-level approach for RLVR exploration.

We introduce FormalMATH, a large-scale Lean4 benchmark for formal mathematical reasoning, comprising 5,560 semantically validated Lean4 statements spanning competition-level and undergraduate mathematics. To improve reliability, FormalMATH is constructed through a human-in-the-loop pipeline that combines type checking, LLM-based semantic verification against the informal–formal statements alignment, negation-based disproving, and expert review. We conduct a systematic evaluation of frontier theorem provers under test-time scaling on FormalMATH. Results show that current provers remain far from solving the benchmark: the strongest model, DeepSeek-Prover-V2 (671B), achieves only 28.31% Pass@32. We further observe substantial domain imbalance across provers, with stronger performance in applied mathematics and algebra but weaker results in discrete mathematics. We identify common failure modes in current provers, including incomplete proofs, weak handling of inequalities, misuse of automation tactics, and redundant hypothesis introduction. Extreme test-time scaling (e.g., Pass@3200) yields only modest gains on a subset of FormalMATH, suggesting that current training paradigms do not equip provers to effectively exploit additional sampling budget. We also observe a counterintuitive negative effect when provers are given human-written natural-language solution references: such references can measurably degrade formal proof generation rather than aid it. Overall, FormalMATH provides a challenging and reliable testbed for measuring progress in formal mathematical reasoning.

Parameter-efficient finetuning (PEFT) has become the standard approach for adapting large language models, yet evaluations largely emphasize downstream accuracy while overlooking the retention of pretrained capabilities. We argue that PEFT should be assessed through the stability-plasticity dilemma: the trade-off between target-task adaptation and resistance to forgetting. We introduce PEFT-Arena, a benchmark that jointly measures downstream performance and general capability retention. Across the studied settings, methods exhibit distinct stability-plasticity profiles, and orthogonal finetuning often lies on a favorable frontier under comparable parameter budgets. We analyze the internal changes associated with these external trade-offs from two complementary geometric perspectives. In weight space, spectral profiles characterize how parameterizations interact with the pretrained singular-value structure. In activation space, representation-similarity diagnostics show a strong association between forgetting and non-isometric distortion on general-evaluation data. Together, these views suggest that preserving pretrained spectral and representational geometry is an important inductive bias for retention, with OFT’s spectrum-preserving updates providing a particularly clear case. Finally, parameterization-aware interpolation shows that final SFT checkpoints can lie beyond a better target-retention operating point. We use post-hoc rewinding as a case study of controlling this trade-off.

Large language models (LLMs) have shown strong abilities in writing and revising programs, yet many program-synthesis benchmarks still evaluate programs in symbolic or digital environments. We introduce compositional machine design, a physically grounded form of program synthesis where machines are written as programs that compose standardized parts, and success is determined by simulated physical behavior. To study this problem, we present BesiegeField, a testbed built on the machine-building game Besiege. In BesiegeField, LLM agents generate machine programs from textual functional demands, execute the resulting machines in simulation, and receive rewards and state feedback. We benchmark LLM agents across representative machine-design tasks under single-agent generation, iterative editing, and hierarchical workflows. Strong models recover task-relevant structures and sometimes achieve nontrivial physical performance, but often struggle with spatially precise assembly, mechanism-level planning, and translating feedback into useful structural edits. We further finetune Qwen2.5-14B, an open-source LLM, with reinforcement learning from simulation-derived rewards. We find that, under a fixed generation budget, RL improves the best machine discovered. We additionally evaluate human performance to provide a reference point for task difficulty. These results establish compositional machine design as a testbed for studying LLM agents that synthesize executable machine programs and improve them through physical feedback.

Orthogonal finetuning (OFT) offers highly parameter-efficient adaptation while preventing catastrophic forgetting, but its high runtime and memory demands limit practical deployment. We identify the core computational bottleneck in OFT as its weight-centric implementation, which relies on costly matrix-matrix multiplications with cubic complexity. To overcome this, we propose OFTv2, an input-centric reformulation that instead uses matrix-vector multiplications (i.e., matrix-free computation), reducing the computational cost to quadratic. We further introduce the Cayley–Neumann parameterization, an efficient orthogonal parameterization that approximates the matrix inversion in the Cayley transform via a truncated Neumann series. These modifications allow OFTv2 to achieve up to 10x faster training and 3x lower GPU memory usage without compromising performance. In addition, we extend OFTv2 to support finetuning quantized foundation models and show that it outperforms the popular QLoRA in training stability, efficiency, and memory usage.

Adapting large language models (LLMs) to specific tasks remains challenging due to the extensive retraining required, prompting the need for efficient adapter techniques. Despite this, the concurrent serving of multiple adapters, each with unique matrix shapes, poses significant system-level challenges. To address these issues, we identify an opportunity in structurally sparse adapters, which, unlike low-rank adapters, maintain consistent matrix shapes while varying in sparsity patterns. Leveraging this characteristic, we introduce SpartanServe, a system designed for efficient concurrent serving of LLMs using multiple structurally sparse adapters. SpartanServe employs a unified matrix multiplication operation and a novel memory management technique to enable effective batching. Furthermore, the incorporation of Triton kernels enhances the acceleration of matrix multiplication in the serving process. Experimental results demonstrate that SpartanServe achieves 2.12× speedup over S-LoRA when serving 96 adapters using a single NVIDIA A100 GPU (40GB), showcasing its efficacy in concurrent LLM serving.