Pith. sign in

REVIEW 3 major objections 5 minor 175 references

A Survey on the Verification of Reinforcement Learning Policies

T0 review · 3 major / 5 minor · reviewed 2026-08-02 · deepseek-v4-flash

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

Pith's one-line read 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

desk verdict 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. read the letter →

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

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

The pith

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

The reading

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.

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

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

Extended reading notes

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

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.

Editorial extensions

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.

Reading between the lines

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.
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.

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 · score 4.0 of 10

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

  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.

Assumptions & free parameters 0 free parameters · 4 assumptions · 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.

assumptions (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.

how reviews work

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}
}
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 the authors.

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. Explanatory behavioral property. (a) Unsafe situation to [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. BaB refinement. (Adapted from [Marzari et al., 2024].) [PITH_FULL_IMAGE:figures/full_fig_p003_3.png] view at source ↗
Figures from the paper (1 more)
Figure 5
Figure 5. Figure 5: Runtime of RL verification tools. (Top) Performance on [PITH_FULL_IMAGE:figures/full_fig_p005_5.png]

Discussion (0). Sign in to comment.

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=

    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

Show all 175 references
  1. [10]

    The Probabilistic Termination Tool Amber , booktitle =

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

    2021

  2. [11]

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

  3. [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

  4. [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 =

    2025 doi

  5. [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

  6. [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

  7. [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 =

    arXiv

  8. [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

  9. [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=

  10. [19]

    2024 , url =

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

    2024

  11. [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

  12. [21]

    2023 , url =

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

    2023

  13. [22]

    2025 , booktitle =

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

    2025

  14. [23]

    IJCAI , pages =

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

    2023

  15. [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

  16. [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

  17. [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 =

  18. [27]

    2022 , url =

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

    2022

  19. [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

  20. [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=

  21. [30]

    2021 , isbn =

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

    2021 doi

  22. [31]

    CAV , pages=

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

  23. [32]

    2024 , eprint=

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

    2024

  24. [33]

    arXiv preprint arXiv:2410.23903 , year=

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

    arXiv

  25. [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

  26. [35]

    HSCC , year=

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

  27. [36]

    FMAS , year=

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

  28. [37]

    CCS , year=

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

  29. [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=

  30. [39]

    CAV , year=

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

  31. [40]

    IJCAI , year=

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

  32. [41]

    NeurIPS , year=

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

  33. [42]

    NFM , year=

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

  34. [43]

    arXiv preprint arXiv:2401.XXXX , year=

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

  35. [44]

    ATVA , year=

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

  36. [45]

    ICLR , year=

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

  37. [46]

    NeurIPS , year=

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

  38. [47]

    Proceedings of Machine Learning Research vol , volume=

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

  39. [48]

    2024 , url =

    European Union , title =. 2024 , url =

    2024

  40. [49]

    IEEE Access , volume=

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

    2021

  41. [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

  42. [51]

    Neural networks , volume=

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

    1989

  43. [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=

  44. [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

  45. [54]

    , author=

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

  46. [55]

    Journal of Machine Learning Research , volume=

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

  47. [56]

    Ethics Guidelines for Trustworthy AI , institution =

  48. [57]

    Energy and AI , institution =

  49. [58]

    International Conference on Machine Learning , pages=

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

    2019

  50. [59]

    Journal of artificial intelligence research , volume=

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

  51. [60]

    Communications of the ACM , volume=

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

    1984

  52. [61]

    Journal of the ACM , volume=

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

    1989

  53. [62]

    Nature , volume=

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

  54. [63]

    Theoretical Computer Science , volume=

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

    1979

  55. [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

  56. [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

  57. [66]

    2024 , author =

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

    2024

  58. [67]

    CAV , year=

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

  59. [68]

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

    2017

  60. [69]

    Robust Explainable AI , pages=

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

    2025

  61. [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=

  62. [71]

    NeurIPS , volume=

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

  63. [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

  64. [73]

    ACM Computing Surveys , volume=

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

    2024

  65. [74]

    ECAI 2025 , pages=

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

    2025

  66. [75]

    nature , volume=

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

    2016

  67. [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=

  68. [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

  69. [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

  70. [79]

    NeurIPS , pages=

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

  71. [80]

    1999 , publisher=

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

    1999

  72. [81]

    Neural computation , volume=

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

    1997

  73. [82]

    Advances in Neural Information Processing Systems , volume=

    Attention is all you need , author=. Advances in Neural Information Processing Systems , volume=

  74. [83]

    NESO Transmission System Operator , howpublished =

  75. [84]

    50Hertz Transmission System Operator , howpublished =

  76. [85]

    SwissGrid Transmission System Operator , howpublished =

  77. [86]

    AIRO 2023 Artificial Intelligence and Robotics 2023 , pages=

    Scaling \#DNN-Verification Tools with Efficient Bound Propagation and Parallel Computing , author=. AIRO 2023 Artificial Intelligence and Robotics 2023 , pages=

    2023

  78. [87]

    arXiv preprint arXiv:2507.05405

    Probabilistically Tightened Linear Relaxation-based Perturbation Analysis for Neural Network Verification , author=. arXiv preprint arXiv:2507.05405. Currently under review at Journal of Artificial Intelligence Research , year=

  79. [88]

    Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence , pages=

    Robust counterfactual explanations in machine learning: a survey , author=. Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence , pages=

  80. [89]

    Artificial intelligence , volume=

    Explanation in artificial intelligence: Insights from the social sciences , author=. Artificial intelligence , volume=. 2019 , publisher=

    2019

  81. [90]

    ACM computing surveys (CSUR) , volume=

    A survey of methods for explaining black box models , author=. ACM computing surveys (CSUR) , volume=. 2018 , publisher=

    2018

  82. [91]

    ICML , year=

    Towards fast computation of certified robustness for relu networks , author=. ICML , year=

  83. [92]

    IEEE SP , pages=

    Ai2: Safety and robustness certification of neural networks with abstract interpretation , author=. IEEE SP , pages=

  84. [93]

    Advances in Neural Information Processing Systems , volume=

    General cutting planes for bound-propagation-based neural network verification , author=. Advances in Neural Information Processing Systems , volume=

  85. [94]

    arXiv preprint arXiv:2312.16760 , year=

    VNN-COMP 2023: Summary and results , author=. arXiv preprint arXiv:2312.16760 , year=

    2023 arXiv

  86. [95]

    arXiv preprint arXiv:2212.10376 , year=

    The third international verification of neural networks competition (VNN-COMP 2022): Summary and results , author=. arXiv preprint arXiv:2212.10376 , year=

    2022 arXiv

  87. [96]

    International Conference on Machine Learning , year=

    A branch and bound framework for stronger adversarial attacks of relu networks , author=. International Conference on Machine Learning , year=

  88. [97]

    arXiv preprint arXiv:2405.17556 , year=

    Probabilistic Verification of Neural Networks using Branch and Bound , author=. arXiv preprint arXiv:2405.17556 , year=

    arXiv

  89. [98]

    Neural networks , volume=

    Probabilistic robustness estimates for feed-forward neural networks , author=. Neural networks , volume=. 2021 , publisher=

    2021

  90. [99]

    European Conference on Computer Vision , pages=

    ProTIP: Probabilistic robustness verification on text-to-image diffusion models against stochastic perturbation , author=. European Conference on Computer Vision , pages=. 2025 , organization=

    2025

  91. [100]

    2019 IEEE/ACM 41st International Conference on Software Engineering: New Ideas and Emerging Results (ICSE-NIER) , pages=

    Robustness of neural networks: A probabilistic and practical approach , author=. 2019 IEEE/ACM 41st International Conference on Software Engineering: New Ideas and Emerging Results (ICSE-NIER) , pages=. 2019 , organization=

    2019

  92. [101]

    NeurIPS , volume=

    A unified view of piecewise linear neural network verification , author=. NeurIPS , volume=

  93. [102]

    Journal of Machine Learning Research , volume=

    Branch and bound for piecewise linear neural network verification , author=. Journal of Machine Learning Research , volume=

  94. [103]

    arXiv preprint arXiv:1812.02795 , year=

    Verification of deep probabilistic models , author=. arXiv preprint arXiv:1812.02795 , year=

    arXiv

  95. [104]

    arXiv preprint arXiv:2402.04892 , year=

    A Unified Framework for Probabilistic Verification of AI Systems via Weighted Model Integration , author=. arXiv preprint arXiv:2402.04892 , year=

    arXiv

  96. [105]

    Proceedings of the AAAI Conference on Artificial Intelligence , volume=

    CC-Cert: A probabilistic approach to certify general robustness of neural networks , author=. Proceedings of the AAAI Conference on Artificial Intelligence , volume=

  97. [106]

    arXiv preprint arXiv:1706.07351 , year=

    An approach to reachability analysis for feed-forward relu neural networks , author=. arXiv preprint arXiv:1706.07351 , year=

    arXiv

  98. [107]

    International Conference on Hybrid Systems: Computation and Control , year=

    Synthesizing barrier certificates using neural networks , author=. International Conference on Hybrid Systems: Computation and Control , year=

  99. [108]

    International Conference on Learning Representations , year=

    Evaluating the robustness of neural networks: An extreme value theory approach , author=. International Conference on Learning Representations , year=

  100. [109]

    ICML , year=

    PROVEN: Verifying robustness of neural networks with a probabilistic approach , author=. ICML , year=

  101. [110]

    2006 , publisher=

    Extreme value theory: an introduction , author=. 2006 , publisher=

    2006

  102. [111]

    Mittelstadt and Chris Russell , title =

    Sandra Wachter and Brent D. Mittelstadt and Chris Russell , title =. CoRR , volume =

  103. [112]

    Proceedings of the

    Rafael Poyiadzi and Kacper Sokol and Ra. Proceedings of the

  104. [113]

    Proceedings of the Conference on Fairness, Accountability, and Transparency (FAT*19) , pages =

    Berk Ustun and Alexander Spangher and Yang Liu , title =. Proceedings of the Conference on Fairness, Accountability, and Transparency (FAT*19) , pages =. 2019 , optcrossref =. doi:10.1145/3287560.3287566 , timestamp =

    2019

  105. [114]

    Designing Control Barrier Function via Probabilistic Enumeration for Safe Reinforcement Learning Navigation , year=

    Marzari, Luca and Trotti, Francesco and Marchesini, Enrico and Farinelli, Alessandro , journal=. Designing Control Barrier Function via Probabilistic Enumeration for Safe Reinforcement Learning Navigation , year=

  106. [115]

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

    Junqi Jiang and Francesco Leofante and Antonio Rago and Francesca Toni , title =. Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence,. 2024 , url =

    2024

  107. [116]

    IEEE SSCI , pages=

    Evaluating robustness of counterfactual explanations , author=. IEEE SSCI , pages=. 2021 , organization=

    2021

  108. [117]

    2025 , publisher =

    Marzari, Luca and Cicalese, Ferdinando and Farinelli, Alessandro and Amato, Christopher and Marchesini, Enrico , title =. 2025 , publisher =. doi:10.1145/3770068 , journal =

    2025 doi

  109. [118]

    Advances in Neural Information Processing Systems 34 (NeurIPS21) , pages =

    Dylan Slack and Anna Hilgard and Himabindu Lakkaraju and Sameer Singh , title =. Advances in Neural Information Processing Systems 34 (NeurIPS21) , pages =. 2021 , url =

    2021

  110. [119]

    On the Adversarial Robustness of Causal Algorithmic Recourse , booktitle =

    Ricardo Dominguez. On the Adversarial Robustness of Causal Algorithmic Recourse , booktitle =

  111. [120]

    Expert Syst

    Songming Zhang and Xiaofeng Chen and Shiping Wen and Zhongshan Li , title =. Expert Syst. Appl. , volume =

  112. [121]

    Thirty-Eighth

    Francesco Leofante and Nico Potyka , title =. Thirty-Eighth. 2024 , url =

    2024

  113. [122]

    Generating Robust Counterfactual Explanations , booktitle =

    Victor Guyomard and Fran. Generating Robust Counterfactual Explanations , booktitle =

  114. [123]

    Marco Virgolin and Saverio Fracaros , title =. Artif. Intell. , volume =. 2023 , url =

    2023

  115. [124]

    Towards Robust Contrastive Explanations for Human-Neural Multi-agent Systems , booktitle =

    Francesco Leofante and Alessio Lomuscio , editor =. Towards Robust Contrastive Explanations for Human-Neural Multi-agent Systems , booktitle =

  116. [125]

    Proceedings of the 11th International Conference on Learning Representations (

    Martin Pawelczyk and Teresa Datta and Johannes van den Heuvel and Gjergji Kasneci and Himabindu Lakkaraju , title =. Proceedings of the 11th International Conference on Learning Representations (

  117. [126]

    Proceedings of the Web Conference (

    Martin Pawelczyk and Klaus Broelemann and Gjergji Kasneci , title =. Proceedings of the Web Conference (

  118. [127]

    KR , pages =

    Francesco Leofante and Elena Botoeva and Vineet Rajani , title =. KR , pages =. 2023 , url =

    2023

  119. [128]

    Proceedings of the 2024 International Conference on Autonomous Agents and Multiagent Systems (

    Recourse under Model Multiplicity via Argumentative Ensembling , author=. Proceedings of the 2024 International Conference on Autonomous Agents and Multiagent Systems (

    2024

  120. [129]

    International Conference on Machine Learning , pages =

    Sanghamitra Dutta and Jason Long and Saumitra Mishra and Cecilia Tilli and Daniele Magazzeni , title =. International Conference on Machine Learning , pages =

  121. [130]

    Proceedings of the 10th International Conference on Learning Representations (

    Emily Black and Zifan Wang and Matt Fredrikson , title =. Proceedings of the 10th International Conference on Learning Representations (

  122. [131]

    Nguyen, Tuan-Duy H and Bui, Ngoc and Nguyen, Duy and Yue, Man-Chung and Nguyen, Viet Anh , booktitle=. Robust

  123. [132]

    Proceedings of the 37th AAAI Conference on Artificial Intelligence (AAAI23) , pages =

    Jiang, Junqi and Leofante, Francesco and Rago, Antonio and Toni, Francesca , title =. Proceedings of the 37th AAAI Conference on Artificial Intelligence (AAAI23) , pages =

  124. [133]

    International Conference on Machine Learning , pages =

    Faisal Hamman and Erfaun Noorani and Saumitra Mishra and Daniele Magazzeni and Sanghamitra Dutta , title =. International Conference on Machine Learning , pages =

  125. [134]

    Junqi Jiang and Francesco Leofante and Antonio Rago and Francesca Toni , title =. Artif. Intell. , volume =. 2024 , url =

    2024

  126. [135]

    NeurIPS , pages =

    Sohini Upadhyay and Shalmali Joshi and Himabindu Lakkaraju , title =. NeurIPS , pages =

  127. [136]

    International Conference on Machine Learning , year=

    Certified adversarial robustness via randomized smoothing , author=. International Conference on Machine Learning , year=

  128. [137]

    arXiv preprint arXiv:1811.07209 , year=

    A statistical approach to assessing neural network robustness , author=. arXiv preprint arXiv:1811.07209 , year=

    arXiv

  129. [138]

    USENIX Security Symposium , pages=

    Formal security analysis of neural networks using symbolic intervals , author=. USENIX Security Symposium , pages=

  130. [139]

    Proceedings of the ACM on Programming Languages , volume=

    An abstract domain for certifying neural networks , author=. Proceedings of the ACM on Programming Languages , volume=. 2019 , publisher=

    2019

  131. [140]

    NeurIPS , volume=

    Provably bounding neural network preimages , author=. NeurIPS , volume=

  132. [141]

    Journal of Machine Learning Research , volume=

    Premap: A unifying preimage approximation framework for neural networks , author=. Journal of Machine Learning Research , volume=

  133. [142]

    Journal of Machine Learning Research (JMLR) , year =

    A comprehensive survey on safe reinforcement learning , author =. Journal of Machine Learning Research (JMLR) , year =

  134. [143]

    IEEE/AIAA Digital Avionics Systems Conference , pages=

    Policy compression for aircraft collision avoidance systems , author=. IEEE/AIAA Digital Avionics Systems Conference , pages=

  135. [144]

    Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence , pages=

    State-wise safe reinforcement learning: a survey , author=. Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence , pages=

  136. [145]

    Handbook of model checking , year=

    Satisfiability modulo theories , author=. Handbook of model checking , year=

  137. [146]

    arXiv preprint arXiv:1312.6199 , year=

    Intriguing properties of neural networks , author=. arXiv preprint arXiv:1312.6199 , year=

    arXiv

  138. [147]

    Proceedings of The 5th Annual Learning for Dynamics and Control Conference , pages =

    Probabilistic Safeguard for Reinforcement Learning Using Safety Index Guided Gaussian Process Models , author =. Proceedings of The 5th Annual Learning for Dynamics and Control Conference , pages =. 2023 , series =

    2023

  139. [148]

    Journal of Artificial Intelligence Research , volume=

    Probabilistically tightened linear relaxation-based perturbation analysis for neural network verification , author=. Journal of Artificial Intelligence Research , volume=

  140. [149]

    Symposium on Foundations of Computer Science , year =

    Pnueli, Amir , title =. Symposium on Foundations of Computer Science , year =

  141. [150]

    Conference on Robot Learning , pages =

    Verification of Neural Control Barrier Functions with Symbolic Derivative Bounds Propagation , author =. Conference on Robot Learning , pages =

  142. [151]

    IEEE Transactions on Automatic Control , volume=

    Control barrier function based quadratic programs for safety critical systems , author=. IEEE Transactions on Automatic Control , volume=. 2016 , publisher=

    2016

  143. [152]

    Conference on Decision and Control , year=

    Reinforcement learning for temporal logic control synthesis with probabilistic satisfaction guarantees , author=. Conference on Decision and Control , year=

  144. [153]

    Journal of Artificial Intelligence Research , volume=

    Implicit safe set algorithm for provably safe reinforcement learning , author=. Journal of Artificial Intelligence Research , volume=

  145. [154]

    International Conference on Machine Learning , year=

    Lyapunov-stable neural control for state and output feedback: a novel formulation , author=. International Conference on Machine Learning , year=

  146. [155]

    Machine Learning for Engineering Modeling, Simulation, and Design Workshop , pages=

    Exact preimages of neural network aircraft collision avoidance systems , author=. Machine Learning for Engineering Modeling, Simulation, and Design Workshop , pages=

  147. [156]

    2004 , publisher=

    Operations research: applications and algorithm , author=. 2004 , publisher=

    2004

  148. [157]

    arXiv preprint arXiv:1409.1259 , year=

    On the properties of neural machine translation: Encoder-decoder approaches , author=. arXiv preprint arXiv:1409.1259 , year=

    arXiv

  149. [158]

    ICLR , year=

    Evaluating robustness of neural networks with mixed integer programming , author=. ICLR , year=

  150. [159]

    International Conference on Tools and Algorithms for the Construction and Analysis of Systems , pages=

    Provable preimage under-approximation for neural networks , author=. International Conference on Tools and Algorithms for the Construction and Analysis of Systems , pages=. 2024 , organization=

    2024

  151. [160]

    Foundations and Trends

    Algorithms for verifying deep neural networks , author=. Foundations and Trends. 2021 , publisher=

    2021

  152. [161]

    Journal of Mathematical Analysis and Applications , issn =

    Optimal Control of Markov Processes with Incomplete State Information I , author =. Journal of Mathematical Analysis and Applications , issn =. 1965 , doi =

    1965

  153. [162]

    Proceedings of the 6th Conference on Theoretical Aspects of Rationality and Knowledge , pages =

    Boutilier, Craig , title =. Proceedings of the 6th Conference on Theoretical Aspects of Rationality and Knowledge , pages =. 1996 , isbn =

    1996

  154. [163]

    Frans A Oliehoek and Christopher Amato , title =

  155. [164]

    Bayen and Yi Wu , title =

    Chao Yu and Akash Velu and Eugene Vinitsky and Yu Wang and Alexandre M. Bayen and Yi Wu , title =. Conference on Neural Information Processing Systems (NeurIPS) , year =

  156. [165]

    Foerster and Gregory Farquhar and Triantafyllos Afouras and Nantas Nardelli and Shimon Whiteson , title =

    Jakob N. Foerster and Gregory Farquhar and Triantafyllos Afouras and Nantas Nardelli and Shimon Whiteson , title =. Conference on Artificial Intelligence (AAAI) , year =

  157. [166]

    Conference on Neural Information Processing Systems (NeurIPS) , year =

    Ryan Lowe and Yi Wu and Aviv Tamar and Jean Harb and Pieter Abbeel and Igor Mordatch , title =. Conference on Neural Information Processing Systems (NeurIPS) , year =

  158. [167]

    International Conference on Learning Representations (ICLR) , year =

    Jianhao Wang and Zhizhou Ren and Terry Liu and Yang Yu and Chongjie Zhang , title =. International Conference on Learning Representations (ICLR) , year =

  159. [168]

    NeurIPS , year=

    Benchmarking Multi-Agent Deep Reinforcement Learning Algorithms in Cooperative Tasks , author=. NeurIPS , year=

  160. [169]

    Journal of Machine Learning Research , year =

    Matteo Bettini and Amanda Prorok and Vincent Moens , title =. Journal of Machine Learning Research , year =

  161. [170]

    2017 , eprint=

    Deep Recurrent Q-Learning for Partially Observable MDPs , author=. 2017 , eprint=

    2017

  162. [171]

    CoRL , year =

    Macro-Action-Based Deep Multi-Agent Reinforcement Learning , author =. CoRL , year =

  163. [172]

    2016 , Eprint =

    Greg Brockman and Vicki Cheung and Ludwig Pettersson and Jonas Schneider and John Schulman and Jie Tang and Wojciech Zaremba , Title =. 2016 , Eprint =

    2016

  164. [173]

    From Sim to Real: A Pipeline for Training and Deploying Traffic Smoothing Cruise Controllers , year=

    Lichtlé, Nathan and Vinitsky, Eugene and Nice, Matthew and Bhadani, Rahul and Bunting and others , journal=. From Sim to Real: A Pipeline for Training and Deploying Traffic Smoothing Cruise Controllers , year=

  165. [174]

    and Barto, Andrew G

    Sutton, Richard S. and Barto, Andrew G. , publisher =. Reinforcement Learning: An Introduction , url =

  166. [175]

    2024 , eprint=

    An Introduction to Centralized Training for Decentralized Execution in Cooperative Multi-Agent Reinforcement Learning , author=. 2024 , eprint=

    2024

  167. [176]

    Shield Decentralization for Safe Multi-Agent Reinforcement Learning , year =

    Melcer, Daniel and Amato, Christopher and Tripakis, Stavros , booktitle =. Shield Decentralization for Safe Multi-Agent Reinforcement Learning , year =

Pith tools

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