Pith. sign in

REVIEW 3 major objections 5 minor 175 references

This survey claims that the fragmented field of post-training reinforcement-learning verification can be organized along three axes — paradigm, temporal scope, and guarantee strength — with practical tool-selection guidance following from t

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

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

T0 review · deepseek-v4-flash

2026-08-02 13:58 UTC pith:HKO7VBAL

load-bearing objection A useful organizing survey of RL verification that needs fixes: a wrong formal definition and a self-sourced, unreproducible benchmark undermine the parts that claim rigor. the 3 major comments →

arxiv 2607.16210 v1 pith:HKO7VBAL submitted 2026-05-14 cs.AI

A Survey on the Verification of Reinforcement Learning Policies

Luca Marzari , Ezio Bartocci , Enrico Marchesini This is my paper
classification cs.AI
keywords reinforcement learning verificationneural network verificationformal verificationprobabilistic verificationreachability analysistaxonomysafety guaranteespreimage analysis
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

The paper is a survey that tries to establish a unified view of methods that verify, after training, that a neural-network reinforcement-learning policy behaves safely. It claims that a rapidly growing but fragmented literature can be organized along three axes: formal versus probabilistic verification, step-wise versus multi-step temporal scope, and the strength of the guarantees offered. It also formalizes the underlying verification problems with a common notation, makes implicit assumptions explicit (such as whether an input-region guarantee really captures closed-loop safety), and connects the taxonomy to practical guidance for choosing a verification tool. A sympathetic reader would care because RL policies are increasingly proposed for safety-critical deployment, and without a shared vocabulary it is hard to tell whether one tool's guarantee is stronger or weaker than another's.

Core claim

The survey's central claim is that every post-training approach to verifying neural-network RL policies fits into a single descriptive framework. Step-wise verification analyzes a single policy decision under an input perturbation set and, the authors note, can be encoded with existing neural-network verifiers; multi-step verification embeds the policy in the environment and reasons over closed-loop trajectories, using temporal logic, control-barrier or Lyapunov certificates, or probabilistic reachability; enumeration-based verification computes the set of states that lead to unsafe actions. The authors further claim that these approaches occupy different points on a scalability-versus-guara

What carries the argument

The load-bearing object is the taxonomy summarized in Table 1, which classifies a dozen-plus verification tools along four columns: verification paradigm (formal or probabilistic), temporal scope (step-wise or multi-step), guarantee strength (sound, complete, probabilistic), and an 'RL readiness' column indicating whether a tool can be applied to trained policies without substantial reformulation. The survey grounds this taxonomy in six formal problem definitions — SAT-based verification, reachability-based verification, LTL-based multi-step verification, all-DNN (preimage enumeration) verification, and RNN-based verification for single and cooperative multi-agent policies — that pin down wh

Load-bearing premise

The framework's value rests on the assumption that the methods collected in Table 1 fairly and completely represent the post-training RL verification literature, and that the benchmark evidence in Table 2 — drawn from the authors' own tools without an independent protocol — is representative; if key methods are missing or the benchmark ranking is unrepresentative, the taxonomy's comparisons and tool-selection guidance could mislead.

What would settle it

Run an independent, protocol-public benchmark that applies the surveyed tools (for example α,β-CROWN, ModelVerification.jl, PREMAP, ε-ProVe, RF-ProVe, and an exact SMT solver) to the same RL benchmarks (ACAS Xu, CartPole, Dubin's rejoin, LunarLander) with published hyperparameters and timeouts. If the observed coverage-versus-runtime ranking among enumeration-based and relaxation-based tools diverges from Table 2's ordering, the survey's tool-selection guidance would need revision. A more direct conceptual falsifier would be a published RL verification method that cannot be placed on the three

Watch this falsifier. Get emailed when new claim-graph text bears on it.

Share X Bluesky LinkedIn Reddit HN

If this is right

  • If the taxonomy is correct, new verification methods can be classified quickly by locating them on the three axes, giving the community a shared vocabulary for comparing guarantees.
  • Tool selection becomes a matter of matching temporal scope and guarantee strength to the deployment question: reachability-based over-approximation for local robustness, SAT-based solvers for falsification and debugging, relaxation-based and probabilistic methods for large-scale repeated verification, enumeration-based tools for region-level risk analysis, and multi-step or neuro-symbolic methods
  • For the surveyed benchmarks, bound-propagation methods scale better than exact solvers as the number of verification instances grows, suggesting that scalable RL verification will lean on tight linear relaxations and branching heuristics rather than exact enumeration.
  • Because step-wise robustness and step-wise safety coincide under a local perturbation set, mature neural-network verification tools can be applied to RL policies without modeling the environment, lowering the barrier to entry.
  • Enumeration-based methods, despite the highest computational cost, produce region-level information — the set of unsafe states — that supports retraining, shielding, and residual-risk estimation, capabilities a binary verdict does not provide.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If region-level preimage analysis continues to scale, verification could shift from a one-time pass/fail check to an iterative debugging loop, where unsafe regions feed targeted retraining, data collection, and runtime shielding.
  • The taxonomy's treatment of history-dependent policies suggests a natural next step: combining verification with learned feasibility oracles for hidden states, so that guarantees cover only realizable interaction histories rather than all abstract ones.
  • The same three axes could extend to adversarial or mixed cooperative-competitive MARL by adding a dimension for opponent modeling, though the survey leaves that formalization open.
  • For modern architectures such as Transformers, the survey's observation that attention and softmax break piecewise-linear assumptions points toward probabilistic or sampling-based verification as a more natural fit than exact enumeration.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 5 minor

Summary. This survey proposes a unifying taxonomy for post-training verification of reinforcement learning (RL) policies, organizing methods along three axes: verification paradigm (formal vs. probabilistic), temporal scope (step-wise vs. multi-step), and guarantee strength, with an additional 'RL readiness' rating. It formalizes step-wise, multi-step, LTL-based, enumeration-based, recurrent-policy, and multi-agent verification problems in a common notation, presents a benchmark comparison of verification tools on ACAS Xu and OpenAI Gym tasks, and discusses open challenges such as recurrent policies, multi-agent systems, and long-horizon reasoning. The central claim is that the taxonomy, together with the benchmark results, provides both a shared vocabulary for the field and practical guidance for tool selection.

Significance. If the taxonomy and the empirical comparison are sound, this would be a valuable reference for researchers and practitioners in RL verification. The paper makes a genuine effort to expose implicit assumptions, to relate apparently disparate methods, and to identify important open problems; the discussion of recurrent policies and multi-agent verification is particularly useful. The survey's strengths are conceptual rather than computational: it does not ship code or machine-checked proofs, but it does offer a structured map of the field. However, the practical tool-selection guidance rests on an empirical benchmark that is not reproducible from the submitted text, and one of the central formal definitions is incorrect. Both issues are fixable, but they currently prevent the survey from being a reliable guide.

major comments (3)
  1. [§3.1, Definition 2] The definition states 'violate ⇔ R(X)⊆Y' for reachability-based verification. If R(X) is an over-approximation of the exact output set, containment in Y is sufficient but not necessary for violation: a single input x∈X with f(x)∈Y already violates the property, even if R(X) also contains safe outputs. If R(X) is meant to be exact, the correct violation condition is R(X)∩Y≠∅, not R(X)⊆Y. As written, the definition is not equivalent to Definition 1 and misrepresents the guarantees that over-approximate reachability tools actually provide. Please restate the implication direction and clarify whether the condition is soundness, completeness, or both.
  2. [§4, Table 2 and Fig. 5] The empirical comparison is the load-bearing support for the tool-selection guidance in Section 4, but it is not reproducible from the manuscript. Table 2 attributes all results to 'Marzari et al.' without a year or a specific reference; the row 'Exact VCAS' is not mapped to any named method or citation; and no hardware, timeout, error-bar definition, or external baseline is provided. Since the authors are also the developers of the probabilistic enumeration tools being compared, the relative ranking cannot be independently corroborated from the submitted text. Please provide a full evaluation protocol, a precise citation for the underlying benchmark, details for the exact baseline, and either an external comparison or an explicit statement that these are self-reported preliminary results. Without this, the practical guidance, e.g., that probabilistic enumeration 'substantially improves
  3. [Table 1 and §3.3] The 'RL readiness' axis is a central part of the taxonomy, but the criteria for assigning 'Yes,' 'Partial,' or 'No' are not defined, and several entries appear to reflect the authors' judgment without justification. Relatedly, the row 'Prob. Enum [Marzari et al.]' and Figure 4's 'Adapted from [Marzari et al.]' lack a year and a specific reference, making it impossible for the reader to identify the method being taxonomized. Please define the readiness scale operationally and complete all incomplete citations.
minor comments (5)
  1. [§3.1, Example 1] The example defines the postcondition Y as max(y1,y2)>y0, which is the condition that the forward action is NOT selected; under Definition 1, Y should be the unsafe set, i.e., y0 > max(y1,y2) or 'y0 is selected.' As written, the example contradicts the formal definition.
  2. [§5, Definitions 5 and 6] The notation H and H∗ is not made precise. H is described as 'a set of histories' while H∗ is 'feasible hidden states'; the relationship between them and how they are encoded in the input tuple should be formalized.
  3. [Table 1, footnote] The footnote 'Not for all the methods' makes it unclear which of the 'Sound & Complete*' entries do not satisfy both properties. Please annotate each affected row individually.
  4. [Fig. 5] The axis labels should be clarified: the y-axis is 'cumulative computation time' but the x-axis is described as 'number of verified properties (instances)'; it would help to specify whether the curves are cumulative over instances sorted by difficulty or by time.
  5. [References] Several citations are incomplete: 'Marzari et al.' appears in Table 1, Table 2, and Figure 4 without a year or reference key. Please resolve these to specific bibliography entries.

Circularity Check

1 steps flagged

Core taxonomy is externally grounded, but the §4 tool-selection guidance rests on a self-sourced, protocol-free benchmark attributed only to the authors.

specific steps
  1. self citation load bearing [Section 4, Table 2 and surrounding analysis]
    "Table 2: Enumeration-based (preimage) evaluation from Marzari et al. … These results suggest that scalability, architectural coverage, and tooling maturity are tightly coupled dimensions rather than independent factors."

    The scalability ranking of enumeration methods — including the central practical claim that probabilistic approaches such as ε-ProVe and RF-ProVe 'substantially improve scalability' — is drawn entirely from a table attributed to 'Marzari et al.', i.e., the same research group. No benchmark protocol, hardware specification, timeout, error-bar definition, or external baseline is given, and the 'Exact VCAS' row is not mapped to a citable method. The evidence and the conclusion are therefore from the same self-citation chain, making the §4 guidance self-supported rather than independently derived. This does not make the taxonomy circular, but it makes the benchmark-based selection advice load-bearing on the authors' own unpublished results.

full rationale

The survey's central taxonomy (§3, Definitions 1–6) is constructed from external and independently citable works (e.g., VNN-COMP, Marabou, nnenum, PREMAP, Kotha et al., Everett et al.), so the unifying organization does not reduce to the authors' own definitions or predictions. The main circularity burden is localized to §4 and Table 2: the empirical comparison that supports the scaling and tool-selection guidance is self-sourced ('from Marzari et al.') with no protocol or external baseline, and the 'Exact VCAS' row lacks a concrete reference. This is a self-citation load-bearing step for the practical recommendations, but it is not a constructional equivalence: no equation is defined in terms of a target result, and no fitted parameter is renamed as a prediction. The 'RL-ready' ratings for the authors' own rows are also self-assessments, but they do not drive the formal taxonomy. Overall, the central taxonomic contribution retains independent content, while the benchmark-backed guidance carries a real self-support problem that warrants a moderate score rather than a high one.

Axiom & Free-Parameter Ledger

0 free parameters · 4 axioms · 0 invented entities

No free parameters or invented entities; the survey introduces only a taxonomy and definitions, and Table 2 reuses numerical results from prior/self-cited work rather than fitting new constants.

axioms (4)
  • domain assumption The surveyed method set (Table 1) is representative of the entire post-training RL verification literature.
    §3 'A Unified Taxonomy' and Table 1: if the selection is unrepresentative, the 'unifying perspective' claim overstates coverage.
  • domain assumption For step-wise RL verification, local robustness and safety can be treated as equivalent when X is a perturbation region and Y is an action-ranking predicate, enabling VNN-LIB encoding.
    §3.1: 'robustness and safety may coincide'; the unified encoding depends on this equivalence holding in the surveyed settings.
  • standard math Verification of ReLU networks is NP-hard (SAT) and #P-hard (enumeration), which the survey uses to explain scalability trade-offs.
    §3.1 cites Katz et al. 2017; §3.3 cites Marzari et al. 2023. Accepted complexity results from prior literature.
  • ad hoc to paper The benchmark results in Table 2 are a faithful reproduction of the cited 'Marzari et al.' evaluation.
    §4/Table 2: no protocol or independent implementation is given; the survey's tool-selection conclusions depend on trusting this unreferenced source.

pith-pipeline@v1.3.0-alltime-deepseek · 12458 in / 10562 out tokens · 88680 ms · 2026-08-02T13:58:57.236572+00:00 · methodology

0 comments
Cite this review

Pith. "Pith review of A Survey on the Verification of Reinforcement Learning Policies." pith.science (2026). https://pith.science/paper/HKO7VBAL

@misc{pith2026260716210,
  author       = {Pith},
  title        = {Pith review of: A Survey on the Verification of Reinforcement Learning Policies},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/HKO7VBAL}},
  note         = {Machine review of arXiv:2607.16210}
}
Share X Bluesky LinkedIn Reddit HN
read the original abstract

Reinforcement learning (RL) is increasingly applied in complex, safety-critical domains, yet the lack of rigorous behavioral guarantees for neural network-based policies remains a major barrier to deployment. Recent advances in policy expressiveness and scale have intensified this challenge, leading to a rapidly growing but conceptually fragmented body of work on RL policy verification. This survey provides a unifying perspective on RL verification methods. We introduce a taxonomy that clarifies relationships among existing approaches along three axes: verification paradigm (formal versus probabilistic), temporal scope (step-wise versus multi-step), and guarantees strength. Beyond taxonomy, we unify underlying theoretical foundations, make implicit assumptions and limitations explicit, and identify emerging directions.

Figures

Figures reproduced from arXiv: 2607.16210 by Enrico Marchesini, Ezio Bartocci, Luca Marzari.

Figure 1
Figure 1. Figure 1: Pipeline for post-training verification of RL policies, high [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Explanatory behavioral property. (a) Unsafe situation to [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: BaB refinement. (Adapted from [Marzari et al., 2024].) [PITH_FULL_IMAGE:figures/full_fig_p003_3.png] view at source ↗
Figure 5
Figure 5. Figure 5: Runtime of RL verification tools. (Top) Performance on [PITH_FULL_IMAGE:figures/full_fig_p005_5.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

175 extracted references · 1 canonical work pages

  1. [1]

    Verifying Global Two-Safety Properties in Neural Networks with Confidence , booktitle =

    Anagha Athavale and Ezio Bartocci and Maria Christakis and Matteo Maffei and Dejan Nickovic and Georg Weissenbacher , editor =. Verifying Global Two-Safety Properties in Neural Networks with Confidence , booktitle =. 2024 , doi =

    2024

  2. [2]

    Formal Methods for ML-Enabled Autonomous Systems , year=

    Supporting Standardization of Neural Networks Verification with VNN-LIB and CoCoNet , author=. Formal Methods for ML-Enabled Autonomous Systems , year=

  3. [4]

    International Journal on Software Tools for Technology Transfer , pages=

    First three years of the international verification of neural networks competition (VNN-COMP) , author=. International Journal on Software Tools for Technology Transfer , pages=. 2023 , publisher=

    2023

  4. [5]

    CAV , pages=

    NNV 2.0: the neural network verification tool , author=. CAV , pages=. 2023 , organization=

    2023

  5. [6]

    arXiv preprint arXiv:2205.00263 , year=

    Complete verification via multi-neuron relaxation guided branch-and-bound , author=. arXiv preprint arXiv:2205.00263 , year=

    Pith/arXiv arXiv

  6. [7]

    International Conference on Formal Modeling and Analysis of Timed Systems , pages=

    Reachability analysis of a general class of neural ordinary differential equations , author=. International Conference on Formal Modeling and Analysis of Timed Systems , pages=. 2022 , organization=

    2022

  7. [8]

    Andrey Kofnov and Daniel Kapla and Ezio Bartocci and Efstathia Bura , title =. Proc. of

  8. [9]

    Proceedings of the ACM on Programming Languages , volume=

    This is the moment for probabilistic loops , author=. Proceedings of the ACM on Programming Languages , volume=. 2022 , publisher=

    2022

  9. [10]

    The Probabilistic Termination Tool Amber , booktitle =

    Marcel Moosbrugger and Ezio Bartocci and Joost. The Probabilistic Termination Tool Amber , booktitle =. 2021 , url =

    2021

  10. [11]

    Martin Tappler and Ignacio D. Lopez. Rule-Guided Reinforcement Learning Policy Evaluation and Improvement , booktitle =

  11. [12]

    Lopez-Miguel and Sebastian Adam and Ezio Bartocci and Thomas Eiter and Martin Tappler , title =

    Ignacio D. Lopez-Miguel and Sebastian Adam and Ezio Bartocci and Thomas Eiter and Martin Tappler , title =. Proc. of

  12. [13]

    Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence,

    RobustX: Robust Counterfactual Explanations Made Easy , author =. Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence,. 2025 , month =. doi:10.24963/ijcai.2025/1264 , url =

    work page doi:10.24963/ijcai.2025/1264 2025

  13. [14]

    Yun and Peizhi Niu and Xusheng Luo and Changliu Liu , title =

    Tianhao Wei and Hanjiang Hu and Luca Marzari and Kai S. Yun and Peizhi Niu and Xusheng Luo and Changliu Liu , title =. CAV , pages =. 2025 , doi =

    2025

  14. [15]

    Donti and Changliu Liu and Enrico Marchesini , title =

    Luca Marzari and Priya L. Donti and Changliu Liu and Enrico Marchesini , title =. Proceedings of the 24th International Conference on Autonomous Agents and Multiagent Systems,. 2025 , url =

    2025

  15. [16]

    Christiano and John Schulman and Dan Man

    Dario Amodei and Chris Olah and Jacob Steinhardt and Paul F. Christiano and John Schulman and Dan Man. Concrete Problems in. arXiv preprint arXiv:1606.06565 , year =

    Pith/arXiv arXiv

  16. [17]

    Conference on Artificial Intelligence,

    Luca Marzari and Davide Corsi and Enrico Marchesini and Alessandro Farinelli and Ferdinando Cicalese , title =. Conference on Artificial Intelligence,. 2024 , doi =

    2024

  17. [18]

    Proceedings of the AAAI Conference on Artificial Intelligence , volume=

    On the Probabilistic Learnability of Compact Neural Network Preimage Bounds , author=. Proceedings of the AAAI Conference on Artificial Intelligence , volume=

  18. [19]

    2024 , url =

    Luca Marzari and Francesco Leofante and Ferdinando Cicalese and Alessandro Farinelli , title =. 2024 , url =

    2024

  19. [20]

    Proceedings of the 2023 International Conference on Autonomous Agents and Multiagent Systems,

    Enrico Marchesini and Luca Marzari and Alessandro Farinelli and Christopher Amato , title =. Proceedings of the 2023 International Conference on Autonomous Agents and Multiagent Systems,. 2023 , url =

    2023

  20. [21]

    2023 , url =

    Luca Marzari and Enrico Marchesini and Alessandro Farinelli , title =. 2023 , url =

    2023

  21. [22]

    2025 , booktitle =

    Aydeniz, Ayhan Alp and Marchesini, Enrico and Loftin, Robert and Amato, Christopher and Tumer, Kagan , title =. 2025 , booktitle =

    2025

  22. [23]

    IJCAI , pages =

    Luca Marzari and Davide Corsi and Ferdinando Cicalese and Alessandro Farinelli , title =. IJCAI , pages =. 2023 , doi =

    2023

  23. [24]

    2023 , url =

    Davide Corsi and Luca Marzari and Ameya Pore and Alessandro Farinelli and Alicia Casals and Paolo Fiorini and Diego Dall'Alba , title =. 2023 , url =

    2023

  24. [25]

    Tools and Algorithms for the Construction and Analysis of Systems

    Guy Amir and Davide Corsi and Raz Yerushalmi and Luca Marzari and David Harel and Alessandro Farinelli and Guy Katz , title =. Tools and Algorithms for the Construction and Analysis of Systems. 2023 , doi =

    2023

  25. [26]

    International Conference on Machine Learning , year =

    Exact Upper and Lower Bounds for the Output Distribution of Neural Networks with Random Inputs , author =. International Conference on Machine Learning , year =

  26. [27]

    2022 , url =

    Luca Marzari and Davide Corsi and Enrico Marchesini and Alessandro Farinelli , title =. 2022 , url =

    2022

  27. [28]

    Towards Hierarchical Task Decomposition using Deep Reinforcement Learning for Pick and Place Subtasks , booktitle =

    Luca Marzari and Ameya Pore and Diego Dall'Alba and Gerardo Aragon. Towards Hierarchical Task Decomposition using Deep Reinforcement Learning for Pick and Place Subtasks , booktitle =. 2021 , url =

    2021

  28. [29]

    International Conference on Computer Aided Verification , year=

    The marabou framework for verification and analysis of deep neural networks , author=. International Conference on Computer Aided Verification , year=

  29. [30]

    2021 , isbn =

    Bak, Stanley , title =. 2021 , isbn =. doi:10.1007/978-3-030-76384-8_2 , booktitle =

    doi:10.1007/978-3-030-76384-8_2 2021

  30. [31]

    CAV , pages=

    Marabou 2.0: a versatile formal analyzer of neural networks , author=. CAV , pages=

  31. [32]

    2024 , eprint=

    A DPLL(T) Framework for Verifying Deep Neural Networks , author=. 2024 , eprint=

    2024

  32. [33]

    arXiv preprint arXiv:2410.23903 , year=

    Neural network verification with pyrat , author=. arXiv preprint arXiv:2410.23903 , year=

    Pith/arXiv arXiv

  33. [34]

    International Conference on Formal Modeling and Analysis of Timed Systems , pages=

    Neural network repair with reachability analysis , author=. International Conference on Formal Modeling and Analysis of Timed Systems , pages=. 2022 , organization=

    2022

  34. [35]

    HSCC , year=

    Reachability Analysis of Recurrent Neural Networks Using Star Sets , author=. HSCC , year=

  35. [36]

    FMAS , year=

    Verification of CNN-LSTM Neural Networks Using Exact-Star Reachability , author=. FMAS , year=

  36. [37]

    CCS , year=

    Cert-RNN: Certified Robustness for Recurrent Neural Networks , author=. CCS , year=

  37. [38]

    Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control , pages=

    Verification of recurrent neural networks with star reachability , author=. Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control , pages=

  38. [39]

    CAV , year=

    Prover: Polyhedral Verification of Recurrent Neural Networks , author=. CAV , year=

  39. [40]

    IJCAI , year=

    Verifiable RNN-based policies for POMDPs under temporal logic constraints , author=. IJCAI , year=

  40. [41]

    NeurIPS , year=

    LSTM networks: Stability analysis and probabilistic verification , author=. NeurIPS , year=

  41. [42]

    NFM , year=

    Probabilistic Verification of Deep Reinforcement Learning , author=. NFM , year=

  42. [43]

    arXiv preprint arXiv:2401.XXXX , year=

    Incremental Model Checking for Reinforcement Learning Policies , author=. arXiv preprint arXiv:2401.XXXX , year=

  43. [44]

    ATVA , year=

    COOL-MC: A Model Checker for RL Policies , author=. ATVA , year=

  44. [45]

    ICLR , year=

    Robustness Verification of Transformers , author=. ICLR , year=

  45. [46]

    NeurIPS , year=

    Decision Transformer: Reinforcement Learning via Sequence Modeling , author=. NeurIPS , year=

  46. [47]

    Proceedings of Machine Learning Research vol , volume=

    Safe decision transformer with learning-based constraints , author=. Proceedings of Machine Learning Research vol , volume=

  47. [48]

    2024 , url =

    European Union , title =. 2024 , url =

    2024

  48. [49]

    IEEE Access , volume=

    Reachability analysis of neural feedback loops , author=. IEEE Access , volume=. 2021 , publisher=

    2021

  49. [50]

    Journal of the American statistical association , volume=

    Probability inequalities for sums of bounded random variables , author=. Journal of the American statistical association , volume=. 1963 , publisher=

    1963

  50. [51]

    Neural networks , volume=

    Multilayer feedforward networks are universal approximators , author=. Neural networks , volume=. 1989 , publisher=

    1989

  51. [52]

    Proceedings of the AAAI Conference on Artificial Intelligence , volume=

    Verification of RNN-based neural agent-environment systems , author=. Proceedings of the AAAI Conference on Artificial Intelligence , volume=

  52. [53]

    International Conference on Formal Modeling and Analysis of Timed Systems , pages=

    DiffRNN: differential verification of recurrent neural networks , author=. International Conference on Formal Modeling and Analysis of Timed Systems , pages=. 2021 , organization=

    2021

  53. [54]

    , author=

    Cert-RNN: Towards Certifying the Robustness of Recurrent Neural Networks. , author=. CCS , volume=

  54. [55]

    Journal of Machine Learning Research , volume=

    Monotonic value function factorisation for deep multi-agent reinforcement learning , author=. Journal of Machine Learning Research , volume=

  55. [56]

    Ethics Guidelines for Trustworthy AI , institution =

  56. [57]

    Energy and AI , institution =

  57. [58]

    International Conference on Machine Learning , pages=

    POPQORN: Quantifying robustness of recurrent neural networks , author=. International Conference on Machine Learning , pages=. 2019 , organization=

    2019

  58. [59]

    Journal of artificial intelligence research , volume=

    Reinforcement learning: A survey , author=. Journal of artificial intelligence research , volume=

  59. [60]

    Communications of the ACM , volume=

    A theory of the learnable , author=. Communications of the ACM , volume=. 1984 , publisher=

    1984

  60. [61]

    Journal of the ACM , volume=

    Learnability and the Vapnik-Chervonenkis dimension , author=. Journal of the ACM , volume=. 1989 , publisher=

    1989

  61. [62]

    Nature , volume=

    Human-level control through deep reinforcement learning , author=. Nature , volume=

  62. [63]

    Theoretical Computer Science , volume=

    The complexity of computing the permanent , author=. Theoretical Computer Science , volume=. 1979 , publisher=

    1979

  63. [64]

    International Journal on Software Tools for Technology Transfer , volume=

    Formal methods and automated verification of critical systems , author=. International Journal on Software Tools for Technology Transfer , volume=. 2018 , publisher=

    2018

  64. [65]

    International Symposium on Automated Technology for Verification and Analysis , pages=

    Verifying recurrent neural networks using invariant inference , author=. International Symposium on Automated Technology for Verification and Analysis , pages=. 2020 , organization=

    2020

  65. [66]

    2024 , author =

    Energy Security and Artificial Intelligence , institution =. 2024 , author =

    2024

  66. [67]

    CAV , year=

    Reluplex: An efficient SMT solver for verifying deep neural networks , author=. CAV , year=

  67. [68]

    Counterfactual explanations without opening the black box: Automated decisions and the GDPR , author=. Harv. JL & Tech. , volume=. 2017 , publisher=

    2017

  68. [69]

    Robust Explainable AI , pages=

    Robustness of Counterfactual Explanations , author=. Robust Explainable AI , pages=. 2025 , publisher=

    2025

  69. [70]

    Advances in Neural Information Processing Systems , volume=

    Automatic perturbation analysis for scalable certified robustness and beyond , author=. Advances in Neural Information Processing Systems , volume=

  70. [71]

    NeurIPS , volume=

    Efficient neural network robustness certification with general activation functions , author=. NeurIPS , volume=

  71. [72]

    2021 , url=

    Kaidi Xu and Huan Zhang and Shiqi Wang and Yihan Wang and Suman Jana and Xue Lin and Cho-Jui Hsieh , booktitle=. 2021 , url=

    2021

  72. [73]

    ACM Computing Surveys , volume=

    Redefining counterfactual explanations for reinforcement learning: Overview, challenges and opportunities , author=. ACM Computing Surveys , volume=. 2024 , publisher=

    2024

  73. [74]

    ECAI 2025 , pages=

    Advancing Neural Network Verification through Hierarchical Safety Abstract Interpretation , author=. ECAI 2025 , pages=. 2025 , publisher=

    2025

  74. [75]

    nature , volume=

    Mastering the game of Go with deep neural networks and tree search , author=. nature , volume=. 2016 , publisher=

    2016

  75. [76]

    Marchesini, Enrico and Donnot, Benjamin and Crozier, Constance and Dytham, Ian and Merz, Christian and Schewe, Lars and Westerbeck, Nico and Wu, Cathy and Marot, Antoine and Donti, Priya L , journal=

  76. [77]

    Donti , booktitle=

    Enrico Marchesini and Eva Boguslawski and Alessandro Leite and Christopher Amato and Matthieu DUSSARTRE and Marc Schoenauer and Benjamin Donnot and Priya L. Donti , booktitle=. 2026 , url=

    2026

  77. [78]

    International Journal on Software Tools for Technology Transfer , volume=

    VNN-COMP , author=. International Journal on Software Tools for Technology Transfer , volume=. 2023 , publisher=

    2023

  78. [79]

    NeurIPS , pages=

    Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification , author=. NeurIPS , pages=

  79. [80]

    1999 , publisher=

    Recurrent neural networks: design and applications , author=. 1999 , publisher=

    1999

  80. [81]

    Neural computation , volume=

    Long short-term memory , author=. Neural computation , volume=. 1997 , publisher=

    1997

Showing first 80 references.