Formal Verification of Analog AI Hardware (FAI)

模拟 AI 硬件 (FAI) 的形式验证

• 批准号: 286525601
• 负责人: Professor Dr.-Ing. Matthias Althoff
• 金额: --
• 依托单位: Lehrstuhl für Informatik VI: Robotik, Künstliche Intelligenz und Echtzeitsysteme
• 依托单位国家: 德国
• 项目类别: Research Grants
• 资助国家: 德国
• 项目状态: 未结题
• 来源: https://gepris.dfg.de/gepris/projekt/286525601?language=en
• 关键词: Formal; Verification; Analog; AI; Hardware

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.

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