Certified Approximate Reachability (CARe): Formal Error Bounds on Deep Learning of Reachable Sets
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866910899737985024 |
|---|---|
| author | Solanki, Prashant Vertovec, Nikolaus Schnitzer, Yannik Van Beers, Jasper de Visser, Coen Abate, Alessandro |
| author_facet | Solanki, Prashant Vertovec, Nikolaus Schnitzer, Yannik Van Beers, Jasper de Visser, Coen Abate, Alessandro |
| contents | Recent approaches to leveraging deep learning for computing reachable sets of continuous-time dynamical systems have gained popularity over traditional level-set methods, as they overcome the curse of dimensionality. However, as with level-set methods, considerable care needs to be taken in limiting approximation errors, particularly since no guarantees are provided during training on the accuracy of the learned reachable set. To address this limitation, we introduce an epsilon-approximate Hamilton-Jacobi Partial Differential Equation (HJ-PDE), which establishes a relationship between training loss and accuracy of the true reachable set. To formally certify this approximation, we leverage Satisfiability Modulo Theories (SMT) solvers to bound the residual error of the HJ-based loss function across the domain of interest. Leveraging Counter Example Guided Inductive Synthesis (CEGIS), we close the loop around learning and verification, by fine-tuning the neural network on counterexamples found by the SMT solver, thus improving the accuracy of the learned reachable set. To the best of our knowledge, Certified Approximate Reachability (CARe) is the first approach to provide soundness guarantees on learned reachable sets of continuous dynamical systems. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_23912 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Certified Approximate Reachability (CARe): Formal Error Bounds on Deep Learning of Reachable Sets Solanki, Prashant Vertovec, Nikolaus Schnitzer, Yannik Van Beers, Jasper de Visser, Coen Abate, Alessandro Systems and Control Machine Learning Optimization and Control Recent approaches to leveraging deep learning for computing reachable sets of continuous-time dynamical systems have gained popularity over traditional level-set methods, as they overcome the curse of dimensionality. However, as with level-set methods, considerable care needs to be taken in limiting approximation errors, particularly since no guarantees are provided during training on the accuracy of the learned reachable set. To address this limitation, we introduce an epsilon-approximate Hamilton-Jacobi Partial Differential Equation (HJ-PDE), which establishes a relationship between training loss and accuracy of the true reachable set. To formally certify this approximation, we leverage Satisfiability Modulo Theories (SMT) solvers to bound the residual error of the HJ-based loss function across the domain of interest. Leveraging Counter Example Guided Inductive Synthesis (CEGIS), we close the loop around learning and verification, by fine-tuning the neural network on counterexamples found by the SMT solver, thus improving the accuracy of the learned reachable set. To the best of our knowledge, Certified Approximate Reachability (CARe) is the first approach to provide soundness guarantees on learned reachable sets of continuous dynamical systems. |
| title | Certified Approximate Reachability (CARe): Formal Error Bounds on Deep Learning of Reachable Sets |
| topic | Systems and Control Machine Learning Optimization and Control |
| url | https://arxiv.org/abs/2503.23912 |