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

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

• 批准号: 2404036
• 负责人: Sumit Jha
• 金额: $ 25万
• 依托单位: Florida International University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-11-01 至 2027-08-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2404036&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 的法定使命，通过评估认为值得支持利用基金会的智力优势和更广泛的影响审查标准。