Establishing almost sure convergence rates for stochastic approximation and reinforcement learning under Markovian noise is a fundamental theoretical challenge. We make progress towards this challenge for a class of stochastic approximation algorithms whose expected updates are contractive, a setting that arises in many reinforcement learning algorithms such as $Q$-learning and linear temporal difference learning. Specifically, for a power-law learning rate $O(n^{-η})$ with $η\in (1/2, 1)$, we obtain an almost sure convergence rate arbitrarily close to $o(n^{1 - 2η})$. For the harmonic learning rate $α_n=α/(n+1)$, the almost sure squared-error rate is $o(n^{-ζ})$ for every $ζ<\min\{1,2(1-κ)α\}$, where $κ$ is the contraction factor. Thus exponents arbitrarily close to one are available when $2(1-κ)α\geq1$. This approaches the $n^{-1}$ polynomial exponent of classical law-of-the-iterated-logarithm benchmarks. Key to our analysis is a novel Lyapunov drift construction that applies a Poisson-equation based correction for Markovian noise to the well-established Moreau-envelope smoothing for the contractive mapping.
The ecosystem of Lean and Mathlib has become the de facto standard for large language model (LLM) assisted formal reasoning with remarkable successes in recent years. Those successes, however, only consume Mathlib as an essential dependency but do not directly contribute to it. In the meantime, the growth of Mathlib has recently been bottlenecked by the review process, which requires human reviewers to judge whether proposed pull requests (PRs) follow the Mathlib's conventions and are worth integrating as part of a shared mathematical infrastructure. This leads to our central question: can LLMs help review Mathlib PRs? To this end, we introduce MathlibPR, a benchmark built from real Mathlib4 PR histories. We further propose a staged evaluation protocol and use it to evaluate both LLM models (e.g., DeepSeek, Qwen, Goedel, and Kimina) and LLM agents (e.g., Codex and Claude Code). Surprisingly, both LLM models and LLM agents struggle to distinguish merge-ready PRs from build-passing PRs that were revised or never merged. By turning Mathlib PR histories into a supervised signal, MathlibPR provides a step toward reviewer assistants and reward models that could help evaluate PRs and steer LLMs toward producing merge-ready Mathlib contributions.
Learning rate is a critical component of reinforcement learning (RL). This work uses global and local clocks to distinguish two types of learning rates. The former is of the standard form $α_t$ that depends only on the time step $t$ (i.e., a global clock). The latter is of the form $α_{ν(S_t, t)}$, where $ν(s, t)$ counts the number of visits to state $s$ until time $t$ (i.e., a local clock). In discounted RL, an RL algorithm that is convergent with a local clock is always also convergent with a global clock, and vice versa. We are not aware of any counterexample. The key contribution of this work is to show that this nice correspondence breaks down in average-reward RL. Specifically, we construct a counterexample showing that although differential temporal difference (TD) learning is convergent with a local clock, it can diverge with a global clock. We empirically observe this divergence in our experiments and also prove that the associated ODE of differential TD with a global clock is unstable. This counterexample closes the open problem in Wan et al. [2021], Blaser et al. [2026].
Surface electromyographic (sEMG) signals provide information about muscle activity and function during movement. Fatigue alters multiple properties of these signals, with patterns that vary across individuals and contraction intensities. However, physiological insights into fatigue remain underused in sEMG modeling, particularly for cross-subject recognition. We introduce FatigueFormer to recognize fatigue states defined by ratings of perceived exertion (RPE). The model incorporates physiologically motivated trend grouping into sEMG encoding by organizing descriptors into increasing- and decreasing-trend streams and combining inter-window context with within-window feature interactions. To assess fatigue-state discriminability across contraction intensities, we further present an sEMG fatigue dataset collected from 30 participants at four levels of maximum voluntary contraction (MVC) and benchmark representative machine learning and deep learning methods. We evaluate performance offline under leave-one-subject-out (LOSO) and within-subject protocols and use the SWIFTIES dataset for external validation. Results support FatigueFormer's effectiveness across the examined contraction intensities and both datasets, while indicating that fatigue-related cues vary across MVC levels. An exploratory adaptation analysis shows higher FatigueFormer scores with more labeled target-user data on complete target recordings, which include calibration samples.
Temporal-difference (TD) learning trains neural representations using bootstrapped targets generated by evolving value estimates, yet how predictive features emerge and propagate under incomplete neural updates remains poorly understood. We investigate this problem using finite-width two-layer ReLU critics on a constructed family of smooth stochastic horizon-$H$ MDPs with unknown quadratic structure and $d$-dimensional observations. We first show that an informative TD update acquires the quadratic Bellman signal and yields a representation admitting a bounded predictive readout. The simultaneous hidden-weight and head update achieves a strict finite-sample prediction-risk improvement over matched head-only SGD, with a $2(d+1)$-fold larger population quadratic response. We then establish that an imperfect learned continuation can already provide informative supervision to an earlier zero-reward stage. By tracking coupled neural updates with one SGD step per target copy, without requiring intermediate Bellman regressions to be solved, we obtain a uniform prediction-error transient $\exp[-Ω(K/(Hd))]$, up to action-independent shifts and explicit sampling and finite-width errors. On the constructed signed-action MDP family whose total reward is bounded by 1, we show that an exploration-then-commit algorithm can achieve $\widetilde{O}(d^3H^{1/3}T^{2/3})$ regret over $T$ episodes, using $K=\widetilde{O}(Hd)$ global updates. Our analysis connects bootstrapped feature acquisition, concurrent neural refinement, and finite-budget policy performance.
Large language models (LLMs) have shown increasing promise in research-level problem solving, yet a comprehensive collection of such problems is still missing, and evaluating them on research-level problems remains challenging. We introduce OpenFrontiers, a cross-disciplinary resource that combines a structured corpus of open research problems with a retrospective benchmark of recently resolved problems in mathematics. The corpus records problem statements, context, progress, and other information for 12,151 problems. The benchmark contains 200 problems, 110 resolved in 2026 and 90 still open, each with a Lean~4 statement checked by automated probes and two independent reviews; a subset HQ-50 further filters based on quality score, etc. Our evaluation protocol grades formal proofs with two independent checkers in an isolated sandbox under closed-book, frozen-retrieval, and live-web conditions. Evaluating seven LLM agents on the HQ-50 subset under a standardized budget, we find that closed-book rediscovery is rare, at most 7 of 40 resolved problems, whereas live-web success mostly reflects retrieval of published solutions. By linking a broad research-problem corpus to a formally graded evaluation subset with documented solutions, OpenFrontiers provides a foundation for measuring research-level rediscovery and studying progress toward solving currently open scientific problems. The dataset and benchmark could be found in https://huggingface.co/collections/FlippyDora/openfrontiers.