Pith. sign in

REVIEW 45 references

VeRecycle: Reclaiming Guarantees from Probabilistic Certificates for Stochastic Dynamical Systems after Change

T0 review · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read VeRecycle shows the maximum reusable safety probability after a localized change is min(original threshold, 1 minus 1 divided by the certificate's infimum on the changed region).

arxiv 2505.14001 v1 pith:OSJTE54G submitted 2025-05-20 cs.AI cs.SYeess.SY

Sterre Lutz , Matthijs T.J. Spaan , Anna Lukina This is my paper · ORCID
classification cs.AIcs.SYeess.SY
keywords probabilisticcertificatessystemsverecycledynamicalguaranteesneuralstochastic
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Probabilistic neural Lyapunov certificates are functions that assign each state a number. The number is high in unsafe states and low in target states; if the function drops in expectation along the controlled process, a reach-avoid probability can be certified. VeRecycle asks: if dynamics change only in a known set of states X?, can the old certificate still certify anything? The key observation is that the changed states are a wildcard, so they cannot be relied on for expected decrease. If an alternative dynamics makes every changed state absorbing, the certificate cannot drop there. Therefore, to survive arbitrary changes, every changed non-target state must already have certificate value at least 1/(1 minus rho prime). This condition translates to a simple formula: the largest reusable threshold rho prime equals min(rho, 1 minus 1 divided by inf{C(X?)}), where the infimum is taken over changed non-target states. VeRecycle computes this infimum approximately with interval bound propagation, producing a guaranteed lower bound on the reusable threshold. In compositional control, each edge certificate gets a recycled threshold, edge weights become minus log(threshold), and a shortest path chooses the best surviving route. The paper's experimental tables show recycled thresholds comparable to re-verification at a fraction of runtime. The catch is in the phrase 'non-target states': the theorem as written takes the infimum over all of X?, and its proof applies condition 3 to states that Definition 2 exempts when they lie in the target set. A target-only change causes the formula to report no threshold even though the guarantee is unaffected. The formula is plausible after that correction; the current statement is not.
Extended reading notes

Core claim

The maximum reclaimable probability threshold e_rho for any dynamics change confined to a known set X? is min(rho, 1 - 1/inf{C(X?)}), and no threshold exists when inf{C(X?)} < 1 (Theorem 1). If this is true, VeRecycle formally salvages probabilistic guarantees without retraining or re-verification when the changed states have high certificate values.

Load-bearing premise

Theorem 1 assumes that every state in X? whose certificate value is below 1/(1-rho) is still constrained by the decrease condition (Definition 2, condition 3). Target states are exempt from that condition, and the paper never excludes them from X?. The proof of Lemmas 2 and 3 selects x in X? with C(x)=inf{C(X?)} and applies condition 3 to it, which fails when the infimum is attained only at target states. In that case the theorem is false: changing dynamics only at a target state cannot lower the reach-avoid probability, yet the formula reports no threshold. The fix is to take the infimum over X? \ X*; as stated, this assumption is load-bearing.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Assumptions & free parameters 0 free parameters · 6 assumptions · 0 invented entities

The central formula has no fitted parameters; it is a function of the given certificate's infimum. It does rely on the certificate definition, regularity assumptions, IBP soundness, and an unflagged disjointness assumption that breaks the theorem as stated.

assumptions (6)
  • domain assumption Reach-avoid certificate soundness: a function satisfying Definition 2 conditions certifies the reach-avoid specification.
    Definition 2 is taken from [Zikelic et al., 2023a]; VeRecycle inherits its soundness from this definition.
  • standard math Regularity assumptions: X, U, W are Borel-measurable; f and pi are Lipschitz; X and W are closed and bounded.
    Section 2 states these as standard control-theory assumptions; they justify probability spaces and IBP/Lipschitz cell verification.
  • ad hoc to paper All low-certificate states inside X? are subject to certificate condition 3, i.e., they are not in the target set X*.
    Theorem 1 and Lemmas 2-3 apply the decrease condition to x in X? with C(x)=inf C(X?). Definition 2 only requires condition 3 on X\X*, so target states are exempt. The paper never states this disjointness assumption; without it the theorem is false when X? contains target states.
  • domain assumption IBP gives valid lower and upper bounds I- and I+ on inf C(X?).
    Theorem 2 and Section 4.2 use IBP; the soundness of the approximation relies on IBP's soundness, which is not proved in this paper.
  • domain assumption Absorbing dynamics f(x,u,w)=x for x in X? is an admissible realization of the changed system.
    Used in Lemmas 2-3 to upper-bound e_rho. It follows from Definition 3 because such f satisfies Equation (2), provided the state remains in X.
  • domain assumption Compositional reach-avoid threshold equals the product of edge thresholds along a path.
    Taken from [Zikelic et al., 2023b]; Algorithm 1 multiplies edge thresholds, so the global guarantee relies on that prior compositional result.

how reviews work

0 comments
Cite this review

Pith. "Pith review of VeRecycle: Reclaiming Guarantees from Probabilistic Certificates for Stochastic Dynamical Systems after Change." pith.science (2026). https://pith.science/paper/OSJTE54G

@misc{pith2026250514001,
  author       = {Pith},
  title        = {Pith review of: VeRecycle: Reclaiming Guarantees from Probabilistic Certificates for Stochastic Dynamical Systems after Change},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/OSJTE54G}},
  note         = {Machine review of arXiv:2505.14001}
}
read the original abstract

Autonomous systems operating in the real world encounter a range of uncertainties. Probabilistic neural Lyapunov certification is a powerful approach to proving safety of nonlinear stochastic dynamical systems. When faced with changes beyond the modeled uncertainties, e.g., unidentified obstacles, probabilistic certificates must be transferred to the new system dynamics. However, even when the changes are localized in a known part of the state space, state-of-the-art requires complete re-certification, which is particularly costly for neural certificates. We introduce VeRecycle, the first framework to formally reclaim guarantees for discrete-time stochastic dynamical systems. VeRecycle efficiently reuses probabilistic certificates when the system dynamics deviate only in a given subset of states. We present a general theoretical justification and algorithmic implementation. Our experimental evaluation shows scenarios where VeRecycle both saves significant computational effort and achieves competitive probabilistic guarantees in compositional neural control.

Figures

Figures reproduced from arXiv: 2505.14001 by the authors.

Figure 1
Figure 1. A probabilistic certificate (color gradient) for a navigation [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. A compositional policy (blue) for a decomposed reach [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Example of a “loose” original certificate (gradient left) [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

45 extracted references · 39 canonical work pages

  1. [1]

    Formal synthesis of Lyapunov neural networks

    [Abate et al., 2021] Alessandro Abate, Daniele Ahmed, Mirco Giacobbe, and Andrea Peruffo. Formal synthesis of Lyapunov neural networks. IEEE Control. Syst. Lett. , 5(3):773–778,

    work page 2021

  2. [6]

    [Blumenthal and Getoor, 1968] R. M. C. Blumenthal and R. K. Getoor. Markov Processes and Potential Theory . Pure and applied mathematics: A series of monographs and textbooks. Academic Press,

    work page 1968

  3. [9]

    Data- driven Interval MDP for Robust Control Synthesis

    [Coppola et al., 2024] Rudi Coppola, Andrea Peruffo, Licio Romao, Alessandro Abate, and Manuel Mazo Jr. Data- driven Interval MDP for Robust Control Synthesis. arXiv preprint arXiv:2404.08344,

    arXiv 2024

  4. [10]

    Safe control with learned certificates: A survey of neural Lyapunov, barrier, and contraction meth- ods for robotics and control

    [Dawson et al., 2023] Charles Dawson, Sicun Gao, and Chuchu Fan. Safe control with learned certificates: A survey of neural Lyapunov, barrier, and contraction meth- ods for robotics and control. IEEE Trans. Robotics , 39(3):1749–1767,

    work page 2023

  5. [11]

    DelftBlue Supercomputer (Phase 2)

    [Delft High Performance Computing Centre (DHPC), 2024] Delft High Performance Computing Centre (DHPC). DelftBlue Supercomputer (Phase 2). https://www.tudelft.nl/dhpc/ark:/44463/DelftBluePhase2,

    work page 2024

  6. [12]

    Controller synthesis from deep reinforcement learn- ing policies

    [Delgrange et al., 2024] Florent Delgrange, Guy Avni, Anna Lukina, Christian Schilling, Ann Nowe, and Guillermo Pérez. Controller synthesis from deep reinforcement learn- ing policies. In EWRL, pages 1–34,

    work page 2024

  7. [13]

    A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis

    [Edwards et al., 2023] Alec Edwards, Andrea Peruffo, and Alessandro Abate. A general verification framework for dynamical and control models via certificate synthesis. CoRR, abs/2309.06090,

    work page Pith review arXiv 2023

  8. [14]

    [Gehr et al., 2018] Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin T. Vechev. AI2: safety and robustness certification of neural networks with abstract interpretation. In IEEE Symposium on Security and Privacy, pages 3–18,

    work page 2018

Show all 45 references
  1. [16]

    On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models

    [Gowal et al., 2019] Sven Gowal, Krishnamurthy Dvi- jotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Relja Arandjelovic, Timothy Mann, and Pushmeet Kohli. On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models. arXiv preprin...

    2019 arXiv

  2. [17]

    Swart, and Daniel A

    [Hagberg et al., 2008] Aric Hagberg, Pieter J. Swart, and Daniel A. Schult. Exploring network structure, dynam- ics, and function using NetworkX. Technical report, Los Alamos National Laboratory (LANL), Los Alamos, NM (United States),

    2008

  3. [18]

    Compositional Learning and Verification of Neural Network Controllers

    [Ivanov et al., 2021] Radoslav Ivanov, Kishor Jothimurugan, Steve Hsu, Shaan Vaidya, Rajeev Alur, and Osbert Bas- tani. Compositional Learning and Verification of Neural Network Controllers. ACM Transactions on Embedded Computing Systems, 20(5s):92:1–92:26,

    2021

  4. [19]

    Safe Learning for Uncertainty-Aware Planning via Interval MDP Abstraction

    [Jiang et al., 2022] Jesse Jiang, Ye Zhao, and Samuel Coogan. Safe Learning for Uncertainty-Aware Planning via Interval MDP Abstraction. IEEE Control Systems Let- ters, pages 2641–2646,

    2022

  5. [20]

    Compositional Reinforcement Learning from Logical Specifications

    [Jothimurugan et al., 2021] Kishor Jothimurugan, Suguman Bansal, Osbert Bastani, and Rajeev Alur. Compositional Reinforcement Learning from Logical Specifications. In NeurIPS, pages 10026–10039,

    2021

  6. [21]

    Control system analysis and design via the sec- ond method of Lyapunov: (i) continuous-time systems (ii) discrete time systems

    [Kalman and Bertram, 1959] Rudolf E Kalman and John E Bertram. Control system analysis and design via the sec- ond method of Lyapunov: (i) continuous-time systems (ii) discrete time systems. IRE Transactions on Automatic Control, 4(3):112,

    1959

  7. [25]

    Towards scalable complete verification of ReLU neural networks via dependency-based branch- ing

    [Kouvaros and Lomuscio, 2021] Panagiotis Kouvaros and Alessio Lomuscio. Towards scalable complete verification of ReLU neural networks via dependency-based branch- ing. In IJCAI, pages 2643–2650,

    2021

  8. [26]

    When to Trust AI: Advances and Challenges for Certification of Neural Networks

    [Kwiatkowska and Zhang, 2023] Marta Kwiatkowska and Xiyue Zhang. When to Trust AI: Advances and Challenges for Certification of Neural Networks. In FedCSIS, pages 25–37,

    2023

  9. [27]

    Calvert, and Luca Laurenti

    [Mathiesen et al., 2023] Frederik Baymler Mathiesen, Simeon C. Calvert, and Luca Laurenti. Safety certification for stochastic systems via neural barrier functions. IEEE Control. Syst. Lett., 7:973–978,

    2023

  10. [28]

    Differentiable Abstract Interpretation for Provably Robust Neural Networks

    [Mirman et al., 2018] Matthew Mirman, Timon Gehr, and Martin Vechev. Differentiable Abstract Interpretation for Provably Robust Neural Networks. In ICML, pages 3578– 3586,

    2018

  11. [29]

    Ver- ifiable Reinforcement Learning Systems via Composition- ality

    [Neary et al., 2023] Cyrus Neary, Aryaman Singh Samyal, Christos Verginis, Murat Cubuktepe, and Ufuk Topcu. Ver- ifiable Reinforcement Learning Systems via Composition- ality. arXiv preprint arXiv:2309.06420,

    2023 arXiv

  12. [30]

    Neural continuous-time su- permartingale certificates

    [Neustroev et al., 2025] Grigory Neustroev, Mirco Gia- cobbe, and Anna Lukina. Neural continuous-time su- permartingale certificates. In AAAI, pages 27538–27546,

    2025

  13. [34]

    Multiple-Environment Markov Decision Pro- cesses

    [Raskin and Sankur, 2014] Jean-François Raskin and Ocan Sankur. Multiple-Environment Markov Decision Pro- cesses. arXiv preprint arXiv:1405.4733,

    2014 arXiv

  14. [35]

    Richards, Felix Berkenkamp, and Andreas Krause

    [Richards et al., 2018] Spencer M. Richards, Felix Berkenkamp, and Andreas Krause. The Lyapunov neural network: Adaptive stability certification for safe learning of dynamical systems. In CoRL, pages 466–476,

    2018

  15. [36]

    Learning stable deep dynamics models for partially observed or delayed dynamical systems

    [Schlaginhaufen et al., 2021] Andreas Schlaginhaufen, Philippe Wenk, Andreas Krause, and Florian Dorfler. Learning stable deep dynamics models for partially observed or delayed dynamical systems. In NeurIPS, pages 11870–11882,

    2021

  16. [37]

    Prox- imal Policy Optimization Algorithms

    [Schulman et al., 2017] John Schulman, Filip Wolski, Pra- fulla Dhariwal, Alec Radford, and Oleg Klimov. Prox- imal Policy Optimization Algorithms. arXiv preprint arXiv:1707.06347,

    2017 arXiv

  17. [38]

    Sutton, Doina Precup, and Satinder Singh

    [Sutton et al., 1999] Richard S. Sutton, Doina Precup, and Satinder Singh. Between MDPs and semi-MDPs: A framework for temporal abstraction in reinforcement learning. Artificial Intelligence, 112(1-2):181–211,

    1999

  18. [40]

    Packard, and Peter J

    [Topcu et al., 2008] Ufuk Topcu, Andrew K. Packard, and Peter J. Seiler. Local stability analysis using simu- lations and sum-of-squares programming. Automatica, 44(10):2669–2675,

    2008

  19. [43]

    Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, Pei Huang, Ori Lahav, Min Wu, Min Zhang, Ekate- rina Komendantskaya, Guy Katz, and Clark W

    [Wu et al., 2024] Haoze Wu, Omri Isac, Aleksandar Zeljic, Teruhiro Tagomori, Matthew L. Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, Pei Huang, Ori Lahav, Min Wu, Min Zhang, Ekate- rina Komendantskaya, Guy Katz, and Clark W. Barrett. Marabou 2.0: A v...

    2024

  20. [44]

    Efficient neu- ral network robustness certification with general activation functions

    [Zhang et al., 2018] Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neu- ral network robustness certification with general activation functions. In NeurIPS, pages 4944–4953,

    2018

  21. [45]

    Compositional neural certifi- cates for networked dynamical systems

    [Zhang et al., 2023] Songyuan Zhang, Yumeng Xiu, Guan- nan Qu, and Chuchu Fan. Compositional neural certifi- cates for networked dynamical systems. In L4DC, pages 272–285, 2023

    2023

  22. [1959]

    Barrett, David L

    [Katz et al., 2017] Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural net- works. In CAV (1), pages 97–117,

    2017

  23. [1968]

    Neural Lyapunov control

    [Chang et al., 2019] Ya-Chien Chang, Nima Roohi, and Si- cun Gao. Neural Lyapunov control. In NeurIPS, pages 3240–3249,

    2019

  24. [1999]

    Learning dynamics models with stable invariant sets

    [Takeishi and Kawahara, 2021] Naoya Takeishi and Yoshi- nobu Kawahara. Learning dynamics models with stable invariant sets. In AAAI, pages 9782–9790,

    2021

  25. [2002]

    [Prajna et al., 2004] Stephen Prajna, Ali Jadbabaie, and George J. Pappas. Stochastic safety verification using bar- rier certificates. In CDC, pages 929–934,

    2004

  26. [2004]

    Puterman

    [Puterman, 2014] Martin L. Puterman. Markov decision pro- cesses: discrete stochastic dynamic programming . John Wiley & Sons,

    2014

  27. [2008]

    Robust control of uncertain Markov decision processes with temporal logic specifications

    [Wolff et al., 2012] Eric M Wolff, Ufuk Topcu, and Richard M Murray. Robust control of uncertain Markov decision processes with temporal logic specifications. In CDC, pages 3372–3379,

    2012

  28. [2012]

    Neural Lyapunov con- trol for discrete-time systems

    [Wu et al., 2023] Junlin Wu, Andrew Clark, Yiannis Kan- taros, and Yevgeniy V orobeychik. Neural Lyapunov con- trol for discrete-time systems. In NeurIPS, pages 2939– 2955,

    2023

  29. [2014]

    Zico Kolter and Gaurav Manek

    [Kolter and Manek, 2019] J. Zico Kolter and Gaurav Manek. Learning stable deep dynamics models. In NeurIPS, pages 11126–11134,

    2019

  30. [2017]

    [Kingma, 2014] Diederik P. Kingma. Adam: A method for stochastic optimization. arXiv preprint arXiv:1412.6980,

    2014 arXiv

  31. [2018]

    Neural termination analysis

    [Giacobbe et al., 2022] Mirco Giacobbe, Daniel Kroening, and Julian Parsert. Neural termination analysis. In ESEC/SIGSOFT FSE, pages 633–645,

    2022

  32. [2019]

    Henzinger, Mathias Lechner, and Dorde Žikeli ´c

    [Chatterjee et al., 2023] Krishnendu Chatterjee, Thomas A. Henzinger, Mathias Lechner, and Dorde Žikeli ´c. A learner-verifier framework for neural network controllers and certificates of stochastic systems. In TACAS (1), pages 3–25,

    2023

  33. [2021]

    Stochastic omega-regular verification and control with supermartingales

    [Abate et al., 2024] Alessandro Abate, Mirco Giacobbe, and Diptarko Roy. Stochastic omega-regular verification and control with supermartingales. InCAV (3), pages 395–419,

    2024

  34. [2022]

    Learning-Based Verification of Stochastic Dynamical Systems with Neural Network Policies

    [Badings et al., 2024] Thom Badings, Wietze Koops, Sebas- tian Junges, and Nils Jansen. Learning-Based Verification of Stochastic Dynamical Systems with Neural Network Policies. arXiv preprint arXiv:2406.00826,

    2024 arXiv

  35. [2023]

    Scenario-based verification of uncertain para- metric MDPs

    [Badings et al., 2022] Thom Badings, Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, and Ufuk Topcu. Scenario-based verification of uncertain para- metric MDPs. International Journal on Software Tools for Technology Transfer, 24(5):803–819,

    2022

  36. [2024]

    Henzinger, Mathias Lechner, and Dorde Žikeli ´c

    [Ansaripour et al., 2023] Matin Ansaripour, Krishnendu Chatterjee, Thomas A. Henzinger, Mathias Lechner, and Dorde Žikeli ´c. Learning provably stabilizing neural controllers for discrete-time stochastic systems. In ATVA (1), pages 357–379,

    2023

  37. [2025]

    On the con- struction of Lyapunov functions using the sum of squares decomposition

    [Papachristodoulou and Prajna, 2002] Antonis Pa- pachristodoulou and Stephen Prajna. On the con- struction of Lyapunov functions using the sum of squares decomposition. In CDC, pages 3482–3487,

    2002

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.