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系统的现场制造展示了这些创新。这项工作创建了新的算法，以实现在新兴的内存硬件技术中部署强大的AI模型，这些技术可能比传统的CMOS技术更容易出现错误。该项目还将允许对功耗减少的神经网络进行培训。鉴于AI的更大采用以及培训越来越强大的神经网络的需求，这一点尤其重要。这项工作为研究社区提供了其他一些贡献，包括提高神经网络对内存电路的可靠性，增加计算机工程和计算机科学的多样性，并跨正式方法，机器学习和硬件设计促进跨学科的合作。该项目致力于推进正式方法，以应对新兴的内存计算系统中遇到的现实世界挑战。通过利用机器学习和形式方法的最新创新，该项目使用决策图，神经网和增强学习来合成神经网的横杆。在通过制造证明这种内存计算系统之前，它会验证双向数字IMC电路。这种努力扩展了我们对内存计算系统的能力和局限性的理解，并在诸如内存计算，正式方法和人工智能等领域创造了创新。该奖项反映了NSF的法定任务，并被认为是值得通过基金会的智力和更广泛影响的评估来通过评估来获得支持的。