基于GNN的作业调度器的可扩展验证
人工智能
2022-09-19 v4
摘要
近年来，图神经网络（GNNs）已被应用于集群上的作业调度，取得了比手工启发式方法更好的性能。尽管性能令人印象深刻，人们仍担忧这些基于GNN的作业调度器是否满足用户对其他重要属性（如防策略性、共享激励和稳定性）的期望。在本工作中，我们考虑对基于GNN的作业调度器进行形式化验证。我们解决了若干领域特有挑战，例如比验证图像和NLP分类器时更深的网络以及更丰富的规范。我们开发了vegas，这是第一个基于精心设计的算法（结合抽象、精化、求解器和证明迁移）来验证这些调度器的单步与多步属性的通用框架。实验结果表明，与先前方法相比，vegas在验证最先进的基于GNN的调度器的重要属性时实现了显著的加速。
引用
@article{arxiv.2203.03153,
title = {Scalable Verification of GNN-based Job Schedulers},
author = {Haoze Wu and Clark Barrett and Mahmood Sharif and Nina Narodytska and Gagandeep Singh},
journal= {arXiv preprint arXiv:2203.03153},
year = {2022}
}
备注
Condensed version published at OOPSLA'22