@InProceedings{scheibler-et-al-mbmv-2015,
author = "Karsten Scheibler and Leonore Winterer and Ralf Wimmer and Bernd Becker",
title = "Towards Verification of Artificial Neural Networks",
year = "2015",
month = mar,
booktitle = "Proceedings of the 18\textsuperscript{th} Workshop ``Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen'' (MBMV)",
address = "Chemnitz, Germany",
editor = "Ulrich Heinkel and Marko R{\"o}{\ss}ler and Daniel Kriesten",
isbn = "978-3-944640-34-1",
pages = "30--40",
publisher = "Technische Universit{\"a}t Chemnitz, Germany",
abstract = "We consider the safety verification of controllers obtained via
machine learning. This is an important problem as the employed
machine learning techniques work well in practice, but cannot guarantee
safety of the produced controller, which is typically represented as
an artificial neural network. Nevertheless, such methods are used
in safety-critical environments.\\par
In this paper we take a typical control problem, namely the Cart Pole System
(a.k.a. inverted pendulum),
and a model of its physical environment and study safety verification of
this system. To do so, we use bounded model checking (BMC). The created
formulas are solved with the SMT-solver iSAT3. We examine the problems
that occur during solving these formulas and show that
extending the solver by special deduction routines can reduce
both memory consumption and computation time on such instances significantly.
This constitutes a first step towards verification of machine-learned controllers,
but a lot of challenges remain.",
}