{"id":{"repo_id":"mit","oai_identifier":"oai:dspace.mit.edu:1721.1/154166"},"canonical_url":"https://search.dev.ndltd.org/etd/mit/oai:dspace.mit.edu:1721.1/154166","repository":{"repo_id":"mit","name":"MIT","base_url":"https://dspace.mit.edu/oai/request"},"display":{"title":"BReach-LP: a Framework for Backward Reachability Analysis of Neural Feedback Loops","abstract":"Neural networks (NNs) can be used to solve a wide variety of robotics problems ranging from computer vision to control. However, while NNs often work well in nominal scenarios, their performance can decrease significantly in scenarios that they were not trained for. Thus, as we move toward real-world deployment of neural feedback loops (NFLs), i.e., closed-loop systems containing NNs, it is critical that we develop methods to verify that these systems are safe. Previous works have developed forward reachability techniques to verify safety for NFLs, but these techniques can be prohibitively conservative in non-convex settings such as obstacle avoidance. To enable safety verificaiton in non-convex settings, this thesis proposes BReach-LP: a set of techniques to conduct backward reachability analysis for NFLs. While backward reachability analysis has been studied for systems not containing NNs, the general noninvertability of NNs makes backward reachability analysis for NFLs a challenging problem. Thus, our approach leverages existing forward NN analysis tools to find affine bounds on the control inputs and solve a series of linear programs to efficiently find an approximation of the backprojection sets, i.e., the set of states for which an NN control policy will drive the system to a given target set. This thesis outlines four variations of BReach-LP, including proofs of their soundness and numerical results demonstrating their application.","abstract_html":"Neural networks (NNs) can be used to solve a wide variety of robotics problems ranging from computer vision to control. However, while NNs often work well in nominal scenarios, their performance can decrease significantly in scenarios that they were not trained for. Thus, as we move toward real-world deployment of neural feedback loops (NFLs), i.e., closed-loop systems containing NNs, it is critical that we develop methods to verify that these systems are safe. Previous works have developed forward reachability techniques to verify safety for NFLs, but these techniques can be prohibitively conservative in non-convex settings such as obstacle avoidance. To enable safety verificaiton in non-convex settings, this thesis proposes BReach-LP: a set of techniques to conduct backward reachability analysis for NFLs. While backward reachability analysis has been studied for systems not containing NNs, the general noninvertability of NNs makes backward reachability analysis for NFLs a challenging problem. Thus, our approach leverages existing forward NN analysis tools to find affine bounds on the control inputs and solve a series of linear programs to efficiently find an approximation of the backprojection sets, i.e., the set of states for which an NN control policy will drive the system to a given target set. This thesis outlines four variations of BReach-LP, including proofs of their soundness and numerical results demonstrating their application.","abstract_has_math":false,"creators":["Rober, Nicholas"],"institution":"Massachusetts Institute of Technology","degree_name":"Master","degree_level":null,"degree_discipline":null,"degree_department":"Massachusetts Institute of Technology. Department of Aeronautics and Astronautics","school":null,"contributors":[],"advisors":["How, Jonathan, P."],"committee_chairs":[],"committee_members":[],"year":2023,"date_issued":"2023-06","date_published":"2023-06","updated_at":"2026-07-22T22:21:34Z","subjects":[],"languages":[],"rights":["In Copyright - Educational Use Permitted","Copyright MIT"],"rights_urls":["http://rightsstatements.org/page/InC-EDU/1.0/"],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/1721.1/154166","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["How, Jonathan, P."]},{"key":"dc:contributor.department","label":"Department","values":["Massachusetts Institute of Technology. Department of Aeronautics and Astronautics"]},{"key":"dc:creator","label":"Author","values":["Rober, Nicholas"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2024-04-16T19:05:03Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2024-04-16T19:05:03Z"]},{"key":"dc:date.issued","label":"Date","values":["2023-06"]},{"key":"dc:publisher","label":"Institution","values":["Massachusetts Institute of Technology"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Master","Master of Science in Aeronautics and Astronautics"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:rights","label":"Dc Rights","values":["In Copyright - Educational Use Permitted","Copyright MIT"]},{"key":"dc:rights.uri","label":"Rights URI","values":["http://rightsstatements.org/page/InC-EDU/1.0/"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://hdl.handle.net/1721.1/154166"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["Neural networks (NNs) can be used to solve a wide variety of robotics problems ranging from computer vision to control. However, while NNs often work well in nominal scenarios, their performance can decrease significantly in scenarios that they were not trained for. Thus, as we move toward real-world deployment of neural feedback loops (NFLs), i.e., closed-loop systems containing NNs, it is critical that we develop methods to verify that these systems are safe. Previous works have developed forward reachability techniques to verify safety for NFLs, but these techniques can be prohibitively conservative in non-convex settings such as obstacle avoidance. To enable safety verificaiton in non-convex settings, this thesis proposes BReach-LP: a set of techniques to conduct backward reachability analysis for NFLs. While backward reachability analysis has been studied for systems not containing NNs, the general noninvertability of NNs makes backward reachability analysis for NFLs a challenging problem. Thus, our approach leverages existing forward NN analysis tools to find affine bounds on the control inputs and solve a series of linear programs to efficiently find an approximation of the backprojection sets, i.e., the set of states for which an NN control policy will drive the system to a given target set. This thesis outlines four variations of BReach-LP, including proofs of their soundness and numerical results demonstrating their application."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["S.M."]},{"key":"dc:title","label":"Title","values":["BReach-LP: a Framework for Backward Reachability Analysis of Neural Feedback Loops"]}]}],"canonical_facts":{"dc:contributor.advisor":["How, Jonathan, P."],"dc:contributor.department":["Massachusetts Institute of Technology. Department of Aeronautics and Astronautics"],"dc:creator":["Rober, Nicholas"],"dc:date.accessioned":["2024-04-16T19:05:03Z"],"dc:date.available":["2024-04-16T19:05:03Z"],"dc:date.issued":["2023-06"],"dc:description.abstract":["Neural networks (NNs) can be used to solve a wide variety of robotics problems ranging from computer vision to control. However, while NNs often work well in nominal scenarios, their performance can decrease significantly in scenarios that they were not trained for. Thus, as we move toward real-world deployment of neural feedback loops (NFLs), i.e., closed-loop systems containing NNs, it is critical that we develop methods to verify that these systems are safe. Previous works have developed forward reachability techniques to verify safety for NFLs, but these techniques can be prohibitively conservative in non-convex settings such as obstacle avoidance. To enable safety verificaiton in non-convex settings, this thesis proposes BReach-LP: a set of techniques to conduct backward reachability analysis for NFLs. While backward reachability analysis has been studied for systems not containing NNs, the general noninvertability of NNs makes backward reachability analysis for NFLs a challenging problem. Thus, our approach leverages existing forward NN analysis tools to find affine bounds on the control inputs and solve a series of linear programs to efficiently find an approximation of the backprojection sets, i.e., the set of states for which an NN control policy will drive the system to a given target set. This thesis outlines four variations of BReach-LP, including proofs of their soundness and numerical results demonstrating their application."],"dc:description.degree":["S.M."],"dc:identifier.uri":["https://hdl.handle.net/1721.1/154166"],"dc:publisher":["Massachusetts Institute of Technology"],"dc:rights":["In Copyright - Educational Use Permitted","Copyright MIT"],"dc:rights.uri":["http://rightsstatements.org/page/InC-EDU/1.0/"],"dc:title":["BReach-LP: a Framework for Backward Reachability Analysis of Neural Feedback Loops"],"dc:type":["Thesis"],"thesis:degree_name":["Master","Master of Science in Aeronautics and Astronautics"]},"updated_at":"2026-07-22T22:21:34Z"}