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 their trustworthiness when deployed in a real-world environment due to their black-box nature. To address these limitations, we consider formal verification of their expected properties such as strategy proofness and locality in this work. We address several domain-specific challenges such as deeper networks and richer specifications not encountered by existing verifiers for image and NLP classifiers. We develop GNN-Verify, 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 on challenging benchmarks show that our approach can provide precise and scalable formal guarantees on the trustworthiness of state-of-the-art GNN-based scheduler.

本文针对基于GNN的作业调度器在满足性能方面表现卓越的同时，关注其是否满足用户在战略稳健性、共享激励和稳定性等其他重要特性方面的期望，提出了一种用于验证GNN作业调度器的通用框架vegas，并通过实验证明其比之前的方法更快速且更为精准。

基于GNN的工作调度程序的可扩展验证