Formal Verification of Analog AI Hardware (FAI)

The FAI project is funded by the German Research Foundation (DFG). The project represents a collaboration between the Leibniz University of Hanover, the Technical University of Munich and the Goethe University of Frankfurt.

This project aims to verify analog Artificial Intelligence hardware to be utilized for safety-critical applications. The existing verification techniques cannot be applied for such task due to the large complexity of Neural Networks.

Our research team investigates the development of new approaches for the formal verification of analog AI hardware that can handle neural networks of arbitrary sizes and types of neurons. Our approach integrates advanced order reduction methods with the implementation of compositional verification framework to handle the increased complexity of the neural networks.

We will develop a new specification-oriented reachability algorithms that automatically adjust the precision of reachable sets up until the provided specification is confirmed or refuted in order to speed up verification. Computational efficiency is achieved by combining this with sophisticated order reduction techniques and verification-driven synthesis of neurons. The suggested synthesis approach produces simpler models that facilitate the verification of bigger networks through a tight interaction with the verification algorithms. The envisioned AI-focused framework will be capable of handling various types of neurons and be applicable to a wider class of applications, including analog signal processing and vehicle control. To assist the designers throughout the design phase, it will offer counterexamples that illustrate the violation.