Formal Verification of Analog AI Hardware (FAI)

由于人工智能的发展趋势，神经网络及其在硬件上的实现变得越来越重要。尽管神经网络具有优势，但其主要缺点是难以验证，因为其巨大的复杂性通常阻碍了现有验证技术的应用。然而，如果人工智能不能做到安全，那么尽管在研究人工智能方法方面投入了巨大资金，但它将不会在现实世界中用于安全关键应用。因此，我们将开发全新的方法来正式验证模拟人工智能硬件，这些硬件能够处理任意大小和类型的神经元的神经网络，例如节能的晶体管级实现。我们的方法将提供以下特性。通过利用神经网络由许多较小的通常相同的子系统组成的特性，利用组合验证框架实现了处理神经网络巨大复杂性的卓越可扩展性。为了加速验证，我们将开发新的面向规范的可达性算法，自动调整可达集的准确性，直到给定的规范被证明或被否定。这与先进的降阶方法和验证驱动的神经元合成一起导致计算效率。与验证算法强耦合的综合方法创建了更简单的模型，支持更大网络的验证。设想中的以人工智能为中心的框架将能够处理任意类型的神经元，也适用于更广泛的应用类别，如车辆控制或模拟信号处理。它将提供反例来证明在设计过程中存在的冲突，以支持开发人员。该项目将通过两个现实世界的例子来证明其对真实系统的适用性：一个是具有2000个神经元的模拟电路的医疗例子，另一个是由神经网络控制的自动驾驶汽车组成的汽车例子。

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.