“Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates” by Udayan Mandal, Guy Amir, Haoze Wu, Ieva Daukantas, Fletcher Lee Newell, Umberto J. Ravaioli, Baoluo Meng, Michael Durling, Milan Ganai, Tobey Shim, Guy Katz, and Clark Barrett. In Proceedings of the 24^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '24), (Nina Narodytska and Philipp Rümmer, eds.), Oct. 2024, pp. 95-106. Prague, Czech Republic.
Deep reinforcement learning (DRL) is a powerful machine learning paradigm for generating agents that control autonomous systems. However, the “black box” nature of DRL agents limits their deployment in real-world safety-critical applications. A promising approach for providing strong guarantees on an agent’s behavior is to use Neural Lyapunov Barrier (NLB) certifcates, which are learned functions over the system whose properties indirectly imply that an agent behaves as desired. However, NLB-based certifcates are typically diffcult to learn and even more diffcult to verify, especially for complex systems. In this work, we present a novel method for training and verifying NLB-based certifcates for discrete-time systems. Specifcally, we introduce a technique for certifcate composition, which simplifes the verifcation of highly-complex systems by strategically designing a sequence of certifcates. When jointly verifed with neural network verifcation engines, these certifcates provide a formal guarantee that a DRL agent both achieves its goals and avoids unsafe behavior. Furthermore, we introduce a technique for certifcate fltering, which signifcantly simplifes the process of producing formally verifed certifcates. We demonstrate the merits of our approach with a case study on providing safety and liveness guarantees for a DRL-controlled spacecraft.
BibTeX entry:
@inproceedings{MAW+FMCAD24,
author = {Udayan Mandal and Guy Amir and Haoze Wu and Ieva Daukantas
and Fletcher Lee Newell and Umberto J. Ravaioli and Baoluo Meng
and Michael Durling and Milan Ganai and Tobey Shim and Guy Katz
and Clark Barrett},
editor = {Nina Narodytska and Philipp R{\"u}mmer},
title = {Formally Verifying Deep Reinforcement Learning Controllers
with Lyapunov Barrier Certificates},
booktitle = {Proceedings of the {\it 24^{th}} International Conference
on Formal Methods In Computer-Aided Design (FMCAD '24)},
pages = {95--106},
publisher = {TU Wien Academic Press},
month = oct,
year = {2024},
doi = {10.34727/2024/isbn.978-3-85448-065-5_15},
note = {Prague, Czech Republic},
url = {https://repositum.tuwien.at/handle/20.500.12708/200782}
}
(This webpage was created with bibtex2web.)