Towards Neural Routing with Verified Bounds on Performance
When data-driven algorithms, especially the ones based on deep neural networks (DNNs), replace classical ones, their superior performance often comes with difficulty in their analysis. On the way to compensate for this drawback, formal verification techniques, which can provide reliable guarantees o...
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2022-09-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/1714 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1850025713898356736 |
|---|---|
| author | Igor Petrovich Buzhinsky Anatoly Abramovich Shalyto |
| author_facet | Igor Petrovich Buzhinsky Anatoly Abramovich Shalyto |
| author_sort | Igor Petrovich Buzhinsky |
| collection | DOAJ |
| description | When data-driven algorithms, especially the ones based on deep neural networks (DNNs), replace classical ones, their superior performance often comes with difficulty in their analysis. On the way to compensate for this drawback, formal verification techniques, which can provide reliable guarantees on program behavior, were developed for DNNs. These techniques, however, usually consider DNNs alone, excluding real-world environments in which they operate, and the applicability of techniques that do account for such environments is often limited. In this work, we consider the problem of formally verifying a neural controller for the routing problem in a conveyor network. Unlike in known problem statements, our DNNs are executed in a distributed context, and the performance of the routing algorithm, which we measure as the mean delivery time, depends on multiple executions of these DNNs. Under several assumptions, we reduce the problem to a number of DNN output reachability problems, which can be solved with existing tools. Our experiments indicate that sound-and-complete formal verification in such cases is feasible, although it is notably slower than the gradient-based search of adversarial examples.The paper is structured as follows. Section 1 introduces basic concepts. Then, Section 2 introduces the routing problem and DQN-Routing, the DNN-based algorithm that solves it. Section 3 proposes the contribution of this paper: a novel sound and complete approach to formally check an upper bound on the mean delivery time of DNN-based routing. This approach is experimentally evaluated in Section 4. The paper is concluded with some discussion of the results and outline of possible future work. |
| format | Article |
| id | doaj-art-2f84b372c3c14b909d82a02a5e0d183e |
| institution | DOAJ |
| issn | 1818-1015 2313-5417 |
| language | English |
| publishDate | 2022-09-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj-art-2f84b372c3c14b909d82a02a5e0d183e2025-08-20T03:00:45ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172022-09-0129322824510.18255/1818-1015-2022-3-228-2451324Towards Neural Routing with Verified Bounds on PerformanceIgor Petrovich Buzhinsky0Anatoly Abramovich Shalyto1Aalto UniversityITMO UniversityWhen data-driven algorithms, especially the ones based on deep neural networks (DNNs), replace classical ones, their superior performance often comes with difficulty in their analysis. On the way to compensate for this drawback, formal verification techniques, which can provide reliable guarantees on program behavior, were developed for DNNs. These techniques, however, usually consider DNNs alone, excluding real-world environments in which they operate, and the applicability of techniques that do account for such environments is often limited. In this work, we consider the problem of formally verifying a neural controller for the routing problem in a conveyor network. Unlike in known problem statements, our DNNs are executed in a distributed context, and the performance of the routing algorithm, which we measure as the mean delivery time, depends on multiple executions of these DNNs. Under several assumptions, we reduce the problem to a number of DNN output reachability problems, which can be solved with existing tools. Our experiments indicate that sound-and-complete formal verification in such cases is feasible, although it is notably slower than the gradient-based search of adversarial examples.The paper is structured as follows. Section 1 introduces basic concepts. Then, Section 2 introduces the routing problem and DQN-Routing, the DNN-based algorithm that solves it. Section 3 proposes the contribution of this paper: a novel sound and complete approach to formally check an upper bound on the mean delivery time of DNN-based routing. This approach is experimentally evaluated in Section 4. The paper is concluded with some discussion of the results and outline of possible future work.https://www.mais-journal.ru/jour/article/view/1714formal verificationtrustworthy aideep neural networksrouting problem |
| spellingShingle | Igor Petrovich Buzhinsky Anatoly Abramovich Shalyto Towards Neural Routing with Verified Bounds on Performance Моделирование и анализ информационных систем formal verification trustworthy ai deep neural networks routing problem |
| title | Towards Neural Routing with Verified Bounds on Performance |
| title_full | Towards Neural Routing with Verified Bounds on Performance |
| title_fullStr | Towards Neural Routing with Verified Bounds on Performance |
| title_full_unstemmed | Towards Neural Routing with Verified Bounds on Performance |
| title_short | Towards Neural Routing with Verified Bounds on Performance |
| title_sort | towards neural routing with verified bounds on performance |
| topic | formal verification trustworthy ai deep neural networks routing problem |
| url | https://www.mais-journal.ru/jour/article/view/1714 |
| work_keys_str_mv | AT igorpetrovichbuzhinsky towardsneuralroutingwithverifiedboundsonperformance AT anatolyabramovichshalyto towardsneuralroutingwithverifiedboundsonperformance |