遞迴神經網絡（RNNs）的認證式局部強健性驗證是一個困難的問題，因為非線性近似所引入的近似誤差會透過遞迴連結傳遞，並隨時間累積。因此，可擴展的線性邊界近似往往過於保守，無法驗證成功實際上安全的輸入，尤其當許多預激活區間帶有較大的近似誤差時更為明顯。本研究提出一套適用於RNN驗證的抽象精煉框架，透過切割這類區間，在每個分支上消除主要的近似誤差。對於RELU，於零點切割可使分支變為精確；對於TANH、SIGMOID等平滑激活函數(同時也出現在LSTM的閘門中)，我們選擇能最小化過度近似面積的切點p*，並以離線預先計算、驗證時以查表方式取得。為控制長序列中切割的組合成本，我們提出以SHAP為導向的選擇策略，依各隱藏層神經元對驗證目標的貢獻排序，再依時序對最關鍵者進行精煉。在CIFAR10、MNIST stroke 與 MNIST 上、橫跨 vanilla RNN 與 LSTM 的實驗顯示，本方法相較於僅用抽象的基準，在驗證成功率與強健性邊界緊度上都有一致提升，同時呈現出RELU與平滑激活函數模型之間明確的執行時間取捨。

Certified robustness verification for recurrent neural networks (RNNs) is hard because relaxation errors from nonlinear activations propagate through the recurrence and accumulate, leaving linear bound propagation too conservative to certify many robust inputs. We propose an abstraction-refinement framework that splits over-approximated pre-activation intervals to cut the dominant relaxation error per branch: at zero for RELU, making it exact, and at an offline-computed point p* for TANH and SIGMOID, retrieved by table lookup. A SHAP-guided strategy keeps splitting tractable by refining only the most critical neurons in temporal order. Across CIFAR10, MNIST stroke, and MNIST on RNNs and LSTMs, our method consistently improves verification success and bound tightness over abstraction-only baselines.

Alahi, A., Goel, K., Ramanathan, V., Robicquet, A., Fei-Fei, L., and Savarese, S. (2016). Social lstm: Human trajectory prediction in crowded spaces. In IEEE Conference on Computer Vision and Pattern Recognition (CVPR), pages 961–971.

Bunel, R., Lu, J., Turkaslan, I., Torr, P. H. S., Kohli, P., and Kumar, M. P. (2020). Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research, 21(42):1–39.

Che, Z., Purushotham, S., Cho, K., Sontag, D., and Liu, Y. (2018). Recurrent neural networks for multivariate time series with missing values. Scientific Reports, 8(1):6085.

Cherny, D., Herasymenko, V., and Semenov, A. (2018). Adversarial machine learning in credit card fraud detection. In IEEE International Conference on Data Stream Mining & Processing (DSMP), pages 351–355.

Cohen, J., Rosenfeld, E., and Kolter, Z. (2019). Certified adversarial robustness via randomized smoothing. In International Conference on Machine Learning (ICML), pages 1310–1320.

Cousot, P. and Cousot, R. (1977). Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 238–252.

De Palma, A., Bunel, R., Desmaison, A., Dvijotham, K., Kohli, P., Torr, P. H., and Kumar, M. P. (2021). Improved branch and bound for neural network verification via lagrangian decomposition. arXiv preprint arXiv:2104.06718.

Du, T., Ji, S., Shen, L., Zhang, Y., Li, J., Shi, J., Fang, C., Yin, J., Beyah, R., and Wang, T. (2021). Cert-rnn: Towards certifying the robustness of recurrent neural networks. In Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security (CCS), pages 516–534.

Du, X., Li, Y., Xie, X., Ma, L., Liu, Y., and Zhao, J. (2020). Marble: Model-based robustness analysis of stateful deep learning systems. In Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering (ASE).

Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., and Vechev, M. (2018). Ai2: Safety and robustness certification of neural networks with abstract interpretation. In IEEE Symposium on Security and Privacy (SP), pages 3–18.

Goodfellow, I. J., Shlens, J., and Szegedy, C. (2015). Explaining and harnessing adversarial examples. In International Conference on Learning Representations (ICLR).

Graves, A., Mohamed, A.-r., and Hinton, G. (2013). Speech recognition with deep recurrent neural networks. In IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP), pages 6645–6649.

Hardy, G. H., Littlewood, J. E., and Pólya, G. (1952). Inequalities. Cambridge University Press, Cambridge, 2nd edition.

Hochreiter, S. and Schmidhuber, J. (1997). Long short-term memory. Neural computation, 9(8):1735–1780.

Katz, G., Barrett, C., Dill, D. L., Julian, K., and Kochenderfer, M. J. (2017). Reluplex: An efficient smt solver for verifying deep neural networks. In Computer Aided Verification (CAV), pages 97–117. Springer.

Katz, G., Barrett, C., Dill, D. L., Julian, K., and Kochenderfer, M. J. (2019). The marabou framework for verification and analysis of deep neural networks. In Computer Aided Verification (CAV), pages 443–452. Springer.

Ko, C.-Y., Lyu, Z., Weng, L., Daniel, L., Wong, N., and Lin, D. (2019). Popqorn: Quantifying robustness of recurrent neural networks. In International Conference on Machine Learning (ICML), pages 3468–3477. PMLR.

Li, J., Bai, G., Pham, L. H., and Sun, J. (2023). Towards an effective and interpretable refinement approach for dnn verification. In IEEE International Conference on Software Quality, Reliability, and Security (QRS), pages 569–580. IEEE.

Li, Y., Wen, C., Juefei-Xu, F., and Feng, C. (2021). Fooling lidar perception via adversarial trajectory perturbation. In Proceedings of the IEEE/CVF International Conference on Computer Vision (ICCV), pages 7898–7907.

Liwicki, M., Graves, A., Bunke, H., and Schmidhuber, J. (2012). Recognition of whiteboard notes: Online, offline and combination. In Series in Machine Perception and Artificial Intelligence, volume 75, pages 1–13. World Scientific.

Lundberg, S. M. and Lee, S.-I. (2017). A unified approach to interpreting model predictions. In Advances in Neural Information Processing Systems, pages 4765–4774.

Madry, A., Makelov, A., Schmidt, L., Tsipras, D., and Vladu, A. (2017). Towards deep learning models resistant to adversarial attacks. arXiv preprint arXiv:1706.06083.

Mohammadinejad, S., Paulsen, B., Deshmukh, J. V., and Wang, C. (2021). Diffrnn: Differential verification of recurrent neural networks. In International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), pages 117–134.

Nelson, D. M., Pereira, A. C., and de Oliveira, R. A. (2017). Stock market’s price movement prediction with lstm neural networks. In Proceedings of the International Joint Conference on Neural Networks (IJCNN), pages 1419–1426.

Ryou, W., Chen, J., Balunovic, M., Singh, G., Dan, A., and Vechev, M. (2021). Scalable polyhedral verification of recurrent neural networks. In International Conference on Computer Aided Verification (CAV), pages 225–248. Springer.

Shi, Z., Jin, Q., Kolter, Z., Jana, S., Hsieh, C.-J., and Zhang, H. (2025). Neural network verification with branch-and-bound for general nonlinearities. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 15696 of Lecture Notes in Computer Science, pages 315–335. Springer.

Singh, G., Gehr, T., Mirman, M., Püschel, M., and Vechev, M. (2019). An abstract domain for certifying neural networks. In Proceedings of the ACM on Programming Languages (POPL), volume 3, pages 1–30.

Singh, G., Gehr, T., Püschel, M., and Vechev, M. (2018). Fast and precise certification of neural networks. In Advances in Neural Information Processing Systems (NeurIPS), pages 10802–10813.

Sundararajan, M., Taly, A., and Yan, Q. (2017). Axiomatic attribution for deep networks.

Sutskever, I., Vinyals, O., and Le, Q. V. (2014). Sequence to sequence learning with neural networks. In Advances in Neural Information Processing Systems (NeurIPS), pages 3104–3112.

Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I., and Fergus, R. (2013). Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199.

Tran, H.-D., Choi, S., Yang, X., Yamaguchi, T., Hoxha, B., and Prokhorov, D. (2023). Verification of recurrent neural networks with star reachability. In Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control (HSCC), pages 1–13.

Wang, S., Zhang, H., Xu, K., Lin, X., Jana, S., Hsieh, C.-J., and Kolter, J. Z. (2021). Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. In Advances in Neural Information Processing Systems (NeurIPS), volume 34, pages 29909–29921.

Xu, K., Zhang, H., Wang, S., Wang, Y., Jana, S., Lin, X., and Hsieh, C.-J. (2021). Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. In International Conference on Learning Representations (ICLR).

Zhang, H., Weng, T.-W., Chen, P.-Y., Hsieh, C.-J., and Daniel, L. (2018). Efficient neural network robustness certification with general activation functions. In Advances in Neural Information Processing Systems (NeurIPS), pages 4939–4948.

Zhang, Y., Albarghouthi, A., and D’Antoni, L. (2021). Certified robustness to programmable transformations in lstms. In Proceedings of the 2021 Conference on Empirical Methods in Natural Language Processing (EMNLP), pages 1068–1083.

Zhang, Y., Du, T., Ji, S., Tang, P., and Guo, S. (2023). Rnn-guard: Certified robustness against multi-frame attacks for recurrent neural networks. arXiv preprint arXiv:2304.07980.

Zhou, D., Brix, C., Hanasusanto, G. A., and Zhang, H. (2024). Scalable neural network verification with branch-and-bound inferred cutting planes. In NeurIPS.