pith. sign in

arxiv: 2605.25346 · v1 · pith:GRYHISA6new · submitted 2026-05-25 · 💻 cs.RO · cs.AI· cs.LG· cs.SY· eess.SY· math.OC

Parallel Differentiable Reachability for Learning and Planning with Certified Neural Dynamics and Controllers

Keyi Shen , Glen Chou This is my paper

Pith reviewed 2026-06-29 22:08 UTC · model grok-4.3

classification 💻 cs.RO cs.AIcs.LGcs.SYeess.SYmath.OC
keywords reachability analysisneural network dynamicscertified controldifferentiable programmingmodel predictive controlroboticsTaylor modelsbound propagation
0
0 comments X

The pith

A parallel differentiable reachability framework produces certified over-approximations for closed-loop neural dynamics and controllers.

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

The paper establishes a reachability framework that is both parallelizable on GPUs and differentiable through automatic differentiation. It achieves this by combining Taylor-model flowpipe construction with CROWN-style linear bound propagation inside a single representation that keeps affine dependencies intact. This setup supports certified reachable-set over-approximations for systems that include neural-network dynamics and controllers in both continuous and discrete time. A sympathetic reader would care because the method can be inserted directly into training loops and online planning pipelines while still supplying formal guarantees under bounded uncertainty.

Core claim

By unifying Taylor-model flowpipe construction with CROWN-style linear bound propagation in a representation that preserves affine dependencies, the framework computes certified reachable-set over-approximations that remain GPU-batched and support automatic differentiation, enabling certified training of dynamics models and controllers as well as reachability-aware sampling-based MPC with gradient refinement.

What carries the argument

The unified representation that preserves affine dependencies while supporting GPU-batched computation and automatic differentiation, which lets Taylor-model and CROWN-style propagation operate together on neural closed-loop systems.

If this is right

  • Certified training produces dynamics models and controllers that remain reachability-friendly.
  • Reachability-aware MPC performs sampling-based planning followed by gradient-based refinement while preserving certificates.
  • Online planning runs on non-prehensile manipulation and quadrotor tasks with hardware validation.
  • The same pipeline scales to systems with state dimension up to 72 while keeping certified over-approximations.

Where Pith is reading between the lines

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

  • The same primitive could be inserted into reinforcement-learning loops to optimize policies under explicit reachability constraints.
  • Tighter certificates might be obtained by swapping in other bound-propagation methods that also preserve affine dependencies.
  • The approach could be tested on systems whose uncertainty is not known to be bounded in advance.
  • Multi-robot coordination problems could use the batched computation to certify collective reachable sets.

Load-bearing premise

Uncertainty stays bounded and the chosen Taylor-model and linear-bound rules produce valid over-approximations for the neural dynamics and controllers that appear in the experiments.

What would settle it

A recorded trajectory of the true closed-loop system that leaves the computed reachable-set over-approximation while uncertainty remains inside the assumed bounds.

Figures

Figures reproduced from arXiv: 2605.25346 by Glen Chou, Keyi Shen.

Figure 1
Figure 1. Figure 1: Reachability-guided planning. We visualize three successful model predictive control (MPC) rollouts of our reachability-guided planner using certified, reachability-regularized models on (a) T-pushing, (b) T-pushing (Real-world) and (c) quadrotor. At each replanning step (indices shown), we plot the current state, the planned trajectory, and the certified reachable set under bounded disturbance (shaded foo… view at source ↗
Figure 2
Figure 2. Figure 2: Overview of the proposed framework. (a) Our parallel differentiable reachability engine unifies Taylor-model (TM) flowpipe propagation for analytical dynamics with CROWN-based neural bound propagation through a shared TM–CROWN interface, enabling GPU-batched and differentiable reachability analysis for continuous- and discrete-time systems. (b) The differentiable reachable sets are used to enable certified… view at source ↗
Figure 3
Figure 3. Figure 3: Benchmarking our JAX reachability tool. Top: Compared with DT CROWN reachability, our method achieves similar reachable-set volumes while being ≈100× faster. Bottom: Compared with CT immrax reachability, our method produces substantially tighter reachable sets with comparable runtime. where max(0, −G(·)) penalizes unsafe trajectories or large reachable sets, and C controls the penalty strength. Paralleliza… view at source ↗
Figure 4
Figure 4. Figure 4: Reachability on a coupled 6-quadrotor swarm. (a) Nominal trajectory. Quadrotors fly toward 6 different directions while coupled by spring-like attraction to the swarm center. (b) Dense sampled reachable set (under-approximation) under uncertainty. (c) Certified reachable set computed by our method. Our method produces a reasonable certified over-approximation. We also evaluate an acceleration-controlled 10… view at source ↗
Figure 5
Figure 5. Figure 5: Benchmarking certified training. Top: Across CT/DT systems and tasks, certified training maintains nominal performance comparable to naïve training. Bottom: Certified training produces substantially tighter reachable sets that more closely match sampled lower-bound volumes. (a) GT States under Uncertainty (b) Reachable Sets under Uncertainty DT Dyn (T pushing) CT Dyn (T pushing) CT Ctl (T pushing) DT Dyn (… view at source ↗
Figure 6
Figure 6. Figure 6: Certified training visualizations. Top: Rollouts from sampled initial states in X0 under the true dynamics or controller. Bottom: States sampled from the certified reachable sets closely overlap with the realizable trajectories [PITH_FULL_IMAGE:figures/full_fig_p009_6.png] view at source ↗
read the original abstract

Neural network (NN) dynamics models and control policies achieve strong performance in robotics, but providing sound guarantees under uncertainty remains difficult, especially for closed-loop NN systems. Existing reachability tools provide formal over-approximations, yet are often non-differentiable, overly conservative, or too slow for modern learning and online planning pipelines. To address this, we present a parallelizable, differentiable reachability framework in JAX for continuous- and discrete-time systems with analytical and NN-based dynamics and controllers. Our framework combines Taylor-model flowpipe construction with CROWN-style linear bound propagation through a unified representation that preserves affine dependencies while supporting GPU-batched computation and automatic differentiation. Building on this reachability primitive, we develop (i) a certified training method that encourages reachability-friendly dynamics models and controllers, and (ii) a reachability-aware sampling-based MPC scheme with gradient-based refinement. Experiments on non-prehensile manipulation and quadrotor tasks, including hardware and higher-dimensional evaluations (up to 72D), demonstrate practical online planning while maintaining certified reachable-set over-approximations under bounded uncertainty.

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 presents a parallelizable, differentiable reachability framework in JAX for continuous- and discrete-time systems with analytical and NN-based dynamics and controllers. It combines Taylor-model flowpipe construction with CROWN-style linear bound propagation through a unified representation that preserves affine dependencies, supports GPU-batched computation and automatic differentiation, and yields certified reachable-set over-approximations for closed-loop NN systems. This primitive is used to develop (i) a certified training method encouraging reachability-friendly models/controllers and (ii) a reachability-aware sampling-based MPC scheme with gradient-based refinement. Experiments on non-prehensile manipulation and quadrotor tasks (including hardware and up to 72D) demonstrate practical online planning while maintaining certified over-approximations under bounded uncertainty.

Significance. If the soundness of the unified representation holds, the framework would meaningfully bridge formal reachability tools with differentiable learning and planning pipelines in robotics. The GPU support, high-dimensional scaling, and hardware validation are concrete strengths. The work provides a practical primitive for certified training and MPC that existing non-differentiable or overly conservative tools do not directly supply.

major comments (2)
  1. [§3] §3 (unified representation): the claim that combining Taylor-model flowpipes with CROWN linear bounds preserves both soundness and affine dependencies for closed-loop NN systems requires an explicit inductive argument or lemma showing that the propagation rules remain valid over-approximations when the dynamics and controller are both NN-parameterized; without this, the central soundness guarantee for the training and MPC applications rests on an unverified assumption.
  2. [§5] §5 (experiments, 72D quadrotor): the reported online planning times and certification tightness are presented without an ablation isolating the contribution of the differentiable reachability primitive versus the sampling-based MPC baseline; this weakens the claim that the framework enables practical certified planning at scale.
minor comments (2)
  1. [§3] Notation for the unified affine representation (e.g., how Taylor coefficients and CROWN bounds are jointly stored) should be introduced with a single running example early in §3 to improve readability.
  2. [§4.2] The abstract and §4.2 refer to 'bounded uncertainty' without specifying the exact form (additive, parametric, or state-dependent); a short paragraph clarifying the uncertainty model assumed throughout would help.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive review and the recommendation for minor revision. We address each major comment below and will incorporate the requested additions into the revised manuscript.

read point-by-point responses

  1. Referee: [§3] §3 (unified representation): the claim that combining Taylor-model flowpipes with CROWN linear bounds preserves both soundness and affine dependencies for closed-loop NN systems requires an explicit inductive argument or lemma showing that the propagation rules remain valid over-approximations when the dynamics and controller are both NN-parameterized; without this, the central soundness guarantee for the training and MPC applications rests on an unverified assumption.

    Authors: We agree that an explicit inductive argument strengthens the central claim. In the revised manuscript we will insert a new lemma in §3 that proves soundness and preservation of affine dependencies by induction over time steps for the closed-loop case in which both the dynamics and the controller are neural networks. The argument composes the standard soundness of Taylor-model flowpipes with the soundness of CROWN-style linear bounds under the unified representation, showing that the over-approximation property is maintained at each propagation step. revision: yes

  2. Referee: [§5] §5 (experiments, 72D quadrotor): the reported online planning times and certification tightness are presented without an ablation isolating the contribution of the differentiable reachability primitive versus the sampling-based MPC baseline; this weakens the claim that the framework enables practical certified planning at scale.

    Authors: We acknowledge that an explicit ablation would better isolate the contribution of the differentiable reachability primitive. In the revised §5 we will add a controlled comparison on the 72D quadrotor task that reports planning times, certification tightness, and success rates for the full reachability-aware MPC versus the sampling-based baseline without the differentiable reachability component. revision: yes

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper introduces a unified differentiable reachability framework by combining Taylor-model flowpipe construction with CROWN-style linear bound propagation. The abstract and description present this as a novel engineering combination supporting GPU batching and autodiff, with downstream uses in certified training and MPC. No equations, fitted parameters, or self-citations are shown to reduce the central claims (sound over-approximations or performance) to inputs by construction. The validity of the over-approximations is explicitly conditioned on bounded uncertainty and the propagation rules, which is a standard soundness assumption rather than a definitional loop. The derivation chain is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The framework rests on the domain assumption of bounded uncertainty and the validity of Taylor-model and CROWN propagation for the NN architectures considered; no free parameters or invented entities are described in the abstract.

axioms (2)
  • domain assumption Uncertainty in initial states, disturbances, and model parameters remains within known bounds.
    Required for the over-approximations to be certified; stated in the abstract as 'under bounded uncertainty'.
  • domain assumption Taylor-model flowpipe construction and CROWN-style linear bound propagation remain valid when composed through the unified affine representation.
    Central to the soundness claim; invoked when the paper states the combination 'preserves affine dependencies'.

pith-pipeline@v0.9.1-grok · 5738 in / 1331 out tokens · 27479 ms · 2026-06-29T22:08:58.442102+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

73 extracted references · 21 canonical work pages · 5 internal anchors

  1. [1]

    An introduction to CORA 2015

    Matthias Althoff. An introduction to CORA 2015. In Proc. of the 1st and 2nd Workshop on Applied Verification for Continuous and Hybrid Systems, pages 120–151. EasyChair, December 2015. doi: 10.29007/zbkv. URL https://easychair.org/publications/paper/xMm

    work page doi:10.29007/zbkv 2015

  2. [2]

    Verified integration of odes and flows using differential algebraic methods on high-order taylor models.Reliable computing, 4(4): 361–369, 1998

    Martin Berz and Kyoko Makino. Verified integration of odes and flows using differential algebraic methods on high-order taylor models.Reliable computing, 4(4): 361–369, 1998

    1998

  3. [3]

    Victor Blomqvist. Pymunk. https://pymunk.org, Novem- ber 2022

    2022

  4. [4]

    Juliareach: a toolbox for set-based reachability

    Sergiy Bogomolov, Marcelo Forets, Goran Frehse, Kos- tiantyn Potomkin, and Christian Schilling. Juliareach: a toolbox for set-based reachability. InProceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pages 39–44, 2019

    2019

  5. [5]

    JAX: composable transformations of Python+NumPy programs, 2018

    James Bradbury, Roy Frostig, Peter Hawkins, Matthew James Johnson, Chris Leary, Dougal Maclaurin, George Necula, Adam Paszke, Jake VanderPlas, Skye Wanderman-Milne, and Qiao Zhang. JAX: composable transformations of Python+NumPy programs, 2018. URL http://github.com/jax-ml/jax

    2018

  6. [6]

    The fifth international verification of neural networks competition (vnn-comp 2024): Summary and results.arXiv preprint arXiv:2412.19985, 2024

    Christopher Brix, Stanley Bak, Taylor T Johnson, and Haoze Wu. The fifth international verification of neural networks competition (vnn-comp 2024): Summary and results.arXiv preprint arXiv:2412.19985, 2024

    work page arXiv 2024

  7. [7]

    Rudy Bunel, Ilker Turkaslan, Philip H. S. Torr, Pushmeet Kohli, and M. Pawan Kumar. A unified view of piecewise linear neural network verification. InAdvances in Neural Information Processing Systems (NeurIPS), 2018

    2018

  8. [8]

    PhD thesis, Fachgruppe Informatik, RWTH Aachen University, 2015

    Xin Chen.Reachability analysis of non-linear hybrid systems using taylor models. PhD thesis, Fachgruppe Informatik, RWTH Aachen University, 2015

    2015

  9. [9]

    Decomposed reachability analysis for nonlinear systems

    Xin Chen and Sriram Sankaranarayanan. Decomposed reachability analysis for nonlinear systems. In2016 IEEE Real-Time Systems Symposium (RTSS), pages 13–24. IEEE, 2016

    2016

  10. [10]

    Taylor model flowpipe construction for non-linear hy- brid systems

    Xin Chen, Erika Abraham, and Sriram Sankaranarayanan. Taylor model flowpipe construction for non-linear hy- brid systems. In2012 IEEE 33rd Real-Time Systems Symposium, pages 183–192. IEEE, 2012

    2012

  11. [11]

    Flow*: An analyzer for non-linear hybrid systems

    Xin Chen, Erika Ábrahám, and Sriram Sankaranarayanan. Flow*: An analyzer for non-linear hybrid systems. In International Conference on Computer Aided Verification, pages 258–263. Springer, 2013

    2013

  12. [12]

    Diffusion policy: Visuomotor policy learning via action diffusion.The International Journal of Robotics Research, 44(10-11):1684–1704, 2025

    Cheng Chi, Zhenjia Xu, Siyuan Feng, Eric Cousineau, Yilun Du, Benjamin Burchfiel, Russ Tedrake, and Shuran Song. Diffusion policy: Visuomotor policy learning via action diffusion.The International Journal of Robotics Research, 44(10-11):1684–1704, 2025

    2025

  13. [13]

    Model error propagation via learned contraction metrics for safe feedback motion planning of unknown systems

    Glen Chou, Necmiye Ozay, and Dmitry Berenson. Model error propagation via learned contraction metrics for safe feedback motion planning of unknown systems. In2021 60th IEEE Conference on Decision and Control (CDC), pages 3576–3583. IEEE, 2021

    2021

  14. [14]

    Safe output feedback motion planning from images via learned perception modules and contraction theory

    Glen Chou, Necmiye Ozay, and Dmitry Berenson. Safe output feedback motion planning from images via learned perception modules and contraction theory. InInter- national Workshop on the Algorithmic Foundations of Robotics, pages 349–367. Springer, 2022

    2022

  15. [15]

    Visual Foresight: Model-Based Deep Reinforcement Learning for Vision-Based Robotic Control

    Frederik Ebert, Chelsea Finn, Sudeep Dasari, Annie Xie, Alex Lee, and Sergey Levine. Visual foresight: Model-based deep reinforcement learning for vision-based robotic control.arXiv preprint arXiv:1812.00568, 2018

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  16. [16]

    Zico Kolter Eric Wong

    J. Zico Kolter Eric Wong. Provable defenses against adversarial examples via the convex outer adversarial polytope. InInternational Conference on Machine Learning (ICML), 2018

    2018

  17. [17]

    Unsupervised Learning for Physical Interaction through Video Prediction

    Chelsea Finn, Ian Goodfellow, and Sergey Levine. Unsu- pervised learning for physical interaction through video prediction.arXiv preprint arXiv:1605.07157, 2016

    work page internal anchor Pith review Pith/arXiv arXiv 2016

  18. [18]

    jax_verify: Neural network verifi- cation in jax

    Google DeepMind. jax_verify: Neural network verifi- cation in jax. https://github.com/google-deepmind/jax_ verify, 2020. GitHub repository

    2020

  19. [19]

    On the effectiveness of interval bound propagation for training verifiably robust models.Proceedings of the IEEE International Confer- ence on Computer Vision (ICCV), 2019

    Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Timothy Mann, and Pushmeet Kohli. On the effectiveness of interval bound propagation for training verifiably robust models.Proceedings of the IEEE International Confer- ence on Computer Vision (ICCV), 2019

    2019

  20. [20]

    Gotube: Scalable statistical verification of continuous-depth models

    Sophie A Gruenbacher, Mathias Lechner, Ramin Hasani, Daniela Rus, Thomas A Henzinger, Scott A Smolka, and Radu Grosu. Gotube: Scalable statistical verification of continuous-depth models. InProceedings of the AAAI Conference on Artificial Intelligence, volume 36, pages 6755–6764, 2022

    2022

  21. [21]

    Dream to Control: Learning Behaviors by Latent Imagination

    Danijar Hafner, Timothy Lillicrap, Jimmy Ba, and Mo- hammad Norouzi. Dream to control: Learning behaviors by latent imagination.arXiv preprint arXiv:1912.01603, 2019

    work page internal anchor Pith review Pith/arXiv arXiv 1912

  22. [22]

    immrax: A parallelizable and differentiable tool- box for interval analysis and mixed monotone reachability in jax.IFAC-PapersOnLine, 58(11):75–80, 2024

    Akash Harapanahalli, Saber Jafarpour, and Samuel Coogan. immrax: A parallelizable and differentiable tool- box for interval analysis and mixed monotone reachability in jax.IFAC-PapersOnLine, 58(11):75–80, 2024

    2024

  23. [23]

    Fastrack: A modular framework for fast and guaranteed safe motion planning

    Sylvia L Herbert, Mo Chen, SooJean Han, Somil Bansal, Jaime F Fisac, and Claire J Tomlin. Fastrack: A modular framework for fast and guaranteed safe motion planning. In2017 IEEE 56th Annual Conference on Decision and Control (CDC), pages 1517–1522. IEEE, 2017

    2017

  24. [24]

    Polar: A polynomial arithmetic framework for verifying neural-network controlled systems

    Chao Huang, Jiameng Fan, Xin Chen, Wenchao Li, and Qi Zhu. Polar: A polynomial arithmetic framework for verifying neural-network controlled systems. In International Symposium on Automated Technology for Verification and Analysis, pages 414–430. Springer, 2022

    2022

  25. [25]

    Training certifiably robust neural networks with efficient local lipschitz bounds.Advances in Neural Information Processing Systems, 34:22745–22757, 2021

    Yujia Huang, Huan Zhang, Yuanyuan Shi, J Zico Kolter, and Anima Anandkumar. Training certifiably robust neural networks with efficient local lipschitz bounds.Advances in Neural Information Processing Systems, 34:22745–22757, 2021

    2021

  26. [26]

    The 6th international verification of neural networks competition (vnn-comp 2025): Summary and results

    Konstantin Kaulen, Tobias Ladner, Stanley Bak, Christo- pher Brix, Hai Duong, Thomas Flinkow, Taylor T Johnson, Lukas Koller, Edoardo Manino, ThanhVu H Nguyen, et al. The 6th international verification of neural networks competition (vnn-comp 2025): Summary and results. arXiv preprint arXiv:2512.19007, 2025

    work page arXiv 2025

  27. [27]

    PhD thesis, University of Oxford, 2021

    Patrick Kidger.On Neural Differential Equations. PhD thesis, University of Oxford, 2021

    2021

  28. [28]

    Planning with learned dynamics: Probabilis- tic guarantees on safety and reachability via lipschitz constants.IEEE Robotics and Automation Letters, 6(3): 5129–5136, 2021

    Craig Knuth, Glen Chou, Necmiye Ozay, and Dmitry Berenson. Planning with learned dynamics: Probabilis- tic guarantees on safety and reachability via lipschitz constants.IEEE Robotics and Automation Letters, 6(3): 5129–5136, 2021

    2021

  29. [29]

    Statistical safety and robustness guarantees for feedback motion planning of unknown underactuated stochastic systems.arXiv preprint arXiv:2212.06874, 2022

    Craig Knuth, Glen Chou, Jamie Reese, and Joe Moore. Statistical safety and robustness guarantees for feedback motion planning of unknown underactuated stochastic systems.arXiv preprint arXiv:2212.06874, 2022

    work page arXiv 2022

  30. [30]

    End-to-end training of deep visuomotor policies

    Sergey Levine, Chelsea Finn, Trevor Darrell, and Pieter Abbeel. End-to-end training of deep visuomotor policies. Journal of Machine Learning Research, 17(39):1–40, 2016

    2016

  31. [31]

    Neural contraction metrics with formal guarantees for discrete-time nonlinear dynamical systems.arXiv preprint arXiv:2504.17102, 2025

    Haoyu Li, Xiangru Zhong, Bin Hu, and Huan Zhang. Neural contraction metrics with formal guarantees for discrete-time nonlinear dynamical systems.arXiv preprint arXiv:2504.17102, 2025

    work page arXiv 2025

  32. [32]

    Two-stage learning of stabilizing neural controllers via zubov sampling and iterative domain expansion.arXiv preprint arXiv:2506.01356, 2025

    Haoyu Li, Xiangru Zhong, Bin Hu, and Huan Zhang. Two-stage learning of stabilizing neural controllers via zubov sampling and iterative domain expansion.arXiv preprint arXiv:2506.01356, 2025

    work page arXiv 2025

  33. [33]

    Learning Particle Dynamics for Manipulating Rigid Bodies, Deformable Objects, and Fluids

    Yunzhu Li, Jiajun Wu, Russ Tedrake, Joshua B Tenen- baum, and Antonio Torralba. Learning particle dynamics for manipulating rigid bodies, deformable objects, and fluids.arXiv preprint arXiv:1810.01566, 2018

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  34. [34]

    Kochenderfer

    Changliu Liu, Tomer Arnon, Christopher Lazarus, Christo- pher Strong, Clark Barrett, and Mykel J. Kochenderfer. Algorithms for verifying deep neural networks.Founda- tions and Trends® in Optimization, 4(3-4), 2021

    2021

  35. [35]

    Safe control under input limits with neural control barrier functions

    Simin Liu, Changliu Liu, and John Dolan. Safe control under input limits with neural control barrier functions. In Conference on Robot Learning, pages 1970–1980, 2023

    1970

  36. [36]

    Nnv 2.0: The neural network verification tool

    Diego Manzanas Lopez, Sung Woo Choi, Hoang-Dung Tran, and Taylor T Johnson. Nnv 2.0: The neural network verification tool. InInternational Conference on Computer Aided Verification, pages 397–412. Springer, 2023

    2023

  37. [37]

    Arch-comp24 category report: Artificial intelligence and neural network control systems (ainncs) for continuous and hybrid systems plants

    Diego Manzanas Lopez, Matthias Althoff, Luis Benet, Clemens Blab, Marcelo Forets, Yuhao Jia, Taylor T Johnson, Manuel Kranzl, Tobias Ladner, Lukas Linauer, Philipp Neubauer, Sophie Neubauer, Christian Schilling, Huan Zhang, and Xiangru Zhong. Arch-comp24 category report: Artificial intelligence and neural network control systems (ainncs) for continuous an...

    work page doi:10.29007/mxld 2024

  38. [38]

    Pawan Kumar

    Jingyue Lu and M. Pawan Kumar. Neural network branching for neural network verification. InInternational Conference on Learning Representations (ICLR), 2020

    2020

  39. [39]

    Multirotor aerial vehicles: Modeling, estimation, and control of quadrotor.IEEE Robotics & Automation Magazine, 19 (3):20–32, 2012

    Robert Mahony, Vijay Kumar, and Peter Corke. Multirotor aerial vehicles: Modeling, estimation, and control of quadrotor.IEEE Robotics & Automation Magazine, 19 (3):20–32, 2012. doi: 10.1109/MRA.2012.2206474

    work page doi:10.1109/mra.2012.2206474 2012

  40. [40]

    Funnel libraries for real-time robust feedback motion planning.The International Journal of Robotics Research, 36(8):947– 982, 2017

    Anirudha Majumdar and Russ Tedrake. Funnel libraries for real-time robust feedback motion planning.The International Journal of Robotics Research, 36(8):947– 982, 2017

    2017

  41. [41]

    Keypoints into the future: Self-supervised correspondence in model-based reinforcement learning

    Lucas Manuelli, Yunzhu Li, Pete Florence, and Russ Tedrake. Keypoints into the future: Self-supervised correspondence in model-based reinforcement learning. arXiv preprint arXiv:2009.05085, 2020

    work page arXiv 2009

  42. [42]

    Arch-comp24 category report: Artificial intelligence and neural network control systems (ainncs) for continuous and hybrid systems plants

    Diego Manzanas_Lopez, Matthias Althoff, Luis Benet, Clemens Blab, Marcelo Forets, Yuhao Jia, Taylor T John- son, Manuel Kranzl, Tobias Ladner, Lukas Linauer, et al. Arch-comp24 category report: Artificial intelligence and neural network control systems (ainncs) for continuous and hybrid systems plants. 2024

    2024

  43. [43]

    Springer Science & Business Media, 2013

    Reuven Y Rubinstein and Dirk P Kroese.The cross- entropy method: a unified approach to combinatorial op- timization, Monte-Carlo simulation and machine learning. Springer Science & Business Media, 2013

    2013

  44. [44]

    A convex relaxation barrier to tight robustness verification of neural networks

    Hadi Salman, Greg Yang, Huan Zhang, Cho-Jui Hsieh, and Pengchuan Zhang. A convex relaxation barrier to tight robustness verification of neural networks. InAdvances in Neural Information Processing Systems (NeurIPS), 2019

    2019

  45. [45]

    Safe domains of attraction for discrete-time nonlinear systems: Characterization and verifiable neural network estimation

    Mohamed Serry, Haoyu Li, Ruikun Zhou, Huan Zhang, and Jun Liu. Safe domains of attraction for discrete-time nonlinear systems: Characterization and verifiable neural network estimation. In2025 IEEE 64th Conference on Decision and Control (CDC), pages 5774–5781, 2025. doi: 10.1109/CDC57313.2025.11312100

    work page doi:10.1109/cdc57313.2025.11312100 2025

  46. [46]

    Bab-nd: Long-horizon motion planning with branch-and-bound and neural dynamics.arXiv preprint arXiv:2412.09584, 2024

    Keyi Shen, Jiangwei Yu, Jose Barreiros, Huan Zhang, and Yunzhu Li. Bab-nd: Long-horizon motion planning with branch-and-bound and neural dynamics.arXiv preprint arXiv:2412.09584, 2024

    work page arXiv 2024

  47. [47]

    Robocraft: Learning to see, simulate, and shape elasto-plastic objects with graph networks.arXiv preprint arXiv:2205.02909, 2022

    Haochen Shi, Huazhe Xu, Zhiao Huang, Yunzhu Li, and Jiajun Wu. Robocraft: Learning to see, simulate, and shape elasto-plastic objects with graph networks.arXiv preprint arXiv:2205.02909, 2022

    work page arXiv 2022

  48. [48]

    Robocook: Long-horizon elasto-plastic object manipulation with diverse tools, 2023

    Haochen Shi, Huazhe Xu, Samuel Clarke, Yunzhu Li, and Jiajun Wu. Robocook: Long-horizon elasto-plastic object manipulation with diverse tools, 2023

    2023

  49. [49]

    Certified Training with Branch-and-Bound for Lyapunov-stable Neural Control

    Zhouxing Shi, Haoyu Li, Cho-Jui Hsieh, and Huan Zhang. Certified training with branch-and-bound for lyapunov- stable neural control, 2026. URL https://arxiv.org/abs/ 2411.18235

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  50. [50]

    An abstract domain for certifying neural networks.Proceedings of the ACM on Programming Languages (POPL), 2019

    Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certifying neural networks.Proceedings of the ACM on Programming Languages (POPL), 2019

    2019

  51. [51]

    Robust tracking with model mismatch for fast and safe planning: an sos optimization approach

    Sumeet Singh, Mo Chen, Sylvia L Herbert, Claire J Tomlin, and Marco Pavone. Robust tracking with model mismatch for fast and safe planning: an sos optimization approach. InInternational Workshop on the Algorithmic Foundations of Robotics, pages 545–564. Springer, 2018

    2018

  52. [52]

    Robust feedback motion planning via contraction theory.The International Journal of Robotics Research, 42(9):655–688, 2023

    Sumeet Singh, Benoit Landry, Anirudha Majumdar, Jean- Jacques Slotine, and Marco Pavone. Robust feedback motion planning via contraction theory.The International Journal of Robotics Research, 42(9):655–688, 2023

    2023

  53. [53]

    How to train your neural control barrier function: Learning safety filters for complex input-constrained systems

    Oswin So, Zachary Serlin, Makai Mann, Jake Gonzales, Kwesi Rutledge, Nicholas Roy, and Chuchu Fan. How to train your neural control barrier function: Learning safety filters for complex input-constrained systems. In 2024 IEEE International Conference on Robotics and Automation (ICRA), pages 11532–11539. IEEE, 2024

    2024

  54. [54]

    Safety beyond the training data: Robust out-of-distribution mpc via conformalized system level synthesis.arXiv preprint arXiv:2602.12047, 2026

    Anutam Srinivasan, Antoine Leeman, and Glen Chou. Safety beyond the training data: Robust out-of-distribution mpc via conformalized system level synthesis.arXiv preprint arXiv:2602.12047, 2026

    work page arXiv 2026

  55. [55]

    Evaluat- ing robustness of neural networks with mixed integer programming, 2019

    Vincent Tjeng, Kai Xiao, and Russ Tedrake. Evaluat- ing robustness of neural networks with mixed integer programming, 2019

    2019

  56. [56]

    Nnv: the neu- ral network verification tool for deep neural networks and learning-enabled cyber-physical systems

    Hoang-Dung Tran, Xiaodong Yang, Diego Man- zanas Lopez, Patrick Musau, Luan Viet Nguyen, Weiming Xiang, Stanley Bak, and Taylor T Johnson. Nnv: the neu- ral network verification tool for deep neural networks and learning-enabled cyber-physical systems. InInternational conference on computer aided verification, pages 3–17. Springer, 2020

    2020

  57. [57]

    Efficient formal safety analysis of neural networks

    Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Efficient formal safety analysis of neural networks. InAdvances in Neural Information Processing Systems (NeurIPS), 2018

    2018

  58. [58]

    Beta-crown: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network robustness veri- fication

    Shiqi Wang, Huan Zhang, Kaidi Xu, Suman Jana, Xue Lin, Cho-Jui Hsieh, and Zico Kolter. Beta-crown: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network robustness veri- fication. InAdvances in Neural Information Processing Systems (NeurIPS), 2021

    2021

  59. [59]

    Dynamic-Resolution Model Learning for Object Pile Manipulation

    Yixuan Wang, Yunzhu Li, Katherine Driggs-Campbell, Li Fei-Fei, and Jiajun Wu. Dynamic-Resolution Model Learning for Object Pile Manipulation. InProceedings of Robotics: Science and Systems, Daegu, Republic of Korea, July 2023. doi: 10.15607/RSS.2023.XIX.047

    work page doi:10.15607/rss.2023.xix.047 2023

  60. [60]

    Yixuan Wang, Weichao Zhou, Jiameng Fan, Zhilu Wang, Jiajun Li, Xin Chen, Chao Huang, Wenchao Li, and Qi Zhu. Polar-express: Efficient and precise formal reacha- bility analysis of neural-network controlled systems.IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 43(3):994–1007, 2023

    2023

  61. [61]

    Model predictive path integral control: From theory to parallel computation.Journal of Guidance, Control, and Dynamics, 40(2):344–357, 2017

    Grady Williams, Andrew Aldrich, and Evangelos A Theodorou. Model predictive path integral control: From theory to parallel computation.Journal of Guidance, Control, and Dynamics, 40(2):344–357, 2017

    2017

  62. [62]

    Verified safe reinforcement learning for neural network dynamic models, 2024

    Junlin Wu, Huan Zhang, and Yevgeniy V orobeychik. Verified safe reinforcement learning for neural network dynamic models, 2024. URL https://arxiv.org/abs/2405. 15994

    2024

  63. [63]

    Daydreamer: World models for physical robot learning

    Philipp Wu, Alejandro Escontrela, Danijar Hafner, Pieter Abbeel, and Ken Goldberg. Daydreamer: World models for physical robot learning. InConference on Robot Learning, pages 2226–2240. PMLR, 2023

    2023

  64. [64]

    Automatic perturbation analysis for scalable certified robustness and beyond.Advances in Neural Information Processing Systems (NeurIPS), 2020

    Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai- Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh. Automatic perturbation analysis for scalable certified robustness and beyond.Advances in Neural Information Processing Systems (NeurIPS), 2020

    2020

  65. [65]

    Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh. Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers.International Conference on Learning Representations (ICLR), 2021

    2021

  66. [66]

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

    Lujie Yang, Hongkai Dai, Zhouxing Shi, Cho-Jui Hsieh, Russ Tedrake, and Huan Zhang. Lyapunov-stable neural control for state and output feedback: A novel formulation. arXiv preprint arXiv:2404.07956, 2024

    work page arXiv 2024

  67. [67]

    Optimization based planner–tracker design for safety guarantees

    He Yin, Monimoy Bujarbaruah, Murat Arcak, and Andrew Packard. Optimization based planner–tracker design for safety guarantees. In2020 American Control Conference (ACC), pages 5194–5200. IEEE, 2020

    2020

  68. [68]

    Exact verification of relu neural control barrier functions.Advances in neural information processing systems, 36:5685–5705, 2023

    Hongchao Zhang, Junlin Wu, Yevgeniy V orobeychik, and Andrew Clark. Exact verification of relu neural control barrier functions.Advances in neural information processing systems, 36:5685–5705, 2023

    2023

  69. [69]

    Efficient neural network robustness certification with general activation functions

    Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. InAdvances in Neural Information Processing Systems (NeurIPS), 2018

    2018

  70. [70]

    Towards stable and efficient training of verifiably robust neural networks.arXiv preprint arXiv:1906.06316, 2019

    Huan Zhang, Hongge Chen, Chaowei Xiao, Sven Gowal, Robert Stanforth, Bo Li, Duane Boning, and Cho-Jui Hsieh. Towards stable and efficient training of verifiably robust neural networks.arXiv preprint arXiv:1906.06316, 2019

    work page arXiv 1906

  71. [71]

    Gen- eral cutting planes for bound-propagation-based neural network verification.Advances in Neural Information Processing Systems, 2022

    Huan Zhang, Shiqi Wang, Kaidi Xu, Linyi Li, Bo Li, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. Gen- eral cutting planes for bound-propagation-based neural network verification.Advances in Neural Information Processing Systems, 2022

    2022

  72. [72]

    A branch and bound framework for stronger adversarial attacks of ReLU networks

    Huan Zhang, Shiqi Wang, Kaidi Xu, Yihan Wang, Suman Jana, Cho-Jui Hsieh, and Zico Kolter. A branch and bound framework for stronger adversarial attacks of ReLU networks. InInternational Conference on Machine Learning (ICML), pages 26591–26604. PMLR, 2022

    2022

  73. [73]

    Crown- reach: A reachability analysis tool for neural network con- trolled systems

    Xiangru Zhong, Yuhao Jia, and Huan Zhang. Crown- reach: A reachability analysis tool for neural network con- trolled systems. https://github.com/Verified-Intelligence/ CROWN-Reach, 2024. GitHub repository, accessed January 30, 2026. Algorithm 3Reachability of CT Dynamics with TM Flowpipe. Comments are in brown. 1: Inputs:dynamics fct,dyn (analytical or NN...

    2024