消息传递神经网络形式化验证的基本极限
机器学习
2022-10-05 v2 计算机科学中的逻辑
摘要
输出可达性与对抗鲁棒性是神经网络最相关的安全属性之一。我们表明在消息传递神经网络(MPNN)（一种常见的图神经网络(GNN)模型）背景下，形式化验证是不可能的。具体而言，我们表明在大小无界、度非平凡且节点标签具有充分表达力的图上工作的图分类器MPNN的输出可达性无法被形式化验证：不存在这样一种算法，能在给定MPNN时正确回答（是或否）是否存在对该MPNN的某有效输入使得相应输出满足给定规范。然而，我们也表明当先验给定输入图的度限制时，节点分类器MPNN的输出可达性与对抗鲁棒性可被形式化验证。我们讨论了这些结果的含义，以期根据所涉及的GNN模型与输入输出规范的表达能力，获得形式化验证GNN原则可能性的完整图景。
引用
@article{arxiv.2206.05070,
title = {Fundamental Limits in Formal Verification of Message-Passing Neural Networks},
author = {Marco Sälzer and Martin Lange},
journal= {arXiv preprint arXiv:2206.05070},
year = {2022}
}