Modelirovanie i Analiz Informatsionnykh Sistem
RUS  ENG    JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB  
General information
Latest issue
Archive
Impact factor

Search papers
Search references

RSS
Latest issue
Current issues
Archive issues
What is RSS



Model. Anal. Inform. Sist.:
Year:
Volume:
Issue:
Page:
Find






Personal entry:
Login:
Password:
Save password
Enter
Forgotten password?
Register


Modelirovanie i Analiz Informatsionnykh Sistem, 2022, Volume 29, Number 3, Pages 228–245
DOI: https://doi.org/10.18255/1818-1015-2022-3-228-245
(Mi mais778)
 

Theory of computing

Towards neural routing with verified bounds on performance

I. P. Buzhinskya, A. A. Shalytob

a Aalto University, 8 Maarintie, Espoo 02150, Finland
b ITMO University, 49 Kronverksky pr., Saint Petersburg 197101, Russia
References:
Abstract: 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.
Keywords: formal verification, trustworthy AI, deep neural networks, routing problem.
Funding agency Grant number
Russian Science Foundation 20-19-00700
The work was financially supported by the Russian Science Foundation (Project 20-19-00700).
Received: 16.06.2022
Revised: 25.08.2022
Accepted: 26.08.2022
Bibliographic databases:
Document Type: Article
UDC: 004.8
MSC: 68T07
Language: English
Citation: I. P. Buzhinsky, A. A. Shalyto, “Towards neural routing with verified bounds on performance”, Model. Anal. Inform. Sist., 29:3 (2022), 228–245
Citation in format AMSBIB
\Bibitem{BuzSha22}
\by I.~P.~Buzhinsky, A.~A.~Shalyto
\paper Towards neural routing with verified bounds on performance
\jour Model. Anal. Inform. Sist.
\yr 2022
\vol 29
\issue 3
\pages 228--245
\mathnet{http://mi.mathnet.ru/mais778}
\crossref{https://doi.org/10.18255/1818-1015-2022-3-228-245}
\mathscinet{http://mathscinet.ams.org/mathscinet-getitem?mr=4495439}
Linking options:
  • https://www.mathnet.ru/eng/mais778
  • https://www.mathnet.ru/eng/mais/v29/i3/p228
  • Citing articles in Google Scholar: Russian citations, English citations
    Related articles in Google Scholar: Russian articles, English articles
    Моделирование и анализ информационных систем
    Statistics & downloads:
    Abstract page:66
    Full-text PDF :26
    References:18
     
      Contact us:
     Terms of Use  Registration to the website  Logotypes © Steklov Mathematical Institute RAS, 2024