pith. sign in

arxiv: 2604.15659 · v1 · submitted 2026-04-17 · 📡 eess.SY · cs.SY

Verification of Autonomous Systems with Optimal Controllers

Dylan Le , Joel McCandless , Carlos Varela , Radoslav Ivanov This is my paper

Pith reviewed 2026-05-10 08:29 UTC · model grok-4.3

classification 📡 eess.SY cs.SY
keywords reachability analysisoptimal controllersgradient descentsafety verificationautonomous systemshybrid dynamical systemsquadrotorcartpole
0
0 comments X

The pith

Treating gradient descent as an embedded digital dynamical system enables reachability-based safety verification for autonomous systems using optimal controllers.

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

The paper seeks to make safety verification feasible for control systems that rely on optimal controllers solved via gradient descent. Optimal controllers minimize costs but are difficult to verify directly due to their online optimization nature and potential for inexact solutions under time limits. The approach models the gradient descent process as its own discrete dynamical system running in parallel with the continuous physical dynamics, augmenting the state with the current control values. This allows standard reachability tools to compute sets of possible states that include both plant evolution and controller iterations. If the method works, it means engineers can certify that approximate optimal control still prevents the system from reaching unsafe regions, addressing a key barrier to using such controllers in safety-critical applications.

Core claim

By embedding the gradient descent iterations as a discrete dynamical system within the continuous plant model, with the control inputs included in the augmented state, the authors construct a reachability algorithm that can verify safety properties for systems using optimal controllers, demonstrated on a quadrotor and cartpole.

What carries the argument

The hybrid dynamical system formed by composing the continuous physical dynamics with the discrete gradient descent iterations, treating controls as state variables.

Load-bearing premise

The assumption that the gradient descent iterations can be faithfully represented as a discrete dynamical system whose reachable sets, when composed with the continuous plant, still allow meaningful safety verification without introducing unacceptable conservatism or missing unsafe behaviors.

What would settle it

An experiment on the quadrotor or cartpole where the actual closed-loop system with gradient descent enters an unsafe state that the computed reachable sets of the composed model had declared unreachable.

Figures

Figures reproduced from arXiv: 2604.15659 by Carlos Varela, Dylan Le, Joel McCandless, Radoslav Ivanov.

Figure 1
Figure 1. Figure 1: System dynamics as a transition system. The tran [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Illustration of shrink wrapping. arithmetic is sufficient to approximate the physical plant dynamics TMf , the digital propagation of TMu through gradient descent presents some considerable challenges. D. Technical Challenges While formulating the problem as an augmented transition system and approximating conservative bounds using TMs is intuitively appealing, finding the reachable sets is very challengin… view at source ↗
Figure 3
Figure 3. Figure 3: Reachability analysis of the running examples. Reachable sets are shown in colored boxes. Simulation steps are [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
read the original abstract

This paper considers the problem of reachability analysis of control systems with optimal controllers, as a first step towards verifying the safety and correctness of such systems. Despite their appeal in guaranteeing task satisfaction through cost minimization, optimal controllers are often challenging to assure. In particular, as system dynamics grow in complexity, solving the resulting optimization problem may be difficult, especially given time and computation constraints on real platforms. Thus, it is essential to verify that, even if the optimal solution is not always found, such controllers still accomplish the high-level control objective. In this paper, we focus on gradient descent algorithms and design a reachability algorithm by treating gradient descent as a separate (digital) dynamical system, embedded in the original (physical) dynamical system, with controls as part of the state. We evaluate the feasibility of the proposed method on two control systems, a two-dimensional quadrotor and a cartpole.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper proposes a reachability analysis method for control systems employing optimal controllers approximated via gradient descent. It models the gradient descent iterations as a discrete dynamical system embedded in the continuous plant dynamics, with the control input included as part of the augmented state vector. Feasibility is illustrated on a two-dimensional quadrotor and a cartpole system.

Significance. If the embedding is made sound, the work could enable formal verification of safety properties for autonomous systems that rely on online optimization under computational constraints, a common setting in robotics and cyber-physical systems. The integration of the optimizer dynamics directly into the hybrid reachability framework addresses a practical gap between control synthesis and assurance.

major comments (2)
  1. [Reachability algorithm] The reachability algorithm section: treating gradient descent as an embedded discrete dynamical system requires that the number of iterations per control interval be fixed or bounded a priori. Without this, the hybrid reachable-set computation either becomes non-terminating or arbitrarily conservative, directly undermining the claim of meaningful safety verification for the composed system.
  2. [Evaluation] Evaluation on the quadrotor and cartpole: the manuscript supplies no reachable-set computation details, quantitative results (e.g., set volumes, computation times, or safety margins), or comparison against baselines. This prevents verification that the method supports the central claim of feasible verification under the embedding.
minor comments (2)
  1. [Abstract] The abstract would benefit from a brief statement on how iteration counts or timing are managed in the discrete embedding to avoid the conservatism issue.
  2. [Notation] Notation for the augmented state (plant state plus control) should be defined explicitly at first use to improve readability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their thoughtful and constructive review. The comments highlight important aspects of making the embedding approach rigorous and the evaluation more convincing. We address each major comment below and outline the revisions we will make.

read point-by-point responses

  1. Referee: [Reachability algorithm] The reachability algorithm section: treating gradient descent as an embedded discrete dynamical system requires that the number of iterations per control interval be fixed or bounded a priori. Without this, the hybrid reachable-set computation either becomes non-terminating or arbitrarily conservative, directly undermining the claim of meaningful safety verification for the composed system.

    Authors: We agree that the number of gradient descent iterations per control interval must be fixed or bounded for the hybrid reachability computation to terminate and remain meaningful. Our modeling treats the optimizer as a discrete dynamical system with a predetermined number of steps per control period, which is the standard assumption for real-time implementations under computational constraints. We will revise the reachability algorithm section to state this assumption explicitly, explain how it guarantees finite termination of the reachability analysis, and discuss the resulting conservatism when an upper bound is used instead of a fixed count. This clarification addresses the concern without changing the core technical contribution. revision: yes

  2. Referee: [Evaluation] Evaluation on the quadrotor and cartpole: the manuscript supplies no reachable-set computation details, quantitative results (e.g., set volumes, computation times, or safety margins), or comparison against baselines. This prevents verification that the method supports the central claim of feasible verification under the embedding.

    Authors: The referee is correct that the current evaluation provides only a high-level feasibility illustration without quantitative details. We will expand the evaluation section to include the specific reachable-set computation parameters (e.g., number of iterations, discretization settings), reported metrics such as reachable-set volumes and computation times for both the quadrotor and cartpole examples, and observed safety margins. We will also add a brief comparison against a baseline that assumes instantaneous optimal control to highlight the effect of the embedding. These additions will be included in the revised manuscript to better substantiate the claims. revision: yes

Circularity Check

0 steps flagged

No circularity: reachability method is an independent modeling choice

full rationale

The paper presents a reachability algorithm by explicitly modeling gradient descent iterations as a discrete dynamical system whose state is augmented with the control input and then composed with the continuous plant dynamics. This is introduced as a new design decision to enable verification of optimal controllers without solving the optimization exactly at runtime. No equations or claims in the provided abstract or description reduce a derived quantity to a fitted parameter, self-definition, or prior self-cited result by construction. The two evaluation examples (quadrotor, cartpole) are presented as feasibility checks on the modeling approach rather than as data used to fit or force the central construction. The derivation chain therefore remains self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The approach rests on standard assumptions of control theory and reachability analysis; no new free parameters, invented entities, or ad-hoc axioms are introduced in the abstract.

axioms (2)
  • domain assumption The continuous-time plant dynamics are known and Lipschitz continuous.
    Required for any reachability analysis of the combined system.
  • domain assumption Gradient descent iterations can be written as a discrete-time map whose state is finite-dimensional.
    Central modeling step stated in the abstract.

pith-pipeline@v0.9.0 · 5452 in / 1274 out tokens · 27032 ms · 2026-05-10T08:29:29.060185+00:00 · methodology

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

35 extracted references · 35 canonical work pages

  1. [1]

    Waymo: The World’s Most Experienced Driver,

    Waymo, “Waymo: The World’s Most Experienced Driver,” https://waymo.com/

    work page

  2. [2]

    V oloCity:The air taxi that’s a cut above,

    V oloCity, “V oloCity:The air taxi that’s a cut above,” https://www.volocopter.com/en/solutions/volocity

    work page

  3. [3]

    Serve robotics,

    S. Robotics, “Serve robotics,” https://www.serverobotics.com/, 2025, accessed: 2025-10-13

    work page 2025

  4. [4]

    Neural lander: Stable drone landing control using learned dynamics,

    G. Shi, X. Shi, M. O’Connell, R. Yu, K. Azizzadenesheli, A. Anand- kumar, Y . Yue, and S.-J. Chung, “Neural lander: Stable drone landing control using learned dynamics,” in2019 international conference on robotics and automation (icra). IEEE, 2019, pp. 9784–9790

    work page 2019

  5. [5]

    Available: https://arxiv.org/abs/2409.15610

    H. Xue, C. Pan, Z. Yi, G. Qu, and G. Shi, “Full-order sampling-based mpc for torque-level locomotion control via diffusion-style annealing,” arXiv preprint arXiv:2409.15610, 2024

    work page arXiv 2024

  6. [6]

    Autonomous drifting with 3 minutes of data via learned tire models,

    F. Djeumou, J. Y . Goh, U. Topcu, and A. Balachandran, “Autonomous drifting with 3 minutes of data via learned tire models,” in2023 IEEE International Conference on Robotics and Automation (ICRA). IEEE, 2023, pp. 968–974

    work page 2023

  7. [7]

    Set propagation techniques for reachability analysis,

    M. Althoff, G. Frehse, and A. Girard, “Set propagation techniques for reachability analysis,”Annual Review of Control, Robotics, and Autonomous Systems, vol. 4, pp. 369–395, 2021

    work page 2021

  8. [8]

    Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations,

    O. Botchkarev and S. Tripakis, “Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations,” inHybrid Systems: Computation and Control: Third International Workshop, HSCC 2000 Pittsburgh, PA, USA, March 23–25, 2000 Proceedings 3. Springer, 2000, pp. 73–88

    work page 2000

  9. [9]

    Computational techniques for hybrid system verification,

    A. Chutinan and B. H. Krogh, “Computational techniques for hybrid system verification,”IEEE Transactions on Automatic Control, vol. 48, no. 1, pp. 64–75, 2003

    work page 2003

  10. [10]

    Computing reachable sets of hybrid systems using a combination of zonotopes and polytopes,

    M. Althoff, O. Stursberg, and M. Buss, “Computing reachable sets of hybrid systems using a combination of zonotopes and polytopes,” Nonlinear Analysis: Hybrid Systems, vol. 4, no. 2, pp. 233–249, 2010

    work page 2010

  11. [11]

    Taylor models and other validated func- tional inclusion methods,

    K. Makino and M. Berz, “Taylor models and other validated func- tional inclusion methods,”International Journal of Pure and Applied Mathematics, vol. 6, pp. 239–316, 2003

    work page 2003

  12. [12]

    Taylor model flowpipe construction for non-linear hybrid systems,

    X. Chen, E. Abraham, and S. Sankaranarayanan, “Taylor model flowpipe construction for non-linear hybrid systems,” in2012 IEEE 33rd Real-Time Systems Symposium. IEEE, 2012, pp. 183–192

    work page 2012

  13. [13]

    Com- putational approaches to reachability analysis of stochastic hybrid systems,

    A. Abate, S. Amin, M. Prandini, J. Lygeros, and S. Sastry, “Com- putational approaches to reachability analysis of stochastic hybrid systems,” inInternational Workshop on Hybrid Systems: Computation and Control. Springer, 2007, pp. 4–17

    work page 2007

  14. [14]

    C2e2: A verification tool for stateflow models,

    P. S. Duggirala, S. Mitra, M. Viswanathan, and M. Potok, “C2e2: A verification tool for stateflow models,” inTACAS 2015, Held as Part of ETAPS 2015, London, UK, Proceedings 21. Springer, 2015, pp. 68–82

    work page 2015

  15. [15]

    dreal: An smt solver for nonlinear theories over the reals,

    S. Gao, S. Kong, and E. M. Clarke, “dreal: An smt solver for nonlinear theories over the reals,” in24th International Conference on Automated Deduction, Lake Placid, NY, USA Proceedings 24. Springer, 2013, pp. 208–214

    work page 2013

  16. [16]

    dreach:δ-reachability analysis for hybrid systems,

    S. Kong, S. Gao, W. Chen, and E. Clarke, “dreach:δ-reachability analysis for hybrid systems,” inTACAS 2015, Held as Part of ETAPS 2015, London, UK, April 11-18, 2015, Proceedings 21. Springer, 2015, pp. 200–205

    work page 2015

  17. [17]

    Spaceex: Scalable ver- ification of hybrid systems,

    G. Frehse, C. Le Guernic, A. Donz ´e, S. Cotton, R. Ray, O. Lebeltel, R. Ripado, A. Girard, T. Dang, and O. Maler, “Spaceex: Scalable ver- ification of hybrid systems,” inInternational Conference on Computer Aided Verification. Springer, 2011, pp. 379–395

    work page 2011

  18. [18]

    An Introduction to CORA 2015

    M. Althoff, “An Introduction to CORA 2015.”ARCH@ CPSWeek, vol. 34, pp. 120–151, 2015

    work page 2015

  19. [19]

    Baier and J.-P

    C. Baier and J.-P. Katoen,Principles of model checking. MIT press, 2008

    work page 2008

  20. [20]

    Hamilton- jacobi reachability: A brief overview and recent advances,

    S. Bansal, M. Chen, S. Herbert, and C. J. Tomlin, “Hamilton- jacobi reachability: A brief overview and recent advances,” in56th Conference on Decision and Control. IEEE, 2017, pp. 2242–2253

    work page 2017

  21. [21]

    Verisig: verifying safety properties of hybrid systems with neural network controllers,

    R. Ivanov, J. Weimer, R. Alur, G. J. Pappas, and I. Lee, “Verisig: verifying safety properties of hybrid systems with neural network controllers,” inProceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, 2019, pp. 169–178

    work page 2019

  22. [22]

    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

    work page 2019

  23. [23]

    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,” inProceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control. ACM, 2019, pp. 157–168

    work page 2019

  24. [24]

    Formal verification of neural network controlled autonomous systems,

    X. Sun, H. Khedr, and Y . Shoukry, “Formal verification of neural network controlled autonomous systems,” inProceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control. ACM, 2019, pp. 147–156

    work page 2019

  25. [25]

    Safety verification of cyber-physical systems with reinforcement learning control,

    H. Tran, F. Cai, D. M. Lopez, P. Musau, T. T. Johnson, and X. Koutsoukos, “Safety verification of cyber-physical systems with reinforcement learning control,”ACM Transactions on Embedded Computing Systems, vol. 18, no. 5s, p. 105, 2019

    work page 2019

  26. [26]

    Verifying the safety of autonomous systems with neural network controllers,

    R. Ivanov, T. J. Carpenter, J. Weimer, R. Alur, G. J. Pappas, and I. Lee, “Verifying the safety of autonomous systems with neural network controllers,”ACM Transactions on Embedded Computing Systems (TECS), vol. 20, no. 1, pp. 1–26, 2020

    work page 2020

  27. [27]

    Case study: verifying the safety of an autonomous racing car with a neural network controller,

    ——, “Case study: verifying the safety of an autonomous racing car with a neural network controller,” inProceedings of the 23rd Inter- national Conference on Hybrid Systems: Computation and Control, 2020, pp. 1–7

    work page 2020

  28. [28]

    Verisig 2.0: Verification of neural network controllers using taylor model preconditioning,

    ——, “Verisig 2.0: Verification of neural network controllers using taylor model preconditioning,” inInternational Conference on Com- puter Aided Verification. Springer, 2021, pp. 249–262

    work page 2021

  29. [29]

    Flow*: An analyzer for non-linear hybrid systems,

    X. Chen, E. ´Abrah´am, and S. Sankaranarayanan, “Flow*: An analyzer for non-linear hybrid systems,” inInt. Conference on Computer Aided Verification, 2013

    work page 2013

  30. [30]

    Tedrake,Underactuated Robotics: Algorithms for Walking, Running, Swimming, Flying, and Manipulation

    R. Tedrake,Underactuated Robotics: Algorithms for Walking, Running, Swimming, Flying, and Manipulation. Course Notes for MIT 6.832, 2023. [Online]. Available: https://underactuated.csail.mit. edu

    work page 2023

  31. [31]

    Neuronlike adaptive elements that can solve difficult learning control problems,

    A. G. Barto, R. S. Sutton, and C. W. Anderson, “Neuronlike adaptive elements that can solve difficult learning control problems,”IEEE Transactions on Systems, Man, and Cybernetics, vol. SMC-13, no. 5, pp. 834–846, 1983

    work page 1983

  32. [32]

    Correct equations for the dynamics of the cart- pole system,

    R. V . Florian, “Correct equations for the dynamics of the cart- pole system,”Center for Cognitive and Neural Studies (Coneural), Romania, vol. 63, 2007

    work page 2007

  33. [33]

    Suppression of the wrapping effect by taylor model-based verified integrators: Long-term stabilization by preconditioning,

    K. Makino and M. Berz, “Suppression of the wrapping effect by taylor model-based verified integrators: Long-term stabilization by preconditioning,”International Journal of Differential Equations and Applications, vol. 10, no. 4, pp. 353–384, 2005

    work page 2005

  34. [34]

    Shrink wrapping for taylor models revisited,

    F. B ¨unger, “Shrink wrapping for taylor models revisited,”Numerical Algorithms, vol. 78, no. 4, pp. 1001–1017, 2018

    work page 2018

  35. [35]

    Reachability analysis of non-linear hybrid systems using taylor models,

    X. Chen, “Reachability analysis of non-linear hybrid systems using taylor models,” Ph.D. dissertation, Fachgruppe Informatik, RWTH Aachen University, 2015

    work page 2015