Scalable Verification of GNN-based Job Schedulers

Abstract

Recently, Graph Neural Networks (GNNs) have been applied for scheduling jobs over clusters, achieving better performance than hand-crafted heuristics. Despite their impressive performance, concerns remain over whether these GNN-based job schedulers meet users' expectations about other important properties, such as strategy-proofness, sharing incentive, and stability. In this work, we consider formal verification of GNN-based job schedulers. We address several domain-specific challenges such as networks that are deeper and specifications that are richer than those encountered when verifying image and NLP classifiers. We develop vegas, the first general framework for verifying both single-step and multi-step properties of these schedulers based on carefully designed algorithms that combine abstractions, refinements, solvers, and proof transfer. Our experimental results show that vegas achieves significant speed-up when verifying important properties of a state-of-the-art GNN-based scheduler compared to previous methods.

arXiv commentCondensed version published at OOPSLA'22

References in corpus (16)

• A Comprehensive Survey on Graph Neural Networks
• Intriguing properties of neural networks
• Graph Convolutional Neural Networks for Web-Scale Recommender Systems
• Provable defenses against adversarial examples via the convex outer adversarial polytope
• Learning to schedule job-shop problems: Representation and policy learning using graph neural network and reinforcement learning
• Formal Security Analysis of Neural Networks using Symbolic Intervals
• Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness
• Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers
• Deep Neural Networks as 0-1 Mixed Integer Linear Programs: A Feasibility Study
• The Convex Relaxation Barrier, Revisited: Tightened Single-Neuron Relaxations for Neural Network Verification
• Branch and Bound for Piecewise Linear Neural Network Verification
• Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees
• Towards Scalable Verification of Deep Reinforcement Learning
• Online Learning Demands in Max-min Fairness
• Improving Neural Network Verification through Spurious Region Guided Refinement
• Fast Geometric Projections for Local Robustness Certification

Cited by in corpus (2)

• Automated Verification of Soundness of DNN Certifiers
• Reachability-Based Formal Verification of Graph Neural Networks with Node and Edge Features