Scalable verification of GNN-based job schedulers
Scalable verification of GNN-based job schedulers
复制标题
DOI：
10.1145/3563325
复制
发表时间：
2022-03
影响因子：
--
通讯作者：
Haoze Wu;Clark W. Barrett;Mahmood Sharif;Nina Narodytska;Gagandeep Singh
中科院分区：
文献类型：
--
作者：
Haoze Wu;Clark W. Barrett;Mahmood Sharif;Nina Narodytska;Gagandeep Singh
最近，图神经网络（GNN）已被应用于集群上的调度作业，实现了比手工制作的算法更好的性能。尽管他们的表现令人印象深刻，但人们仍然担心这些基于GNN的工作搜索器是否满足用户对其他重要属性的期望，例如战略防护，共享激励和稳定性。在这项工作中，我们考虑正式验证GNN为基础的工作任务。我们解决了几个特定领域的挑战，例如比验证图像和NLP分类器时遇到的更深入的网络和更丰富的规范。我们开发拉斯维加斯，第一个通用的框架，验证这些基于精心设计的算法，结合联合收割机的抽象，细化，求解器和证明转移的单步和多步属性。我们的实验结果表明，与以前的方法相比，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.