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

合作研究：FMitF：第一轨：使用形式方法合成和验证内存计算系统

• 批准号: 2319399
• 负责人: Rickard Ewetz
• 金额: $ 25万
• 依托单位: The University of Central Florida Board of Trustees
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-09-01 至 2027-08-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2319399&HistoricalAwards=false
• 关键词: Collaborative; Research; FMitF; Track; Synthesis

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.

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