# Scalable Verification of GNN-based Job Schedulers

arXiv: https://arxiv.org/abs/2203.03153 · HTML: https://mlsanity.com/paper/2203.03153/

## Key facts

- Cited by 19 papers in the map (data through 14 Oct 2026).
- Builds on 45 of its 77 references that are in the map.
- First posted on arXiv 7 Mar 2022.

## Builds on (most cited first, 30 of 45)

- [Semi-Supervised Classification with Graph Convolutional Networks](https://mlsanity.com/paper/1609.02907/) (2016)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [A Comprehensive Survey on Graph Neural Networks](https://mlsanity.com/paper/1901.00596/) (2019)
- [Convolutional Neural Networks on Graphs with Fast Localized Spectral Filtering](https://mlsanity.com/paper/1606.09375/) (2016)
- [Graph Convolutional Neural Networks for Web-Scale Recommender Systems](https://mlsanity.com/paper/1806.01973/) (2018)
- [Convolutional Networks on Graphs for Learning Molecular Fingerprints](https://mlsanity.com/paper/1509.09292/) (2015)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Provable defenses against adversarial examples via the convex outer adversarial polytope](https://mlsanity.com/paper/1711.00851/) (2017)
- [Learning Combinatorial Optimization Algorithms over Graphs](https://mlsanity.com/paper/1704.01665/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Learning Convolutional Neural Networks for Graphs](https://mlsanity.com/paper/1605.05273/) (2016)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Adversarial Attacks on Graph Neural Networks via Meta Learning](https://mlsanity.com/paper/1902.08412/) (2019)
- [Towards Fast Computation of Certified Robustness for ReLU Networks](https://mlsanity.com/paper/1804.09699/) (2018)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Semidefinite relaxations for certifying robustness to adversarial examples](https://mlsanity.com/paper/1811.01057/) (2018)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [Learning Scheduling Algorithms for Data Processing Clusters](https://mlsanity.com/paper/1810.01963/) (2018)
- [A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks](https://mlsanity.com/paper/1902.08722/) (2019)
- [Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks](https://mlsanity.com/paper/1708.03322/) (2017)
- [Towards More Practical Adversarial Attacks on Graph Neural Networks](https://mlsanity.com/paper/2006.05057/) (2020)
- [Verification of Deep Convolutional Neural Networks Using ImageStars](https://mlsanity.com/paper/2004.05511/) (2020)
- [Lyapunov-stable neural-network control](https://mlsanity.com/paper/2109.14152/) (2021)
- [Certifiable Robustness to Graph Perturbations](https://mlsanity.com/paper/1910.14356/) (2019)
- [Certified Robustness of Graph Neural Networks against Adversarial Structural Perturbation](https://mlsanity.com/paper/2008.10715/) (2020)
- [Learning to schedule job-shop problems: Representation and policy learning using graph neural network and reinforcement learning](https://mlsanity.com/paper/2106.01086/) (2021)
- [CNN-Cert: An Efficient Framework for Certifying Robustness of Convolutional Neural Networks](https://mlsanity.com/paper/1811.12395/) (2018)

## Built on by (most cited first, 19 of 19)

- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [The Third International Verification of Neural Networks Competition (VNN-COMP 2022): Summary and Results](https://mlsanity.com/paper/2212.10376/) (2022)
- [VeriX: Towards Verified Explainability of Deep Neural Networks](https://mlsanity.com/paper/2212.01051/) (2022)
- [Provably Bounding Neural Network Preimages](https://mlsanity.com/paper/2302.01404/) (2023)
- [Toward Certified Robustness Against Real-World Distribution Shifts](https://mlsanity.com/paper/2206.03669/) (2022)
- [Verifying message-passing neural networks via topology-based bounds tightening](https://mlsanity.com/paper/2402.13937/) (2024)
- [Formal Verification of Graph Convolutional Networks with Uncertain Node Features and Uncertain Graph Structure](https://mlsanity.com/paper/2404.15065/) (2024)
- [A Scalable, Interpretable, Verifiable & Differentiable Logic Gate Convolutional Neural Network Architecture From Truth Tables](https://mlsanity.com/paper/2208.08609/) (2022)
- [AutoSpec: Automated Generation of Neural Network Specifications](https://mlsanity.com/paper/2409.10897/) (2024)
- [Bridging Efficiency and Safety: Formal Verification of Neural Networks with Early Exits](https://mlsanity.com/paper/2512.20755/) (2025)
- [The FABRIC Strategy for Verifying Neural Feedback Systems](https://mlsanity.com/paper/2603.08964/) (2026)
- [Specification Generation for Neural Networks in Systems](https://mlsanity.com/paper/2412.03028/) (2024)
- [The Luna Bound Propagator for Formal Analysis of Neural Networks](https://mlsanity.com/paper/2603.23878/) (2026)
- [Analyzing Symbolic Properties for DRL Agents in Systems and Networking](https://mlsanity.com/paper/2604.04914/) (2026)
- [Towards Verified and Targeted Explanations through Formal Methods](https://mlsanity.com/paper/2604.14209/) (2026)
- [Neural Network Verification using Partial Multi-Neuron Relaxation](https://mlsanity.com/paper/2605.30155/) (2026)
- [NNV3: Expanding Neural Network Verification to New Architectures and Domains](https://mlsanity.com/paper/2609.30050/) (2026)
- [Reachability-Based Formal Verification of Graph Neural Networks with Node and Edge Features](https://mlsanity.com/paper/2609.30079/) (2026)
- [Jumping the Line: Exploiting Length Predictions in LLM Scheduling](https://mlsanity.com/paper/2610.03430/) (2026)

## Abstract (arXiv)

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.