SHF: Small: Boosting Reasoning in Boolean Networks with Attributed Graph Learning

布尔网络，主要以图形表示，已经成为一种有效的逻辑表示，不仅可以模拟计算过程，还可以模拟科学和工程中的一些现象，如遗传分析，电子设计自动化，形式验证等。然而，在现代科学和工程应用中使用的布尔网络可能非常大，结构复杂，这使得它们在现实世界的应用中不太实用。例如，用于优化逻辑电路的布尔网络可能有数十亿个顶点，使用传统算法无法有效处理。近年来，机器学习（ML）技术被广泛应用于图上的各种问题，即图学习，通过利用社交网络预测和药物分析中的图特征，已成功地应用于加速应用。该项目旨在开发一个系统框架，利用图学习来推理布尔网络，包括数据集设计、学习算法开发、训练模型、系统集成和各种应用领域的评估。该框架将在一个可扩展的平台上实现，该平台可用于科学和工程领域的各种应用。该项目将为学术界和工业界参与者创造独特的教育和推广机会，包括研究生和本科生的指导，研究者在电子设计和深度学习方面的新课程的教学创新，以及吸引和培养具有不同背景的高素质研究人员。研究团队将在图融合、图粗化和细化以及图神经网络方面开发一套新颖的算法，以实现高质量和可扩展的嵌入，用于对十亿节点布尔网络的功能、高级抽象进行推理。该项目中的方法将介于形式化方法中的经典符号技术和机器学习之间，以便在许多领域（如验证和合成、生物信息学、人工智能和安全）中受益。具体来说，研究者计划在符号推理任务中利用和推进ML，这样它就可以像传统的符号推理方法一样执行真正可扩展的布尔推理。该项目的发展将集中在图融合和神经网络架构、特定领域压缩算法、端到端系统集成和大规模系统级并行性中的新算法上。此外，该框架将在算法设计空间探索中进行评估，目标是布尔可满足性求解和布尔优化。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Boolean networks, mostly represented as graphs, have emerged as an effective logical representation to model not only the computational processes but also several phenomena from science and engineering, such as genetic analysis, electronic design automation, formal verification, etc. However, Boolean networks used in modern science and engineering applications can be extremely large with complex structures, which makes them less practical for real-world applications. For example, Boolean networks for optimizing logic circuits can have billions of vertices and cannot be effectively handled using traditional algorithms. Recent years have seen a widespread application of machine-learning (ML) techniques to various problems over graphs, namely graph learning, which has been successfully applied to accelerate applications by exploiting graph features found in social-network prediction and drug analysis. This project aims to develop a systematic framework that leverages graph learning to reason about Boolean networks, including dataset design, learning-algorithm development, training models, system integration, and evaluation over various application domains. The framework will be implemented in an extensible platform that can be used for a variety of applications in science and engineering. This project will create unique education and outreach opportunities for both academic and industrial participants, which involve mentoring of graduate and undergraduate students, innovation in teaching with investigator’s new courses in electronic design and deep learning, and attracting and preparing high-quality researchers with diverse backgrounds.The team of researchers will develop a set of novel algorithms in graph fusion, graph coarsening and refinement, and graph neural networks, to achieve high-quality and scalable embeddings for reasoning about functional, high-level abstractions of billion-node Boolean networks. The methods in this project will sit between the classical symbolic techniques in formal methods and ML in order to benefit both research communities in many domains, such as verification and synthesis, bioinformatics, artificial intelligence, and security. Specifically, the investigator plans to leverage and advance ML in symbolic-reasoning tasks, such that it can perform truly scalable Boolean reasoning analogously to traditional symbolic-reasoning approaches. The developments of this project will focus on novel algorithms in graph fusion and neural network architectures, domain-specific compression algorithms, end-to-end system integration, and large-scale system-level parallelism. In addition, the framework will be evaluated in algorithmic design-space exploration, targeting Boolean satisfiability solving and Boolean optimization.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.