完备神经网络验证加速技术综述(形式化方法与应用)
作者:
作者单位:

1.软件研究所;2.利物浦大学


A Survey of Acceleration Techniques for Complete Neural Network Verification
  • 摘要
  • | |
  • 访问统计
  • | | |
  • 引证文献
  • | |
  • 文章评论
    摘要:

    人工智能技术已被广泛应用于生活的各个领域。然而,神经网络作为人工智能的主要实现手段,在面对训练数据之外的输入或对抗攻击时,可能表现出意料之外的行为。在自动驾驶、智能医疗等安全攸关领域,这些未定义行为可能会对生命安全造成重大威胁。因此,使用完备验证方法证明神经网络的性质,保障其行为的正确性显得尤为重要。为了提高验证效率,各种完备神经网络验证工具均提出各自的优化方法,但并未充分探索这些方法的真正起到的作用,使得后来的研究者难以找出最有效的优化方向。本综述介绍了神经网络验证领域的通用技术,并提出一个完备神经网络验证的通用框架。在此框架中,我们重点讨论了目前最先进的工具在约束求解、分支选择与边界计算这三个核心部分上的所采用的优化方法。针对各个工具本身的性能和核心加速方法,我们设计了一系列实验,旨在探究各种加速方式对于工具性能的贡献,并尝试寻找最有效的加速策略和更具潜力的优化方向,为研究者提供有价值的参考。

    Abstract:

    Artificial intelligence(AI) has been widely applied to various aspects of our lives. However, neural networks, as the primary technique of realizing AI, can exhibit undefined behavior when faced with inputs outside of their training data or under the adversarial attacks. In safety-critical domains such as autonomous driving and intelligent healthcare, these undefined behaviors could pose significant threats to human safety. Therefore, it is crucial to use complete verification methods to establish the properties of neural networks and ensure their behavior is well-understood and reliable. To enhance efficiency, various complete neural network verification tools have proposed their own optimization methods. However, the true impact of these methods has not been thoroughly explored, making it challenging for researchers to identify the most effective optimization directions. This survey introduces the common techniques in the field of neural network verification and presents a universal framework for complete neural network verification. Within this framework, we focus on discussing the optimization methods employed by the state-of-the-art tools for constraint solving, branch selection, and boundary computation. We have designed a series of experiments to investigate the contributions of various acceleration techniques to the performance of each tool and to explore the most effective acceleration strategies and more promising optimization directions. These results aim to provide valuable references for researchers in the field.

    参考文献
    相似文献
    引证文献
    引证文献 [0] 您输入的地址无效!
    没有找到您想要的资源,您输入的路径无效!

    网友评论
    网友评论
    分享到微博
    发 布
引用本文
相关视频

分享
文章指标
  • 点击次数:188
  • 下载次数: 0
  • HTML阅读次数: 0
  • 引用次数: 0
历史
  • 收稿日期:2023-09-10
  • 最后修改日期:2023-12-14
  • 录用日期:2023-12-20
文章二维码
您是第20250560位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号