SAGE: A Symbiosis of Satisfiability Checking, Graph Neural Networks and Symbolic Computation

  • Director: Mădălina Eraşcu
  • Funding Agency: UEFISCDI (PN-III-P1-1.1-TE-2021-0676)
  • Project Period: September 2022 - August 2024
  • Host Institution: West University of Timisoara

    • Project Overview

    Our life depends on software and systems using software. Nowadays, software is complex and, hence, error-prone. In order to overcome this problem, we need methods for assisting the software development. This project addresses the challenging problem of program analysis by developing rigorous mathematical techniques dealing with the logically complex parts of software. At this aim, we will use, refine and combine methods from satisfiability checking, graph neural networks and symbolic computation. These will make possible the analysis of software that is beyond the power of existing methods since advanced symbolic computation techniques (invariant theory) and graph neural networks combined with satisfiability checking (SAT/SMT solving) is not exploited in the state-of-the-art program analysis methods and tools. e are going to develop new theory and algorithms that detects the problem symmetries and similarities in family of problems by combining invariant theory, graph neural networks and SAT/SMT solving which, unlike state-of-the-art, would allow solving efficiently theoretically intractable problems. Our research project targets the analysis of complex software and follows three main research directions:

    1. Methods for symmetry breaking and for learning problems similarities
    2. Theory and algorithms
    3. Tools and evaluations

    Project Results

    1. Optimization Solvers for Cloud Deployment: We benchmarked various optimization solvers for automating the deployment of component-based applications in the Cloud. By applying 15 symmetry-breaking strategies, computational performance improved significantly across different solvers, with Z3 showing the best results. However, static symmetry breaking strategies sometimes conflicted with solver techniques.
    2. SAGE Tool for Kubernetes: SAGE is a tool designed to optimize deployments in Kubernetes clusters, offering more efficient service placement than the default Kubernetes scheduler. It minimizes infrastructure costs by analyzing application demands and cluster resources, consistently providing optimal solutions.
    3. Graph Neural Networks for Cloud Deployment: We integrated Graph Neural Networks (GNNs) with Satisfiability Modulo Theory (SMT) to optimize cloud deployment plans. By learning from historical data, GNNs guide solvers to find optimal solutions faster. The approach is demonstrated with a Secure Web Container application.
    4. Binarized Neural Networks (BNNs) for Traffic Sign Recognition: We proposed BNN architectures that achieve high accuracy in traffic sign recognition, particularly in resource-constrained environments like autonomous driving systems. These models offer a balance between accuracy and computational efficiency.
    5. Robustness of BNNs for Traffic Signs: We benchmarked the robustness of BNN models in traffic sign recognition, addressing real-world challenges such as adversarial examples. The study highlights verification difficulties and suggests that extending verification time could improve results.
    6. Verification of BNNs for Traffic Sign Classification: We examined the safety risks of BNNs, focusing on adversarial examples. The outcome is that these examples need further validation to improve BNN design. Insights from the Verification of Neural Networks Competition (VNN-COMP) are also discussed.

    NEWS

    Year 2024

    Year 2023

    Year 2022

    Project Members (current and former)

    Publications and Reports

    Github Repository

    https://github.com/SAGE-Project

    Utils (only in Romanian)

    Am adunat o serie de detalii din proiect pe care mi-ar fi fost util să le cunosc atât în faza de scriere, cât şi, mai ales, în cea de implementare. Se pot găsi aici.

    Contact: Mădălina ERAŞCU.