用于神经网络等价性验证的几何路径枚举
机器学习
2021-12-14 v1 人工智能
计算复杂性
计算机科学中的逻辑
摘要
随着神经网络(NN)日益引入安全关键领域，在部署前形式化验证NN的需求不断增长。本文关注NN等价性形式化验证问题，旨在证明两个NN(例如原始版本与压缩版本)表现出等价行为。针对该问题已提出两种方法：混合整数线性规划与区间传播。第一种方法缺乏可扩展性，而后者仅适用于权重变化小的结构相似NN。我们论文的贡献有四部分。首先，我们通过证明epsilon-等价问题是coNP完全的给出理论结果。其次，我们将Tran等人的单NN几何路径枚举算法扩展到多NN设定。第三步，我们实现扩展算法用于等价性验证，并评估其实用所需的优化。最后，我们进行 comparative 评估，展示在等价性验证与反例发现中我们的方法优于先前SOTA的用例。
引用
@article{arxiv.2112.06582,
title = {Geometric Path Enumeration for Equivalence Verification of Neural Networks},
author = {Samuel Teuber and Marko Kleine Büning and Philipp Kern and Carsten Sinz},
journal= {arXiv preprint arXiv:2112.06582},
year = {2021}
}
备注
Paper presented at The 33rd IEEE International Conference on Tools with Artificial Intelligence (ICTAI)