BURNS: Backward Underapproximate Reachability for Neural-Feedback-Loop Systems

Chelsea Rose Sidrane, Jana Tumova
Proceedings of The 8th Annual Learning for Dynamics and Control Conference, PMLR 331:965-981, 2026.

Abstract

Learning-enabled planning and control algorithms are increasingly popular, but they often lack rigorous guarantees of performance or safety. Frameworks such as reachability analysis can be used to provide such guarantees. We introduce an algorithm for computing underapproximate backward reachable sets of nonlinear discrete time neural feedback loops. We then use the backward reachable sets to check goal-reaching properties. Our algorithm is based upon ideas from robustness analysis for vision networks, and on overapproximating the system dynamics function. Together these enable computation of underapproximate backward reachable sets through solutions of mixed-integer linear programs. We rigorously analyze the soundness of our algorithm and demonstrate it on a numerical example. Our work expands the class of properties that can be verified for learning-enabled systems.

Cite this Paper

BibTeX
@InProceedings{pmlr-v331-sidrane26a, title = {BURNS: Backward Underapproximate Reachability for Neural-Feedback-Loop Systems}, author = {Sidrane, Chelsea Rose and Tumova, Jana}, booktitle = {Proceedings of The 8th Annual Learning for Dynamics and Control Conference}, pages = {965--981}, year = {2026}, editor = {Sukhatme, Gaurav and Lindemann, Lars and Tu, Stephen and Wierman, Adam and Atanasov, Nikolay}, volume = {331}, series = {Proceedings of Machine Learning Research}, month = {17--19 Jun}, publisher = {PMLR}, pdf = {https://raw.githubusercontent.com/mlresearch/v331/main/assets/sidrane26a/sidrane26a.pdf}, url = {https://proceedings.mlr.press/v331/sidrane26a.html}, abstract = {Learning-enabled planning and control algorithms are increasingly popular, but they often lack rigorous guarantees of performance or safety. Frameworks such as reachability analysis can be used to provide such guarantees. We introduce an algorithm for computing underapproximate backward reachable sets of nonlinear discrete time neural feedback loops. We then use the backward reachable sets to check goal-reaching properties. Our algorithm is based upon ideas from robustness analysis for vision networks, and on overapproximating the system dynamics function. Together these enable computation of underapproximate backward reachable sets through solutions of mixed-integer linear programs. We rigorously analyze the soundness of our algorithm and demonstrate it on a numerical example. Our work expands the class of properties that can be verified for learning-enabled systems.} }
Endnote
%0 Conference Paper %T BURNS: Backward Underapproximate Reachability for Neural-Feedback-Loop Systems %A Chelsea Rose Sidrane %A Jana Tumova %B Proceedings of The 8th Annual Learning for Dynamics and Control Conference %C Proceedings of Machine Learning Research %D 2026 %E Gaurav Sukhatme %E Lars Lindemann %E Stephen Tu %E Adam Wierman %E Nikolay Atanasov %F pmlr-v331-sidrane26a %I PMLR %P 965--981 %U https://proceedings.mlr.press/v331/sidrane26a.html %V 331 %X Learning-enabled planning and control algorithms are increasingly popular, but they often lack rigorous guarantees of performance or safety. Frameworks such as reachability analysis can be used to provide such guarantees. We introduce an algorithm for computing underapproximate backward reachable sets of nonlinear discrete time neural feedback loops. We then use the backward reachable sets to check goal-reaching properties. Our algorithm is based upon ideas from robustness analysis for vision networks, and on overapproximating the system dynamics function. Together these enable computation of underapproximate backward reachable sets through solutions of mixed-integer linear programs. We rigorously analyze the soundness of our algorithm and demonstrate it on a numerical example. Our work expands the class of properties that can be verified for learning-enabled systems.
APA
Sidrane, C.R. & Tumova, J.. (2026). BURNS: Backward Underapproximate Reachability for Neural-Feedback-Loop Systems. Proceedings of The 8th Annual Learning for Dynamics and Control Conference, in Proceedings of Machine Learning Research 331:965-981 Available from https://proceedings.mlr.press/v331/sidrane26a.html.

Related Material