Value Functions as Supermartingale Certificates

• URL: http://arxiv.org/abs/2605.31524v1
• Date: Fri, 29 May 2026 16:39:02 GMT
• Title: Value Functions as Supermartingale Certificates
• Abstract summary: We show that under an appropriate reward, the value function associated to a policy that almost surely satisfies an $$-regular property encodes a Streett supermartingale certificate for that specification.<n>Our results, validated experimentally on finite Markov decision processes, hold for finite, countably infinite, and continuous state spaces, suggesting a principled route to certificate synthesis via RL.
• Score: 48.922124609307566
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Certification methods for stochastic systems provide sufficient proof rules, based on real-valued supermartingale certificates, to determine the almost-sure satisfaction of $ω$-regular properties (and therefore of linear temporal logic) over general state spaces, encompassing both countably infinite and continuous state spaces. Conversely, reinforcement learning (RL) methods for $ω$-regular tasks have received considerable attention, but they typically lack formal guarantees that the learned policy satisfies the specification, except possibly for finite state and action spaces. We bridge these two lines of research by establishing a novel theoretical connection: under an appropriate reward, the value function associated to a policy that almost surely satisfies an $ω$-regular property encodes a Streett supermartingale certificate for that specification. Our results, validated experimentally on finite Markov decision processes, hold for finite, countably infinite, and continuous state spaces, suggesting a principled route to certificate synthesis via RL.

Related papers

• On the Formal Limits of Alignment Verification [0.24049560288708582]
  A foundational question for AI safety is whether alignment can be formally certified.<n>We prove that no verification procedure can simultaneously satisfy three properties: soundness (no misaligned system is certified), generality (verification runs in time), and tractability.<n>The result follows from three independent barriers: the computational complexity of full-domain neural network verification, the non-identifiability of internal goal structure from behavioral observation, and the limits of finite evidence for properties defined over infinite domains.
  arXiv  Detail & Related papers  (2026-03-08T23:03:21Z)
• P2S: Probabilistic Process Supervision for General-Domain Reasoning Question Answering [51.04492568024515]
  We introduce Probabilistic Process Supervision (P2S), a novel framework for fine-grained process rewards.<n>P2S provides fine-grained process rewards without requiring a separate reward model or human-annotated reasoning steps.
  arXiv  Detail & Related papers  (2026-01-28T14:35:20Z)
• Stopping Rules for Stochastic Gradient Descent via Anytime-Valid Confidence Sequences [51.56484100374058]
  We study stopping rules for gradient descent (SGD) for convex optimization.<n>We develop an anytime-valid, data-dependent upper confidence sequence for the weighted average suboptimality of projected SGD.<n>These are the first rigorous, time-uniform performance guarantees and finitetime $varepsilon$-optimality certificates.
  arXiv  Detail & Related papers  (2025-12-15T09:26:45Z)
• Phase Transition for Stochastic Block Model with more than $\sqrt{n}$ Communities (II) [51.320599504997745]
  We show that when the number $K$ of communities remains smaller than $sqrtn$, non-trivial community recovery is possible in time above the Kesten--Stigum threshold.<n>We also show that, in moderately sparse settings, the optimal algorithms appear to be fundamentally different from spectral methods.
  arXiv  Detail & Related papers  (2025-11-26T15:54:17Z)
• Provably Sample-Efficient Robust Reinforcement Learning with Average Reward [4.530028899565083]
  We propose a new algorithm designed for robust Markov Decision Processes (MDPs) with transition uncertainty characterized by $ell_p$-norm and contamination models.<n>Our algorithm operates without requiring any prior knowledge of the robust MDP.<n>Our work provides essential theoretical understanding of sample efficiency of robust average reward RL.
  arXiv  Detail & Related papers  (2025-05-18T15:34:45Z)
• DeepLTL: Learning to Efficiently Satisfy Complex LTL Specifications for Multi-Task RL [59.01527054553122]
  Linear temporal logic (LTL) has recently been adopted as a powerful formalism for specifying complex, temporally extended tasks.<n>Existing approaches suffer from several shortcomings.<n>We propose a novel learning approach to address these concerns.
  arXiv  Detail & Related papers  (2024-10-06T21:30:38Z)
• Reward Certification for Policy Smoothed Reinforcement Learning [14.804252729195513]
  Reinforcement Learning (RL) has achieved remarkable success in safety-critical areas. Recent studies have introduced "smoothed policies" in order to enhance its robustness. It is still challenging to establish a provable guarantee to certify the bound of its total reward.
  arXiv  Detail & Related papers  (2023-12-11T15:07:58Z)
• Learning Control Policies for Stochastic Systems with Reach-avoid Guarantees [20.045860624444494]
  We study the problem of learning controllers for discrete-time non-linear dynamical systems with formal reach-avoid guarantees. We learn a certificate in the form of a reach-avoid supermartingale (RASM), a novel notion that we introduce in this work. Our approach solves several important problems -- it can be used to learn a control policy from scratch, to verify a reach-avoid specification for a fixed control policy, or to fine-tune a pre-trained policy.
  arXiv  Detail & Related papers  (2022-10-11T10:02:49Z)
• Distillation of RL Policies with Formal Guarantees via Variational Abstraction of Markov Decision Processes (Technical Report) [0.0]
  We consider the challenge of policy simplification and verification in the context of policies learned through reinforcement learning (RL) We derive new bisimulation bounds between the unknown environment and a learned discrete latent model of it. We show how one can use a policy obtained via state-of-the-art RL to efficiently train a variational autoencoder that yields a discrete latent model with provably approximately correct bisimulation guarantees.
  arXiv  Detail & Related papers  (2021-12-17T17:57:32Z)
• Offline Reinforcement Learning: Fundamental Barriers for Value Function Approximation [74.3002974673248]
  We consider the offline reinforcement learning problem, where the aim is to learn a decision making policy from logged data. offline RL is becoming increasingly relevant in practice, because online data collection is well suited to safety-critical domains. Our results show that sample-efficient offline reinforcement learning requires either restrictive coverage conditions or representation conditions that go beyond complexity learning.
  arXiv  Detail & Related papers  (2021-11-21T23:22:37Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.