Formal Verification of Analog AI Hardware (FAI)

• Applicants: Professor Dr.-Ing. Matthias Althoff; Professor Dr.-Ing. Lars Hedrich; Dr.-Ing. Markus Olbrich
• Subject Area: Electronic Semiconductors, Components and Circuits, Integrated Systems, Sensor Technology, Theoretical Electrical Engineering
• Term: since 2016
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 286525601

Due to the current trend towards artificial intelligence, neural networks and their realizations in hardware gain more and more importance. Despite their advantages, the major drawback of neural networks is that they are extremely hard to verify since their large complexity usually prohibits the application of existing verification techniques. However, if AI can not be made safe, it will not be used in the real world for safety-critical applications, despite the huge investments in researching AI methods. Therefore, we will develop completely new approaches for the formal verification of analog AI hardware that are able to handle neural networks of arbitrary sizes and types of neurons e.g. energy-efficient transistor-level implementations. Our approach will provide the following features. Exceptional scalability to handle the huge complexity of neural networks using a compositional verification framework is realized by exploiting the nature of neural networks being composed of many smaller often identical subsystems. For accelerating verification, we will develop novel specification-oriented reachability algorithms that automatically adapt the accuracy of reachable sets until the given specification is proven or disproven. This together with advanced order reduction methods and verification-driven synthesis of neurons results in computational efficiency. The proposed synthesis approach in strong coupling with the verification algorithms creates simpler models supporting the verification of larger networks. The envisioned AI-focused framework will be able to handle arbitrary types of neurons being also applicable to a broader class of applications such as vehicle control or analog signal processing. It will provide counterexamples that demonstrate the violation to support the developers during the design process. The project will demonstrate the applicability to real systems with two real-world examples: A medical example featuring an analog circuit with 2000 neurons, and an automotive example consisting of a neural-network-controlled autonomous car.

• DFG Programme: Research Grants