基于 Softplus 函数的神经网络的 Reluplex 算法验证研究

信息安全研究 ›› 2022, Vol. 8 ›› Issue (9): 917-.

基于 Softplus 函数的神经网络的 Reluplex 算法验证研究

陆明远, 侯春燕, 王劲松

(天津理工大学计算机科学与工程学院天津300384)

出版日期:2022-09-02 发布日期:2022-09-02
通讯作者: 陆明远硕士.主要研究方向为软件形式化验证方法、人工神经网络和信息安全. 1933044495@qq.com
作者简介:陆明远硕士.主要研究方向为软件形式化验证方法、人工神经网络和信息安全. 1933044495@qq.com 侯春燕博士，副教授，硕士生导师.主要研究方向为软件形式化验证方法、软件漏洞挖掘、软件测试和机器深度学习. chunyanhou@tjut.edu.cn 王劲松博士，教授，博士生导师.主要研究方向为人工智能、数据挖掘、区块链和信息安全. jswang@tjut.edu.cn

Research on Verification of Neural Network Based on Softplus Function by Reluplex Algorithm

Online:2022-09-02 Published:2022-09-02

摘要/Abstract

摘要： 形式化验证是计算机科学中运用数理逻辑的方式验证某个系统是否可行的方法，而把形式化验证方法充分应用于神经网络领域，则能更好地研究神经网络的特性与应用.Reluplex是一种对深度神经网络进行验证的单纯形算法，它使用Relu作为激活函数，而Relu的神经元在训练过程中较脆弱并可能垂死.Softplus是与Relu近似但比Relu更平滑的激活函数，改进了Reluplex算法使之能检验采用Softplus激活函数的深度神经网络，随后获取了在Softplus激活函数下测试鲁棒对抗性得到的实验数据结果，通过与Relu测试结果进行对比，证明了Softplus的测试效率明显高于Relu，它比Relu更平衡，从而让神经网络的学习更快.该研究扩展了神经网络验证算法的功能并展开了相应的对比分析，有利于以后更好地验证和改进深度神经网络，以确保其安全性.

关键词: 神经网络, 形式化验证, 激活函数, Relu函数, Softplus函数

Abstract: Formal verification is a method in computer science that uses mathematical logic to verify whether a system is feasible. Applying formal verification methods to the field of neural networks fully can facilitate us to study the characteristics and applications of neural networks better. Reluplex is a kind of simplex algorithm for verifying deep neural networks which uses Relu as the activation function, and neurons of Relu are fragile and may die during training. Softplus is an activation function similar to Relu but smoother than it. We improved the Reluplex algorithm to test deep neural networks which is using Softplus activation function, and then obtained experimental data results by testing robust adversarial under Softplus activation function. Through the comparison with the test results under Relu, it is confirmed that test efficiency under Softplus is significantly higher than that of Relu, which is more balanced than Relu so that the neural network can learn faster. This study expands the functions of the neural network verification algorithm and conducts a corresponding comparative analysis, which is beneficial to better verify and improve deep neural networks to ensure its security in the future.

Key words: neural network, formal verification, activation function, Relu, Softplus

陆明远, 侯春燕, 王劲松. 基于 Softplus 函数的神经网络的 Reluplex 算法验证研究[J]. 信息安全研究, 2022, 8(9): 917-.

参考文献

［1］Seligman E, Schubert E T, Kirankumar M. Formal Verification: An Essential Toolkit for Modern VLSI Design［M］. Amsterdam: Elsevier Science, 2015［2］朱红章, 李连艳, 任晓斌, 等. 基于PCR和RBF神经网络的城市智能增长水平评价模型［J］. 计算机与现代化, 2020, 8(5): 1521, 28［3］管建池, 肇莹, 刘红星. 优化神经元激活函数类型的重要性［J］. 济南大学学报: 自然科学版, 2005, 19(3): 282282［4］叶小舟, 陶飞飞, 戚荣志, 等. 循环神经网络结构中激活函数的改进［J］. 计算机与现代化, 2016, 5(12): 2933［5］Brinkmann R, Kelf D. Formal verification—The industrial perspective［M］ Formal System Verification. Berlin: Springer, 2017: 155182［6］Drechsler R. Advanced Formal Verification［M］. Amsterdam: Kluwer Academic Publishers, 2004［7］焦李成. 神经网络系统理论［M］. 西安: 西安电子科技大学出版社, 1990［8］刘豹, 胡代平. 神经网络在预测中的一些应用研究［J］. 系统工程学报, 1999, 14(4): 338344［9］张行. 人工智能在手写签字鉴定应用中的研究［J］. 信息安全研究, 2020, 6(7): 622633［10］Katz G, Barrett C, Dill D L, et al. Reluplex: An efficient SMT solver for verifying deep neural networks［G］ LNCS 10426: Proc of Int Conf on Computer Aided Verification. Berlin: Springer, 2017: 97117［11］Zhang Daiyuan, Zhang Hao. Computational complexity of training algorithm for a kind of neural network［J］. Applied Mechanics and Materials, 2014, 644645647648649650: 24032406［12］Liang Xinglong, Xu Jun. Biased ReLU neural networks［J］. Neurocomputing, 2021, 423(3): 7179［13］Annema A. Learning behavior and temporary minima of twolayer neural networks［J］. FeedForward Neural Networks, 1995, 7(9): 107145［14］Masahiro N. An artificial neuron model with a periodic activation function［M］ Chaos and Fractals in Engineering, Singapore: World Scientific, 1999: 239267［15］胡耀垓, 李伟, 胡继明. 一种改进激活函数的人工神经网络及其应用［J］. 武汉大学学报: 信息科学版, 2004, 29(10): 916919［16］Zheng Hao, Yang Zhanlei, Liu Wenju, et al. Improving deep neural networks using Softplus units［C］ Proc of Int Joint Conf on Neural Networks (IJCNN). Piscataway, NJ: IEEE, 2015: 114［17］Zhao Huizhen, Liu Fuxian, Li Longyue, et al. A novel Softplus linear unit for deep convolutional neural networks［J］. Applied Intelligence, 2017, 48(9): 17071720［18］李晓峰, 徐玖平, 王荫清, 等. BP人工神经网络自适应学习算法的建立及其应用［J］. 系统工程理论与实践, 2004, 24(5): 18［19］高隽. 人工神经网络原理及仿真实例［M］. 北京: 机械工业出版社, 2003［20］Qian L, Furber S. Noisy Softplus: A biology inspired activation function［C］ Proc of Int Conf on Neural Information Processing. Berlin: Springer, 2016: 405412［21］李松, 刘力军, 翟曼. 改进粒子群算法优化BP神经网络的短时交通流预测［J］. 系统工程理论与实践, 2012, 32(9): 20452049［22］Graupe D. Deep Learning Neural Networks: Design and Case Studies［M］. Singapore: World Scientific, 2016［23］Zhang Lu, Tan Jianjun, Han Dan, et al. From machine learning to deep learning: Progress in machine intelligence for rational drug discovery［J］. Drug Discovery Today, 2017, 22(11): 16801685［24］Chen C L, Zhang Chunyang, Chen Long, et al. Fuzzy restricted Boltzmann machine for the enhancement of deep learning［J］. IEEE Trans on Fuzzy Systems, 2015, 23(6): 21632173［25］罗运鑫, 佘堃, 于钥, 等. 基于忆阻神经网络的车辆标志识别技术研究［J］. 信息安全研究, 2017, 3(8): 715727［26］Deng Li, Yu Dong. Deep Learning: Methods and Applications［M］. Amsterdam: Now Publishers Incorporation, 2014［27］Patil V, Jaware T, Badgujar R. Artificial Neural Network［M］. Dusseldorf, Germany: LAP Lambert Academic Publication, 2019