在 Coq 中形式化神经网络的逐段仿射激活函数
机器学习
2023-01-31 v1
摘要
神经网络的验证依赖于激活函数为逐段仿射(pwa)——这使得验证问题可被编码供定理证明器使用。本文首次针对交互式定理证明器给出了 pwa 激活函数的形式化,专为在 Coq 中使用 Coquelicot 实分析库验证神经网络而定制。作为概念验证,我们构造了流行的 pwa 激活函数 ReLU。我们将形式化集成至 Coq 的神经网络模型中,并设计了一种已验证的从神经网络 N 到表示 N 的 pwa 函数的转换,通过组合我们为各层构造的 pwa 函数实现。该表示支持证明自动化编码,例如 Coq 的 lra 策略——一种线性实算术判定过程。此外,我们的形式化为在神经网络验证框架中集成 Coq 作为自动证明失败时的后备证明器铺平了道路。
引用
@article{arxiv.2301.12893,
title = {Formalizing Piecewise Affine Activation Functions of Neural Networks in Coq},
author = {Andrei Aleksandrov and Kim Völlinger},
journal= {arXiv preprint arXiv:2301.12893},
year = {2023}
}