Collaborative Research: FMitF: Track I: Synthesis and Verification of In-Memory Computing Systems using Formal Methods

这个项目是一个合作项目，汇集了正式方法，机器学习，计算机辅助设计和内存计算系统制造方面的专业知识。该项目的主要目标是创建可以在计算机内存中合成神经网络的形式化方法，并证明其正确性。该项目的任务包括使用模拟内存计算（IMC）加速神经网络的验证，以及使用形式化方法和机器学习合成神经网络的混合模拟-数字IMC。该项目使用IMC系统的现场制造来展示这些创新。这项工作创建了新的算法，用于在新兴的内存硬件技术上部署强大的AI模型，这些技术可能比传统的CMOS技术更容易出错。该项目还将允许在降低功耗的情况下训练神经网络。考虑到人工智能的广泛采用以及训练越来越强大的神经网络的需求，这一点尤为重要。这一奋进为研究界做出了其他几项贡献，包括增强内存电路上神经网络的可靠性，增加计算机工程和计算机科学的多样性，以及促进跨正式方法，机器学习和硬件设计的跨学科合作。该项目的重点是推进形式化方法，以解决新兴内存计算系统中遇到的现实挑战。通过利用机器学习和形式化方法的最新创新，该项目使用决策图、神经网络和强化学习来合成神经网络的交叉杆。它验证双向数字IMC电路，然后通过制造来演示这种内存计算系统。这一努力扩展了我们对内存计算系统的能力和局限性的理解，并在内存计算、形式化方法和人工智能等领域创造了创新。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

This project is a collaborative effort that brings together expertise in formal methods, machine learning, computer-aided design, and fabrication of in-memory computing systems. The main goal of the project is to create formal methods that can synthesize neural networks in the memory of the computer and also prove their correctness. The project pursues tasks that include the verification of neural networks accelerated using analog in-memory computing (IMC) and the synthesis of hybrid analog-digital IMC for neural networks using formal methods and machine learning. The project demonstrates these innovations using in-field fabrication of IMC systems. The effort creates new algorithms for enabling the deployment of robust AI models on emerging in-memory hardware technologies that may be more prone to errors than traditional CMOS technologies. The project would also allow the training of neural networks with reduced power consumption. This is particularly important given the larger adoption of AI and the need to train more and more powerful neural networks. The endeavor enables several other contributions to the research community, including enhancing the reliability of neural networks on in-memory circuits, increasing diversity in computer engineering and computer science, and fostering interdisciplinary collaboration across formal methods, machine learning, and hardware design. The project focuses on advancing formal methods to tackle real-world challenges encountered in emerging in-memory computing systems. By leveraging recent innovations in machine learning and formal methods, the project synthesizes crossbars for neural nets using decision diagrams, neural nets, and reinforcement learning. It verifies bidirectional digital IMC circuits before demonstrating such in-memory computing systems through fabrication. This effort expands our understanding of the capabilities and limitations of in-memory computing systems and creates innovations in fields such as in-memory computing, formal methods, and artificial intelligence.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.