Pith. sign in

REVIEW 3 major objections 4 minor 42 references

Learning Verifiable Control Policies Using Relaxed Verification

T0 review · 3 major / 4 minor · reviewed 2026-08-16 · deepseek-v4-flash

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

Pith's one-line read Safety verification during training yields policies that pass checks

desk verdict A useful verification-in-the-loop training idea with a likely sign error in the reported loss weights; the core approach is worth refereeing, but the experiments need cleaning up. read the letter →

arxiv 2504.16879 v1 pith:63F6IZ2Q submitted 2025-04-23 eess.SY cs.LGcs.SY

Puja Chaudhury , Alexander Estornell , Michael Everett This is my paper · ORCID
classification eess.SYcs.LGcs.SY
keywords verification-in-the-looptrainingneuralfeedbackloopCROWNreachabilityanalysisreach-avoidspecificationinvariantsetboundtightnesslossunicyclecontrolquadrotor
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

This paper argues that safety verification should not wait until after training; instead, the verifier should participate in training so that the learned policy is verifiable with cheap relaxed bounds. The authors train neural network control policies by computing differentiable over-approximations of forward reachable sets with CROWN and adding loss terms for goal-reaching, obstacle overlap, bound tightness, and invariance. On unicycle and 6D quadrotor models, the trained policies reach goal regions while the CROWN reachable sets avoid obstacles, and in one experiment the reachable set at a fixed time is a certified forward invariant set. If the approach is right, safety-critical learning-based control can rely on lightweight, fast verification at runtime rather than expensive post-hoc analysis.

What carries the argument

The central mechanism is CROWN, a LiRPA-style backward linear-relaxation bound propagation that computes hyperrectangle outer bounds on the image of a computation graph. Applied to the closed-loop dynamics $x_{t+1}=f(x_t,\pi_\theta(x_t))$, it produces reachable set over-approximations $\bar{R}_t$ that are differentiable with respect to the policy parameters $\theta$. These bounds feed the loss terms $L_{\mathrm{overlap}}$, $L_{\mathrm{goal}}$, $L_{\mathrm{vol}}$, and $L_{\mathrm{inv}}$, so gradient descent directly optimizes verifiability of the resulting closed-loop system.

What would settle it

Run the unicycle experiments with $w_{\mathrm{overlap\,danger}}$ changed from $-15$ to a positive value and with $t_{\mathrm{inv}}$ swept over nearby steps; if the CROWN reachable sets then intersect an obstacle or $\bar{R}_{t_{\mathrm{inv}}}$ stops being forward invariant, the reported verification success is an artifact of those settings. Independently, densely sample initial states in $X_0$ and simulate the closed loop; any true trajectory that hits an obstacle while the CROWN bounds avoid it would falsify the claimed specification satisfaction.

Watch

Extended reading notes

Core claim

The central claim is that including verification-derived terms in the training loss produces neural control policies whose closed-loop behavior, as bounded by the CROWN relaxation, provably satisfies reach-avoid and invariance specifications. The paper reports, for example, a 3-layer ReLU unicycle policy whose CROWN over-approximations $\bar{R}_1,\dots,\bar{R}_{24}$ do not intersect the avoid sets and reach the goal region in 24 steps, and a separate run where $\bar{R}_{22}$ is forward invariant. A key sub-claim is that the bound-volume term $L_{\mathrm{vol}}$ lets a lightweight relaxed verifier produce tight bounds that normally require expensive branch-and-bound. The method requires no external reward signal; all loss terms are computed from the reachable set bounds themselves.

Load-bearing premise

The hand-tuned soft penalty weights—particularly the negative obstacle-overlap weight ($w_{\mathrm{overlap\,danger}}=-15$) and the fixed invariance start time $t_{\mathrm{inv}}=22$—must produce specification satisfaction that survives reasonable perturbations of those choices.

Editorial extensions

If this is right

  • Runtime monitoring can use the same cheap CROWN bounds the policy was trained against, so specifications that change during operation can be re-checked quickly.
  • The bound-volume term reduces the conservatism of relaxed verification, so guaranteeing a trained policy may not require branch-and-bound or SDP.
  • The invariance term can turn a trained policy into one with a certified forward invariant set around the goal, verified by a single subset check.
  • The approach trains policies without an external reward signal, using only reachable-set-derived losses.
  • The method scales to a 6D quadrotor model with obstacles within thousands of training epochs.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A testable extension is to vary the invariance start time $t_{\mathrm{inv}}$ and the obstacle-overlap weight; the paper fixes $t_{\mathrm{inv}}=22$ and sets $w_{\mathrm{overlap\,danger}}=-15$, so robustness of the reported invariant set and obstacle avoidance to those choices is open.
  • The same differentiable-CROWN loss could be applied to backward reachable sets or to Lyapunov-like certificate search, potentially eliminating the need for a separate certificate network.
  • If bound tightness transfers across initial sets, one could pre-train on a coarse initial set and refine on smaller subsets, making verified-in-the-loop training scale to higher-dimensional systems.
  • The absence of an external reward signal suggests the reachability-derived losses themselves could serve as a dense reward substitute in reinforcement learning settings.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 4 minor

Summary. The paper proposes a verification-in-the-loop training method for neural network control policies. At each training iteration, differentiable CROWN reachable-set over-approximations are used to define loss terms that penalize overlap with obstacles, encourage goal reaching, minimize reachable-set volume, and encourage late-horizon forward invariance. The closed-loop bounds are computed iteratively over a finite horizon and are used both as training signals and, after training, as verification certificates. Experiments on a unicycle model and a 6D quadrotor model report reach-avoid behavior and an apparent forward invariant set, along with a qualitative comparison against a numerical-gradient baseline.

Significance. If the reported results hold, the contribution is useful: it provides a lightweight mechanism to bias policy search toward policies that are amenable to fast, sound verification, and the use of sound CROWN bounds means a verified over-approximation is a genuine safety certificate for the true dynamics. The paper releases its code and includes a comparison to a prior numerical-gradient approach. However, the evidence is currently weakened by an apparent sign inconsistency in the main loss equation, the lack of statistical evaluation, and the hand-picked invariance start time. These issues must be resolved before the central claims are established.

major comments (3)
  1. [Section IV-A, Eq. (10) and Eq. (5)] The loss weights in Eq. (10) contradict the stated objectives. Eq. (5) defines L_overlap as the volume of intersection between the reachable box and a target region. With w_overlap_danger = -15, minimizing -15 * L_overlap_obs encourages the reachable set to intersect obstacles, and with w_overlap_goal = +20, minimizing +20 * L_overlap_goal discourages intersection with the goal. Both signs are opposite to the intended reach-avoid objective. Furthermore, Section IV-C states "wobstacle overlap = 20, wgoal overlap = 15" while Eq. (11) reports w_overlap_goal = -15 and omits the obstacle term entirely. Because the training objective is the mechanism by which the reported policies are obtained, this inconsistency must be resolved by checking the released code and correcting either the formulas or the reported weights; as printed, the main experimental claim is unsupported.
  2. [Section IV-C, Eq. (8) and the invariance experiment] The reported invariant set is a direct consequence of the choice t_inv = 22. Linv penalizes ||\bar{x}_{t+1} - \bar{x}_t|| for all t >= t_inv, so the objective explicitly encourages \bar{R}_{23} to coincide with \bar{R}_{22}. The CROWN subset check is a valid sound verification, but the demonstration does not establish the method's robustness: no ablation over t_inv, no multiple seeds, and no evidence that an invariant set is found when t_inv is not chosen to match the final invariant set. The claim that the method "can lead to an invariant set" would be considerably strengthened by reporting success rates across t_inv values and random initializations.
  3. [Section IV, overall experimental design] The results consist of single training runs and single trajectory visualizations, without seeds, error bars, or quantitative success metrics. The comparison in Section IV-A with the numerical-gradient baseline is qualitative (Fig. 2), and the text does not report how often each method produces a policy that passes the CROWN verification. Since the central assertion is that the proposed loss reliably yields verifiable policies, at least success-rate statistics over multiple random seeds and quantitative measures of reachable-set volume and obstacle clearance should be reported.
minor comments (4)
  1. [Eq. (8)] The two terms printed as ||\bar{x}_{t+1} - \bar{x}_t||^2 appear identical; presumably one should apply to the lower bound \underline{x}_t and the other to the upper bound \bar{x}_t.
  2. [Section III-A, Eq. (5) and surrounding text] The phrase "penalizes the volume of (positional) reachable sets that are not within a region" is inconsistent with the displayed formula, which computes the volume of the intersection with the region; please clarify the intended penalization.
  3. [Section IV-B, last paragraph] The phrase "true reachable sets according to the sampled trajectories" should read "sampled trajectories" or "empirical reachable sets," since finitely many samples do not determine a true reachable set.
  4. [Algorithm 1, line 6] The call CROWN(f, \bar{R}_t) should specify that the controller parameters are \theta_i, and the notation for the set of avoid sets A0:A in the input list is undefined.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the paper's loss terms and CROWN-based evaluation are aligned by the method's stated objective, not by a hidden definitional reduction.

full rationale

The paper's derivation chain is self-contained: the approach is to define a loss (Eqs. 5-8) from CROWN reachable bounds and optimize it (Algorithm 1); the experiments then evaluate the optimized policy with the same sound CROWN verifier. This is the method's stated objective, not a hidden reduction. The tightness and invariance results are direct consequences of optimizing Lvol and Linv, but the paper presents them as demonstrations of the loss terms' effect, not as independent predictions. CROWN is an external, sound relaxation (Theorem II.1 cited to [1]), so using it for both loss and evaluation does not make the evaluation circular. No parameter is fitted to a subset of data and then used to 'predict' that same subset; tinv and weights are stated hyperparameters. No load-bearing self-citation or imported uniqueness theorem appears. The acknowledged caveat that soft penalties may not guarantee safety (Section III) is a limitation, not circularity. The apparent sign inconsistencies in Eqs. (10)/(11) are correctness risks but do not constitute a circular derivation.

Assumptions & free parameters 4 free parameters · 3 assumptions · 0 invented entities

The central claim rests on standard soundness of LiRPA over-approximations plus the heuristic assumption that hand-tuned soft penalties can shape the policy. The loss weights and tinv are free parameters that directly influence the reported successes.

free parameters (4)
  • Unicycle loss weights (w_goal=8, w_overlap_danger=-15, w_overlap_goal=20, w_vol=0.5)
    Hand-chosen per experiment; no sensitivity analysis. The negative w_overlap_danger is likely a sign error if the loss is meant to penalize obstacle overlap.
  • Invariance start timestep tinv = 22
    Chosen by hand; the reported forward invariant set is \bar{R}_{22}, the same timestep where the invariance loss becomes active.
  • Quadrotor loss weights (w_goal=50, w_overlap=-50, w_vel=0.05, w_vol=40, w_obs_entry=500, w_obs_prox=100)
    Hand-tuned; the negative w_overlap is again suspicious for an obstacle-overlap penalty.
  • Quadrotor volume loss bias and scaling = bias -vol(X0), scaled by 1/vol(X0)
    Ad hoc normalization; the paper notes these constants 'should be able to be removed'.
assumptions (3)
  • standard math CROWN/LiRPA produces sound over-approximations of the image of a neural network or computation graph over a box input set
    Theorem II.1 and Corollary II.2; assumed sound and implemented correctly in auto_LiRPA.
  • domain assumption The discrete-time dynamics (unicycle Eq. 9, quadrotor Eq. 12) exactly represent the system being controlled
    The safety guarantees apply to these models, not to any physical hardware; model mismatch is not discussed.
  • ad hoc to paper Minimizing the weighted sum of soft reachability losses will drive the policy toward satisfying the specification
    The paper states this is not guaranteed and suggests [35] for hard guarantees.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Learning Verifiable Control Policies Using Relaxed Verification." pith.science (2026). https://pith.science/paper/63F6IZ2Q

@misc{pith2026250416879,
  author       = {Pith},
  title        = {Pith review of: Learning Verifiable Control Policies Using Relaxed Verification},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/63F6IZ2Q}},
  note         = {Machine review of arXiv:2504.16879}
}
read the original abstract

To provide safety guarantees for learning-based control systems, recent work has developed formal verification methods to apply after training ends. However, if the trained policy does not meet the specifications, or there is conservatism in the verification algorithm, establishing these guarantees may not be possible. Instead, this work proposes to perform verification throughout training to ultimately aim for policies whose properties can be evaluated throughout runtime with lightweight, relaxed verification algorithms. The approach is to use differentiable reachability analysis and incorporate new components into the loss function. Numerical experiments on a quadrotor model and unicycle model highlight the ability of this approach to lead to learned control policies that satisfy desired reach-avoid and invariance specifications.

Figures

Figures reproduced from arXiv: 2504.16879 by the authors.

Figure 1
Figure 1. Learning verifiable control policies. The objective [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗
Figure 2
Figure 2. Comparison of reachable sets computed by each method for a unicycle model and reach-avoid specification. The [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Effect of Bound Volume Loss, Lvol. For the unicycle system with a different start/goal from before, the reachable sets calculated by CROWN after training are much tighter when wvol = 4 (left) than wvol = 0.05 (right), even though the system’s performance and true reachable sets are nearly identical. This highlights the benefit of including Lvol in the training process: it enables obtaining reasonably tight bounds ev… view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Effect of Invariance Loss, Linv. Without considering this loss, the reachable sets often continue to grow or go past the goal (e.g., see [PITH_FULL_IMAGE:figures/full_fig_p005_4.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

42 extracted references · 10 canonical work pages

  1. [33]

    Verification in the Loop: Correct-by-Construction Control Learning with Reach-avoid Guarantees

    Y . Wang, C. Huang, Z. Wang, Z. Wang, and Q. Zhu, “Verification in the loop: Correct-by-construction control learning with reach-avoid guarantees,” arXiv preprint arXiv:2106.03245 , 2021

    work page Pith review arXiv 2021

  2. [35]

    Verified safe reinforce- ment learning for neural network dynamic models,

    J. Wu, H. Zhang, and Y . V orobeychik, “Verified safe reinforce- ment learning for neural network dynamic models,” arXiv preprint arXiv:2405.15994, 2024

    arXiv 2024

  3. [1]

    Efficient neural network robustness certification with general activa- tion functions,

    H. Zhang, T.-W. Weng, P.-Y . Chen, C.-J. Hsieh, and L. Daniel, “Efficient neural network robustness certification with general activa- tion functions,” Advances in Neural Information Processing Systems (NeurIPS), 2018

    2018

  4. [2]

    Towards fast computation of certified robustness for relu networks,

    L. Weng, H. Zhang, H. Chen, Z. Song, C.-J. Hsieh, L. Daniel, D. Boning, and I. Dhillon, “Towards fast computation of certified robustness for relu networks,” in International Conference on Machine Learning (ICML), 2018, pp. 5276–5285

    2018

  5. [3]

    Automatic perturbation analy- sis for scalable certified robustness and beyond,

    K. Xu, Z. Shi, H. Zhang, Y . Wang, K.-W. Chang, M. Huang, B. Kailkhura, X. Lin, and C.-J. Hsieh, “Automatic perturbation analy- sis for scalable certified robustness and beyond,” Advances in Neural Information Processing Systems (NeurIPS) , vol. 33, pp. 1129–1141, 2020

    2020

  6. [4]

    Semidefinite relax- ations for certifying robustness to adversarial examples,

    A. Raghunathan, J. Steinhardt, and P. S. Liang, “Semidefinite relax- ations for certifying robustness to adversarial examples,” Advances in Neural Information Processing Systems (NeurIPS) , vol. 31, 2018

    2018

  7. [5]

    Evaluating robustness of neural networks with mixed integer programming,

    V . Tjeng, K. Y . Xiao, and R. Tedrake, “Evaluating robustness of neural networks with mixed integer programming,” in International Conference on Learning Representations (ICLR) , 2018

    2018

  8. [6]

    The marabou framework for verification and analysis of deep neural networks,

    G. Katz, D. A. Huang, D. Ibeling, K. Julian, C. Lazarus, R. Lim, P. Shah, S. Thakoor, H. Wu, A. Zelji´c et al., “The marabou framework for verification and analysis of deep neural networks,” in International Conference on Computer-Aided Verification (CAV), 2019, pp. 443–452

    2019

Show all 42 references
  1. [7]

    Re- luplex: An efficient SMT solver for verifying deep neural networks,

    G. Katz, C. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer, “Re- luplex: An efficient SMT solver for verifying deep neural networks,” in International Conference on Computer-Aided Verification (CAV) , 2017, pp. 97–117

    2017

  2. [8]

    Verifying low-dimensional input neural networks via input quantization,

    K. Jia and M. Rinard, “Verifying low-dimensional input neural networks via input quantization,” in International Static Analysis Symposium, 2021, pp. 206–214

    2021

  3. [9]

    Reachable polyhedral marching (RPM): A safety verification algorithm for robotic systems with deep neural network components,

    J. A. Vincent and M. Schwager, “Reachable polyhedral marching (RPM): A safety verification algorithm for robotic systems with deep neural network components,” in IEEE International Conference on Robotics and Automation (ICRA) , 2021, pp. 9029–9035

    2021

  4. [10]

    Overt: An algorithm for safety verification of neural network control policies for nonlinear systems,

    C. Sidrane, A. Maleki, A. Irfan, and M. J. Kochenderfer, “Overt: An algorithm for safety verification of neural network control policies for nonlinear systems,” Journal of Machine Learning Research , vol. 23, no. 117, pp. 1–45, 2022

    2022

  5. [11]

    One-shot reachability anal- ysis of neural network dynamical systems,

    S. Chen, V . M. Preciado, and M. Fazlyab, “One-shot reachability anal- ysis of neural network dynamical systems,” in2023 IEEE International Conference on Robotics and Automation (ICRA) . IEEE, 2023, pp. 10 546–10 552

    2023

  6. [12]

    Reachability analysis of neural feedback loops,

    M. Everett, G. Habibi, C. Sun, and J. P. How, “Reachability analysis of neural feedback loops,” IEEE Access, vol. 9, pp. 163 938–163 953, 2021

    2021

  7. [13]

    A reachability method for verifying dynamical systems with deep neural network controllers,

    K. D. Julian and M. J. Kochenderfer, “A reachability method for verifying dynamical systems with deep neural network controllers,” arXiv preprint arXiv:1903.00520 , 2019

    1903 arXiv

  8. [14]

    Reach-SDP: Reachability analysis of closed-loop systems with neural network controllers via semidefinite programming,

    H. Hu, M. Fazlyab, M. Morari, and G. J. Pappas, “Reach-SDP: Reachability analysis of closed-loop systems with neural network controllers via semidefinite programming,” in IEEE Conference on Decision and Control (CDC) , 2020, pp. 5929–5934

    2020

  9. [15]

    Polar-express: Efficient and precise formal reachability analysis of neural-network controlled systems,

    Y . Wang, W. Zhou, J. Fan, Z. Wang, J. Li, X. Chen, C. Huang, W. Li, and Q. Zhu, “Polar-express: Efficient and precise formal reachability analysis of neural-network controlled systems,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems , vol. 43, n...

    2023

  10. [16]

    Verisig: verifying safety properties of hybrid systems with neural network con- trollers,

    R. Ivanov, J. Weimer, R. Alur, G. J. Pappas, and I. Lee, “Verisig: verifying safety properties of hybrid systems with neural network con- trollers,” in International Conference on Hybrid Systems: Computation and Control, 2019, pp. 169–178

    2019

  11. [17]

    Reachability analysis for neural feedback systems using regressive polynomial rule inference,

    S. Dutta, X. Chen, and S. Sankaranarayanan, “Reachability analysis for neural feedback systems using regressive polynomial rule inference,” in International Conference on Hybrid Systems: Computation and Control, 2019, pp. 157–168

    2019

  12. [18]

    Reachnn: Reachability analysis of neural-network controlled systems,

    C. Huang, J. Fan, W. Li, X. Chen, and Q. Zhu, “Reachnn: Reachability analysis of neural-network controlled systems,” ACM Transactions on Embedded Computing Systems (TECS), vol. 18, no. 5s, pp. 1–22, 2019

    2019

  13. [19]

    Reachnn*: A tool for reachability analysis of neural-network controlled systems,

    J. Fan, C. Huang, X. Chen, W. Li, and Q. Zhu, “Reachnn*: A tool for reachability analysis of neural-network controlled systems,” in International Symposium on Automated Technology for Verification and Analysis, 2020, pp. 537–542

    2020

  14. [20]

    Reachable set estimation for neural network control systems: A simulation-guided approach,

    W. Xiang, H.-D. Tran, X. Yang, and T. T. Johnson, “Reachable set estimation for neural network control systems: A simulation-guided approach,” IEEE Transactions on Neural Networks and Learning Systems, vol. 32, no. 5, pp. 1821–1830, 2020

    2020

  15. [21]

    Neural network compression of ACAS Xu early prototype is unsafe: Closed-loop verification through quantized state backreachability,

    S. Bak and H.-D. Tran, “Neural network compression of ACAS Xu early prototype is unsafe: Closed-loop verification through quantized state backreachability,” in NASA Formal Methods, 2022, pp. 280–298

    2022

  16. [22]

    Beta-crown: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification,

    S. Wang, H. Zhang, K. Xu, X. Lin, S. Jana, C.-J. Hsieh, and J. Z. Kolter, “Beta-crown: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification,” arXiv preprint arXiv:2103.06624 , 2021

    2021 arXiv

  17. [23]

    Safety verification of neural feedback systems based on constrained zonotopes,

    Y . Zhang and X. Xu, “Safety verification of neural feedback systems based on constrained zonotopes,” in 2022 IEEE 61st Conference on Decision and Control (CDC) . IEEE, 2022, pp. 2737–2744

    2022

  18. [24]

    Scalable verified training for provably robust image classification,

    S. Gowal, K. D. Dvijotham, R. Stanforth, R. Bunel, C. Qin, J. Uesato, R. Arandjelovic, T. Mann, and P. Kohli, “Scalable verified training for provably robust image classification,” in Proceedings of the IEEE/CVF International Conference on Computer Vision , 2019, pp. 4842–4851

    2019

  19. [25]

    Neural Lyapunov control,

    Y .-C. Chang, N. Roohi, and S. Gao, “Neural Lyapunov control,” Ad- vances in Neural Information Processing Systems (NeurIPS) , vol. 32, 2019

    2019

  20. [26]

    Learning certified control using contrac- tion metric,

    D. Sun, S. Jha, and C. Fan, “Learning certified control using contrac- tion metric,” in Conference on Robot Learning . PMLR, 2021, pp. 1519–1539

    2021

  21. [27]

    Actor-critic reinforcement learning for control with stability guarantee,

    M. Han, L. Zhang, J. Wang, and W. Pan, “Actor-critic reinforcement learning for control with stability guarantee,” IEEE Robotics and Automation Letters, vol. 5, no. 4, pp. 6217–6224, 2020

    2020

  22. [28]

    Learning safe multi-agent control with decentralized neural barrier certificates,

    Z. Qin, K. Zhang, Y . Chen, J. Chen, and C. Fan, “Learning safe multi-agent control with decentralized neural barrier certificates,” in International Conference on Learning Representations (ICLR) , 2020

    2020

  23. [29]

    Lyapunov- stable neural-network control,

    H. Dai, B. Landry, L. Yang, M. Pavone, and R. Tedrake, “Lyapunov- stable neural-network control,” in Robotics: Science and Systems , Virtual, Jul. 2021. [Online]. Available: https://arxiv.org/pdf/2109. 14152.pdf

    2021

  24. [30]

    Safe control with learned certificates: A survey of neural Lyapunov, barrier, and contraction methods,

    C. Dawson, S. Gao, and C. Fan, “Safe control with learned certificates: A survey of neural Lyapunov, barrier, and contraction methods,” arXiv preprint arXiv:2202.11762, 2022

    2022 arXiv

  25. [31]

    Learning-based verification of stochastic dynamical systems with neural network policies,

    T. Badings, W. Koops, S. Junges, and N. Jansen, “Learning-based verification of stochastic dynamical systems with neural network policies,” arXiv preprint arXiv:2406.00826 , 2024

    2024 arXiv

  26. [32]

    Lyapunov-stable neural control for state and output feedback: A novel formulation,

    L. Yang, H. Dai, Z. Shi, C.-J. Hsieh, R. Tedrake, and H. Zhang, “Lyapunov-stable neural control for state and output feedback: A novel formulation,” arXiv preprint arXiv:2404.07956 , 2024

    2024 arXiv

  27. [34]

    Joint differentiable optimization and verification for certified reinforcement learning,

    Y . Wang, S. Zhan, Z. Wang, C. Huang, Z. Wang, Z. Yang, and Q. Zhu, “Joint differentiable optimization and verification for certified reinforcement learning,” in Proceedings of the 2023 ACM/IEEE 14th International Conference on Cyber-Physical Systems (ICCPS). ACM, 2023, pp. 13...

    2023 arXiv

  28. [36]

    Bunel, J

    R. Bunel, J. Uesato, and L. Berrada, jax verify, 8 2023. [Online]. Available: https://github.com/google-deepmind/jax verify

    2023

  29. [37]

    Z. Shi, K. Xu, and H. Zhang, auto LiRPA, 3 2025. [Online]. Available: https://github.com/Verified-Intelligence/auto LiRPA

    2025

  30. [38]

    Ttt: A temporal refinement heuristic for tenuously tractable discrete time reachability problems,

    C. Sidrane and J. Tumova, “Ttt: A temporal refinement heuristic for tenuously tractable discrete time reachability problems,”arXiv preprint arXiv:2407.14394, 2024

    2024 arXiv

  31. [39]

    Constraint-aware refinement for safety verification of neural feedback loops,

    N. Rober and J. P. How, “Constraint-aware refinement for safety verification of neural feedback loops,” IEEE Control Systems Letters , 2024

    2024

  32. [40]

    Adam: A method for stochastic optimiza- tion,

    D. P. Kingma and J. Ba, “Adam: A method for stochastic optimiza- tion,” arXiv preprint arXiv:1412.6980 , 2014

    2014 arXiv

  33. [41]

    Safety verification and robustness analysis of neural networks via quadratic constraints and semidefinite programming,

    M. Fazlyab, M. Morari, and G. J. Pappas, “Safety verification and robustness analysis of neural networks via quadratic constraints and semidefinite programming,” IEEE Transactions on Automatic Control, vol. 67, no. 1, pp. 1–15, 2020

    2020

  34. [42]

    Backward reachability analysis of neural feedback loops: Techniques for linear and nonlinear systems,

    N. Rober, S. M. Katz, C. Sidrane, E. Yel, M. Everett, M. J. Kochen- derfer, and J. P. How, “Backward reachability analysis of neural feedback loops: Techniques for linear and nonlinear systems,” IEEE Open Journal of Control Systems , vol. 2, pp. 108–124, 2023

    2023

Pith tools

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