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

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.