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.