不动点迭代器的抽象解释及其在神经网络中的应用
机器学习
2023-04-27 v2 人工智能
摘要
我们提出了一种新的抽象解释框架，用于数值不动点迭代器的精确过近似。我们的关键观察是，与通常用于过近似所有可达程序状态的标准抽象解释（AI）不同，在此设定下，只需对具体不动点（即最终程序状态）进行抽象。我们的框架面向在具体内容上具有收敛性和唯一性保证的数值不动点迭代器，并基于两项主要技术贡献：（i）允许我们在不使用连接（join）的情况下计算可靠且精确的不动点抽象的理论见解；（ii）一种新的抽象域 CH-Zonotope，它支持高效的传播和包含检查，同时保持高精度。我们在一个名为 CRAFT 的工具中实现了我们的框架，并在一种新颖的基于不动点的神经网络架构（monDEQ）上进行了评估，该架构尤其难以验证。我们广泛的评估表明，CRAFT 在速度（两个数量级）、可扩展性（一个数量级）和精度（认证准确率提高 25%）方面均超越了最先进水平。
引用
@article{arxiv.2110.08260,
title = {Abstract Interpretation of Fixpoint Iterators with Applications to Neural Networks},
author = {Mark Niklas Müller and Marc Fischer and Robin Staab and Martin Vechev},
journal= {arXiv preprint arXiv:2110.08260},
year = {2023}
}
备注
PLDI'23: 44th ACM SIGPLAN International Conference on Programming Language Design and Implementation