一句话：提出 vegas，首个可扩展验证基于 GNN 的作业调度器单步与多步性质的形式化框架。
基于图神经网络（GNN）的作业调度器在集群调度中表现优于手工启发式，但其是否满足策略防操纵、共享激励、稳定性等性质仍令人担忧。本文对这类调度器进行形式化验证，并针对其网络更深、规约更丰富的领域挑战，提出 vegas：首个同时验证单步与多步性质的通用框架。vegas 将抽象、精化、求解器与证明迁移相结合，设计了可扩展算法。实验表明，与先前方法相比，vegas 在验证当前最优 GNN 调度器的关键性质时取得显著加速。
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.
@article{paperbot1439,
title = {Scalable verification of GNN-based job schedulers},
author = {Haoze Wu and Clark Barrett and Mahmood Sharif and Nina Narodytska and Gagandeep Singh},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563325}
}