发表机构
Leiden Institute of Advanced Computer Science, Leiden; University of Oxford; RWTH Aachen University; University of British Columbia（莱顿大学高级计算机科学研究所; 牛津大学; 亚琛工业大学; 不列颠哥伦比亚大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本研究探索求解器级热启动方法，利用先前解信息加速神经网络验证，实验表明可显著减少运行时间并解决超时实例。
AI 中文摘要
神经网络验证已成为对神经网络行为提供形式化保证的关键工具。然而，许多验证问题在最坏情况下在计算上仍然难以处理：即使对于常见的对抗鲁棒性规范，验证也是NP完全的。在此，我们探索将求解器级热启动应用于神经网络验证，以利用先前解决方案的信息。我们研究当若干属性被修改时（包括扰动半径、输入数据以及网络本身）对运行时间的影响，使用一个可泛化且可能适用于最先进验证器的流水线。我们的结果表明，在大多数情况下，热启动可以显著减少验证时间。此外，热启动使得在给定时间限制内无法从头解决的实例能够成功验证。
英文摘要
Neural network verification has become a key tool for providing formal guarantees on the behaviour of neural networks. However, many verification problems remain computationally intractable in the worst case: even for common adversarial robustness specifications, verification is NP-complete. Here, we explore the application of solver-level warmstarting for neural network verification to exploit information from previous solutions. We study the effect on running time as several properties are modified, including perturbation radii, input data and the networks themselves, using a pipeline that is generalisable and potentially adaptable to state-of-the-art verifiers. Our results show that warmstarting can significantly reduce verification time in most cases. Moreover, warmstarting enables the successful verification of instances that could not be solved from scratch within the given time limit.
Commentsto be published in the postproceedings of WORKSHOP ON SECURE AND TRUSTWORTHY AI (2026) co-located with the European Conference on Machine Learning and Principles and Practice of Knowledge Discovery in Databases
