Learning Verifiable Control Policies Using Relaxed Verification
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916704025575424 |
|---|---|
| author | Chaudhury, Puja Estornell, Alexander Everett, Michael |
| author_facet | Chaudhury, Puja Estornell, Alexander Everett, Michael |
| contents | To provide safety guarantees for learning-based control systems, recent work has developed formal verification methods to apply after training ends. However, if the trained policy does not meet the specifications, or there is conservatism in the verification algorithm, establishing these guarantees may not be possible. Instead, this work proposes to perform verification throughout training to ultimately aim for policies whose properties can be evaluated throughout runtime with lightweight, relaxed verification algorithms. The approach is to use differentiable reachability analysis and incorporate new components into the loss function. Numerical experiments on a quadrotor model and unicycle model highlight the ability of this approach to lead to learned control policies that satisfy desired reach-avoid and invariance specifications. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_16879 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Learning Verifiable Control Policies Using Relaxed Verification Chaudhury, Puja Estornell, Alexander Everett, Michael Systems and Control Machine Learning To provide safety guarantees for learning-based control systems, recent work has developed formal verification methods to apply after training ends. However, if the trained policy does not meet the specifications, or there is conservatism in the verification algorithm, establishing these guarantees may not be possible. Instead, this work proposes to perform verification throughout training to ultimately aim for policies whose properties can be evaluated throughout runtime with lightweight, relaxed verification algorithms. The approach is to use differentiable reachability analysis and incorporate new components into the loss function. Numerical experiments on a quadrotor model and unicycle model highlight the ability of this approach to lead to learned control policies that satisfy desired reach-avoid and invariance specifications. |
| title | Learning Verifiable Control Policies Using Relaxed Verification |
| topic | Systems and Control Machine Learning |
| url | https://arxiv.org/abs/2504.16879 |