Pith. sign in

REVIEW 4 major objections 6 minor 47 references

Verification of Visual Controllers via Compositional Geometric Transformations

T0 review · 4 major / 6 minor · reviewed 2026-08-06 · deepseek-v4-flash

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

Pith's one-line read This paper shows that outer approximations of reachable states for vision-based neural controllers can be computed soundly by bounding each moving object's image appearance separately and recomposing the bounds through alpha blending…

desk verdict Genuinely new pipeline for per-entity geometric verification, but the central soundness claim is asserted rather than proven and never checked against the actual renderer. read the letter →

arxiv 2507.04523 v1 pith:RTQVEJOS submitted 2025-07-06 cs.RO cs.LG

Alexander Estornell , Leonard Jung , Michael Everett This is my paper
classification cs.ROcs.LG
keywords reachabilityanalysisneuralnetworkverificationperception-basedcontrolgeometrictransformationsalphacompositingclosed-loopsystemsimage-basedcontrollerslinearrelaxationbounds
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 claims that closed-loop safety verification of controllers that act directly on camera images can be made sound under realistic, low-dimensional visual uncertainties, rather than only under pixel-level $\ell^p$ noise. The proposed method decomposes a scene into movable entities, bounds each entity's image appearance under its own rotation, translation, or scaling using geometric transformations, and $\alpha$-composites those per-entity bounds into pixel-wise linear bounds on the full observation. It then feeds those image bounds through a neural-network verifier and a dynamics model to produce outer approximations of the set of future states reachable from an initial state set. The value of the claim is that state-space verification tools, which normally require the controller to see the state, can now certify controllers that never touch the state.

What carries the argument

The load-bearing object is the compositional scene model of Eq. (7): each entity $i$ has a fixed mask $\alpha_i$, a template image $Y_i$, and a state-dependent geometric transformation $I_{\mu_i(x)}$; the full observation is the $\alpha$-composited blend $Y = Y_0 \prod_i(1-I_{\mu_i}(\alpha_i))+\sum_i I_{\mu_i}(\alpha_i)I_{\mu_i}(Y_i)\prod_{j>i}(1-I_{\mu_j}(\alpha_j))$. Around this model the pipeline applies (i) DeepG-style sampling-based bound refinement to obtain per-entity pixel-wise affine bounds on $I_{\mu_i}(Y_i)$ and $I_{\mu_i}(\alpha_i)$ over the latent parameter range $\mu(X_t)$, and (ii) a custom CROWN-style linear relaxation that consumes precomputed affine bounds rather than raw input sets, thereby relaxing the blended observation and then the controller-dynamics composition. The work this machinery does is to convert a high-dimensional image-rendering uncertainty into low-dimensional parameter bounds that off-the-shelf state-space reachability tools can consume.

What would settle it

Render a grid of true states inside a chosen initial range using the actual Gym renderer, compute the paper's pixel bounds for that range, and check whether every rendered image lies inside the bounds; any violation shows the certificate applies to the modeled observation, not the real one. Alternatively, sample many closed-loop rollouts from $X_t$ and test whether any sampled state ever leaves the computed $\bar{R}_T$.

Watch

Extended reading notes

Core claim

The central claim is that the one-step reachable set $\bar{R}_1(X_t)$ of the closed-loop system $x_{t+1}=f(x_t,\pi_\theta(o(x_t)))$ can be soundly outer-approximated even when $o$ is a renderer and $\pi_\theta$ consumes only images. The paper proves this by showing that when the observation process is modeled as per-entity geometric transformations composed through $\alpha$ blending, Eq. (7), the observation bounds $[\underline{Y},\overline{Y}]$ are valid affine bounds on $o(X_t)$, that propagating them through the controller yields valid control bounds $[\underline{u},\overline{u}]$, and that propagating state and control bounds through the dynamics yields a polytope containing all true next states. Repeating this step gives outer bounds for arbitrary horizons. The authors state this as formal guarantees of soundness, with the caveat that the guarantees are relative to the assumed observation model.

Load-bearing premise

The soundness of the reachable-set certificate depends on the real observation process being exactly captured by the paper's model: known per-entity masks, known state-to-transformation maps, and alpha compositing over fixed entity templates; the paper does not validate this model against the Gym renderers used in the experiments.

Editorial extensions

If this is right

  • A controller that never observes the state can be certified over a horizon using only state-range information available at training or simulation time, so safety certificates become possible for pixels-to-torques policies.
  • Different objects in a scene can move under different transformations at once, covering settings like a two-link arm where one joint rotates and the other translates, which whole-image transformation methods cannot capture.
  • The bounds are constructive: the same pipeline yields pixel-level observation bounds that can be visualized, so a user can see which image regions drive looseness in the reachable set.
  • Larger image resolution and longer horizons degrade tightness, so the method trades image fidelity against certificate usefulness in a predictable way.
  • Because the pipeline composes with any LiRPA-compatible controller and dynamics graph, improvements in neural-network verifiers directly tighten the resulting reachable sets.

Reading between the lines

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

  • A natural testable extension is to validate the assumed compositing model against a real renderer: if the pixel bounds from Eq. (7) fail to contain true rendered pixels for sampled states, the certificate is for a different observation process, and the paper's soundness claim should be read as conditional on that model match.
  • The same alpha-compositing construction could be adapted to handle occlusions or depth ordering by treating the mask ordering as an additional uncertainty parameter, which the current fixed-order composition does not allow.
  • One could invert the pipeline and train controllers to minimize the width of $\bar{R}_1$, effectively using the verifier's slacks as a loss term, since the image bounds are differentiable functions of the masks and transformation parameters.
  • The slackness metric used in Section IV measures distance to sampled states rather than true reachable-set volume; reporting volume or inclusion tests for the next state would give a more direct certificate-quality measure.
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

4 major / 6 minor

Summary. The paper proposes a two-stage pipeline for verifying perception-based neural-network controllers under entity-specific geometric perturbations. In the first stage, a scene is decomposed into entities, each with a mask and a state-dependent geometric transformation; DeepG is used to obtain affine pixel bounds on each transformed entity, and a "modified CROWN" is said to compose these bounds through the alpha-blending model in Eq. (7) into pixel-wise bounds on the observation. In the second stage, these image bounds are propagated through the controller and dynamics to produce an outer bound on the one-step reachable set, with multi-step bounds obtained by iteration. Experiments on CartPole, Pendulum, and Acrobot display reachable-set bounds, slackness measurements, and runtimes.

Significance. If the soundness claim were established, this would be a valuable contribution: it connects state-space reachability analysis to vision-based controllers under structured geometric uncertainty and avoids vacuous pixel-space bounds by using DeepG. The entity-level compositional bounding idea is interesting, and the reported runtimes in Table I suggest practical scalability. However, the paper does not prove its central soundness claim, and the experimental section does not validate the assumed observation model against the actual renderers. As submitted, the contribution is a promising framework rather than a verified method.

major comments (4)
  1. [Section III-C / Contribution 3] The central soundness claim is asserted but not proven. No theorem in the paper states that Algorithm 1's output satisfies {f(x, \pi_\theta(o(x))) : x \in X_t} \subseteq [x', x']; the only quoted results are Theorem II.1 and Theorem II.3 from prior work. The "modified CROWN" introduced in Section III-B is described only in words, so the soundness of propagating precomputed affine bounds through the bilinear blending in Eq. (7) and through \pi_\theta is not established.
  2. [Section III-A, Eqs. (4)-(7)] The outer-approximation guarantee is for a hand-authored alpha-compositing model, not for the actual observation process o in Eq. (1). The paper never validates that Gym's renderer produces images inside [Y, \bar{Y}] for x \in X_t, nor does it state a theorem that the renderer equals Eq. (7). Antialiasing, lighting, background, and composition order can move pixels outside the model bounds, so \bar{R}_1(X_t) may not contain the true reachable set. The limitations section (Section VI) lists state-dependence and entity decomposability but not this renderer-model mismatch.
  3. [Section IV.D, Eq. (10)] The slackness experiments do not test soundness. The metric measures the distance from sampled states to the bounds but does not report whether every sampled state is contained in the bounds, and sampling cannot establish containment for all states. Since these experiments are the only empirical evidence connecting the abstract model to the real renderer, the soundness claim remains unverified.
  4. [Section III-B] The method for composing per-entity DeepG bounds into a bound on Eq. (7) is underspecified. The alpha and RGB channels for the same entity are correlated through the same \mu_i, but the paper does not state how the products I_{\mu_i}(\alpha_i) \cdot I_{\mu_i}(Y_i) and the products over (1 - I_{\mu_j}(\alpha_j)) are relaxed, nor why the result is an outer bound. Without this specification, the pipeline is not reproducible and the claimed guarantee cannot be checked.
minor comments (6)
  1. [Section III-A] After Eq. (5), "gives the initial latent state rage" should be "range".
  2. [Section II-A, Eq. (2)] Eq. (2) is missing a closing brace: it reads R_1(X_t) \triangleq \{x_{t+1} | x_{t+1} = f(x_t, \pi_\theta(o(x_t))\}.
  3. [Section III-A] The phrase "we consider only spatial transformations without loss of generality" should be justified; dropping brightness and contrast is a restriction unless they are shown to be subsumed.
  4. [Algorithm 1] Algorithm 1 uses the notation {I_i}_0^k, while the text refers to n entities; the relationship between k and n should be defined consistently.
  5. [Table I] Table I would benefit from a statement of the measurement protocol (e.g., number of runs, variance, and whether times are per observation bound or per full pipeline).
  6. [Section IV.B] The sentence "The CartPole reachable sets overlap more than other systems" is unclear; specify whether the overlap is across time steps, across sampled trajectories, or with the initial set.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the derivation is self-contained, with bounds computed from an explicit observation model and external verifiers rather than from the target claim.

full rationale

The paper's derivation chain is not circular. It assumes an explicit observation model in Eqs. (4)-(7), in which the observation is a composition of entity-specific geometric transformations and alpha blending, then uses DeepG [12] to bound each transformed entity and mask, a modified CROWN/linear relaxation to bound the blending function and the controller, and finally propagates the resulting bounds through the dynamics. No parameter is fitted to the reachable-set output, and the final bound is not used to adjust the earlier pixel bounds. The soundness of DeepG and CROWN is external and independently established; the only self-citation ([21]) is used as a state-based reachability subroutine and is not load-bearing for the novel observation-bounding claim. The gap between the hand-authored alpha-compositing model and the actual Gym renderers is a correctness or validation limitation, not a circular reduction: the formal guarantee is conditional on the model, and no equation in the paper reduces the target result to its own input. Hence the circularity score is 0.

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

The central claim depends on no fitted numeric constants. The hand-designed artifacts are the masks alpha_i and mappings mu_i(x), which are structural rather than numeric free parameters. The reliance on external soundness theorems (DeepG, CROWN) and on the exact match between the modeled and actual observation process are the main assumptions.

assumptions (4)
  • domain assumption The true observation process equals the alpha-composited geometric transformations of fixed entity templates with known masks and known state-to-parameter maps (Eq (4)-(7)).
    This equality is required for bounds on the modeled observation process to bound the actual observations; the paper does not validate it against the Gym renderers.
  • standard math DeepG's pixel-wise linear bounds are sound over the specified transformation parameter ranges (Theorem II.3).
    The paper relies on this external tool's soundness without re-deriving it.
  • standard math CROWN/LiRPA produces sound upper and lower affine bounds for the blending function and the controller network (Theorem II.1).
    Borrowed from reference [1].
  • domain assumption The dynamics f and state set Xt are known and can be bounded soundly.
    State-based reachability tools require an accurate dynamics model; the paper's limitations section states this requirement.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Verification of Visual Controllers via Compositional Geometric Transformations." pith.science (2026). https://pith.science/paper/RTQVEJOS

@misc{pith2026250704523,
  author       = {Pith},
  title        = {Pith review of: Verification of Visual Controllers via Compositional Geometric Transformations},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/RTQVEJOS}},
  note         = {Machine review of arXiv:2507.04523}
}
read the original abstract

Perception-based neural network controllers are increasingly used in autonomous systems that rely on visual inputs to operate in the real world. Ensuring the safety of such systems under uncertainty is challenging. Existing verification techniques typically focus on Lp-bounded perturbations in the pixel space, which fails to capture the low-dimensional structure of many real-world effects. In this work, we introduce a novel verification framework for perception-based controllers that can generate outer-approximations of reachable sets through explicitly modeling uncertain observations with geometric perturbations. Our approach constructs a boundable mapping from states to images, enabling the use of state-based verification tools while accounting for uncertainty in perception. We provide theoretical guarantees on the soundness of our method and demonstrate its effectiveness across benchmark control environments. This work provides a principled framework for certifying the safety of perception-driven control systems under realistic visual perturbations.

Figures

Figures reproduced from arXiv: 2507.04523 by the authors.

Figure 1
Figure 1. Dynamical System with Vision-Based Control Policy. [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Verification Pipeline. Given an initial state range, the proposed algorithm calculates bounds on future states. [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. An environment decomposed into entities. This paper [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figures from the paper (4 more)
Figure 4
Figure 4. Figure 4: Reachable sets over multiple timesteps for three systems. Our method’s reachable sets (bounding boxes) are shown [PITH_FULL_IMAGE:figures/full_fig_p006_4.png]
Figure 5
Figure 5. Figure 5: For two systems, a visual representation of image upper (top) and lower (bottom) bounds for each entity (first two [PITH_FULL_IMAGE:figures/full_fig_p007_5.png]
Figure 6
Figure 6. Figure 6: Bound slackness Eq (10) by image resolutions. [PITH_FULL_IMAGE:figures/full_fig_p007_6.png]
Figure 7
Figure 7. Figure 7: Reachable sets on Acrobot for varying image sizes (and thus different control policies). [PITH_FULL_IMAGE:figures/full_fig_p008_7.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

47 extracted references · 40 canonical work pages

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

    work page 2018

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

    work page 2018

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

    work page 2020

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

    work page 2018

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

    work page 2018

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

    work page 2019

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

    work page 2017

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

    work page 2021

Show all 47 references
  1. [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

  2. [10]

    An abstract domain for certifying neural networks,

    G. Singh, T. Gehr, M. P ¨uschel, and M. Vechev, “An abstract domain for certifying neural networks,” Proceedings of the ACM on Programming Languages, vol. 3, no. POPL, pp. 1–30, 2019

    2019

  3. [11]

    On the effectiveness of interval bound propagation for training verifiably robust models,

    S. Gowal, K. Dvijotham, R. Stanforth, R. Bunel, C. Qin, J. Uesato, R. Arandjelovic, T. Mann, and P. Kohli, “On the effectiveness of interval bound propagation for training verifiably robust models,”

  4. [12]

    Certi- fying geometric robustness of neural networks,

    M. Balunovic, M. Baader, G. Singh, T. Gehr, and M. Vechev, “Certi- fying geometric robustness of neural networks,” Advances in Neural Information Processing Systems , vol. 32, 2019

    2019

  5. [13]

    Towards verifying robustness of neural networks against a family of semantic perturbations,

    J. Mohapatra, T.-W. Weng, P.-Y . Chen, S. Liu, and L. Daniel, “Towards verifying robustness of neural networks against a family of semantic perturbations,” in Proceedings of the IEEE/CVF Conference on Com- puter Vision and Pattern Recognition , 2020, pp. 244–252

    2020

  6. [14]

    Tss: Transformation-specific smoothing for robustness certification,

    L. Li, M. Weber, X. Xu, L. Rimanic, B. Kailkhura, T. Xie, C. Zhang, and B. Li, “Tss: Transformation-specific smoothing for robustness certification,” in Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security , 2021, pp. 535–557

    2021

  7. [15]

    Ver- ification of image-based neural network controllers using generative models,

    S. M. Katz, A. L. Corso, C. A. Strong, and M. J. Kochenderfer, “Ver- ification of image-based neural network controllers using generative models,” Journal of Aerospace Information Systems , vol. 19, no. 9, pp. 574–584, 2022

    2022

  8. [16]

    Scalable and interpretable verifica- tion of image-based neural network controllers for autonomous vehi- cles,

    A. Parameshwaran and Y . Wang, “Scalable and interpretable verifica- tion of image-based neural network controllers for autonomous vehi- cles,” in Proceedings of the ACM/IEEE 16th International Conference on Cyber-Physical Systems (with CPS-IoT Week 2025) , 2025, pp. 1– 11

    2025

  9. [17]

    Bunel, J

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

    2023

  10. [18]

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

    2025

  11. [19]

    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

  12. [20]

    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

  13. [21]

    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

  14. [22]

    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

  15. [23]

    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

  16. [24]

    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

  17. [25]

    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

  18. [26]

    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

  19. [27]

    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

  20. [28]

    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

  21. [29]

    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

  22. [30]

    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

  23. [31]

    Probably approximately correct vision- based planning using motion primitives,

    S. Veer and A. Majumdar, “Probably approximately correct vision- based planning using motion primitives,” in Conference on Robot Learning. PMLR, 2021, pp. 1001–1014

    2021

  24. [32]

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

    G. Chou, N. Ozay, and D. Berenson, “Safe output feedback motion planning from images via learned perception modules and contraction theory,” in International Workshop on the Algorithmic Foundations of Robotics. Springer, 2022, pp. 349–367

    2022

  25. [33]

    Scenario-based compositional verification of autonomous systems with neural perception,

    C. Watson, R. Alur, D. Gopinath, R. Mangal, and C. S. Pasareanu, “Scenario-based compositional verification of autonomous systems with neural perception,” arXiv preprint arXiv:2504.20942 , 2025

    2025 arXiv

  26. [34]

    Verifying controllers with vision-based perception using safe approx- imate abstractions,

    C. Hsieh, Y . Li, D. Sun, K. Joshi, S. Misailovic, and S. Mitra, “Verifying controllers with vision-based perception using safe approx- imate abstractions,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 41, no. 11, pp. 4205–4216, 2022

    2022

  27. [35]

    System-level safety monitoring and re- covery for perception failures in autonomous vehicles,

    K. Chakraborty, Z. Feng, S. Veer, A. Sharma, B. Ivanovic, M. Pavone, and S. Bansal, “System-level safety monitoring and re- covery for perception failures in autonomous vehicles,” arXiv preprint arXiv:2409.17630, 2024

    2024 arXiv

  28. [36]

    Enhancing safety and robustness of vision-based controllers via reachability analysis,

    K. Chakraborty, A. Gupta, and S. Bansal, “Enhancing safety and robustness of vision-based controllers via reachability analysis,” arXiv preprint arXiv:2410.21736, 2024

    2024 arXiv

  29. [37]

    Discovering closed-loop failures of vision-based controllers via reachability analysis,

    K. Chakraborty and S. Bansal, “Discovering closed-loop failures of vision-based controllers via reachability analysis,” IEEE Robotics and Automation Letters, vol. 8, no. 5, pp. 2692–2699, 2023

    2023

  30. [38]

    Toward certified robustness against real-world distribution shifts,

    H. Wu, T. Tagomori, A. Robey, F. Yang, N. Matni, G. Pappas, H. Hassani, C. Pasareanu, and C. Barrett, “Toward certified robustness against real-world distribution shifts,” in 2023 IEEE Conference on Secure and Trustworthy Machine Learning (SaTML) . IEEE, 2023, pp. 537–553

    2023

  31. [39]

    Data- driven modeling and verification of perception-based autonomous systems,

    T. Waite, A. Robey, H. Hamed, G. J. Pappas, and R. Ivanov, “Data- driven modeling and verification of perception-based autonomous systems,” arXiv preprint arXiv:2312.06848 , 2023

    2023 arXiv

  32. [40]

    Enforcing safety for vision-based controllers via control barrier functions and neural radiance fields,

    M. Tong, C. Dawson, and C. Fan, “Enforcing safety for vision-based controllers via control barrier functions and neural radiance fields,” in 2023 IEEE International Conference on Robotics and Automation (ICRA). IEEE, 2023, pp. 10 511–10 517

    2023

  33. [41]

    Nnlander-verif: A neural network formal verification framework for vision-based autonomous aircraft landing,

    U. Santa Cruz and Y . Shoukry, “Nnlander-verif: A neural network formal verification framework for vision-based autonomous aircraft landing,” in NASA Formal Methods Symposium . Springer, 2022, pp. 213–230

    2022

  34. [42]

    One-shot reachabil- ity analysis of neural network dynamical systems,

    S. Chen, V . M. Preciado, and M. Fazlyab, “One-shot reachabil- ity analysis of neural network dynamical systems,” arXiv preprint arXiv:2209.11827, 2022

    2022 arXiv

  35. [43]

    Branch and bound for piecewise linear neural network verification,

    R. Bunel, J. Lu, I. Turkaslan, P. H. Torr, P. Kohli, and M. P. Kumar, “Branch and bound for piecewise linear neural network verification,” Journal of Machine Learning Research , vol. 21, no. 42, pp. 1–39, 2020

    2020

  36. [44]

    Neural network verification with branch-and-bound for general nonlineari- ties,

    Z. Shi, Q. Jin, Z. Kolter, S. Jana, C.-J. Hsieh, and H. Zhang, “Neural network verification with branch-and-bound for general nonlineari- ties,” in International Conference on Tools and Algorithms for the Construction and Analysis of Systems . Springer, 2025, pp. 315–335

    2025

  37. [45]

    Gymnasium: A standard interface for reinforcement learning environments,

    M. Towers, A. Kwiatkowski, J. Terry, J. U. Balis, G. De Cola, T. Deleu, M. Goulao, A. Kallinteris, M. Krimmel, A. KG et al., “Gymnasium: A standard interface for reinforcement learning environments,” arXiv preprint arXiv:2407.17032, 2024

    2024 arXiv

  38. [46]

    Proximal policy optimization algorithms,

    J. Schulman, F. Wolski, P. Dhariwal, A. Radford, and O. Klimov, “Proximal policy optimization algorithms,” arXiv preprint arXiv:1707.06347, 2017

    2017 arXiv

  39. [2019]

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

    [Online]. Available: https://arxiv.org/abs/1810.12715

    arXiv

Pith tools

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