ФОРМАЛЬНАЯ ВЕРИФИКАЦИЯ СПРАВЕДЛИВОСТИ И УСТОЙЧИВОСТИ ДЕРЕВЬЕВ РЕШЕНИЙ С ПОМОЩЬЮ SMT-РЕШАТЕЛЕЙ

Поскольку системы искусственного интеллекта все чаще внедряются в критически важных для безопасности сферах, таких как здравоохранение и финансы, обеспечение их надежности и соблюдения требований крайне важно. В то время как глубокие нейронные сети получили значительное внимание в формальной верификации, традиционные модели, такие как деревья решений, часто предпочитаемые за их интерпретируемость, не могут по умолчанию навязывать ограничения после обучения на справедливость и стабильность.

В данной статье представлен новый, комплексный подход к формальной проверке классификаторов дерева принятия решений с использованием теорий по модулю удовлетворения (SMT). Мы предлагаем надежную схему трансляции, которая преобразует обученные деревья принятия решений в логические ограничения, позволяя делать вывод по ограничениям, гарантирующий демографический паритет и локальную устойчивость во время прогнозирования. Мы реализуем эту структуру с помощью решателя z3 SMT и проверяем его по широко признанным стандартам справедливости, включая наборы данных UCI Adult, German Credit и Loan Approval. Экспериментальные результаты показывают, что наша ограниченная модель эффективно исключает нарушения демографического паритета с предельной точностью менее 0,2%. Этот подход превращает решатель SMT из простого диагностического инструмента в доказуемо справедливый движок выводов, подходящий для регулируемых отраслей.

1. Jiang, H., and Nachum, O. Identifying and Correcting Label Bias in Machine Learning. arXiv preprint (2019). https://doi.org/10.48550/arXiv.1901.04966

2. Freiesleben, T., and Grote, T. Beyond generalization: A theory of robustness in machine learning. Synthese, 202 (4), Article 109 (2023). https://doi.org/10.1007/s11229-023-04334-9

3. Nauman, M., Akhtar, N., Alhudhaif, A., and Alothaim, A. Guaranteeing Correctness of Machine Learning Based Decision Making at Higher Educational Institutions. IEEE Access, 9, 92864–92880 (2021). https://doi.org/10.1109/ACCESS.2021.3088901

4. Matsunaga, S., and Yoshimura, G. Efficient and High-Quality Formal Verification for Decision Tree Ensembles. In: 2024 IEEE International Conference on Data Mining Workshops (ICDMW), pp. 51–58 (2024). https://doi.org/10.1109/ICDMW65004.2024.00013

5. Zhao, L., Wu, L., Gao, Y., Wang, X., and Yu, B. Formal Modeling and Verification of Convolutional Neural Networks based on MSVL. In: 2022 9th International Conference on Dependable Systems and Their Applications (DSA), pp. 280–289 (2022). https://doi.org/10.1109/DSA56465.2022.00046

6. Zhang, Z., Liu, J., Liu, G., Wang, J., and Zhang, J. Robustness Verification of Swish Neural Networks Embedded in Autonomous Driving Systems. IEEE Transactions on Computational Social Systems, 10 (4), 2041–2050 (2023). https://doi.org/10.1109/TCSS.2022.3179659

7. Katz, G., Barrett, C., Dill, D.L., Julian, K., and Kochenderfer, M.J. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In: Majumdar, R., Kunčak, V. (eds.) Computer Aided Verification. Cham: Springer, pp. 97–117 (2017). https://doi.org/10.1007/978-3-319-63387-9_5

8. Khalifa, K., Safar, M., and El-Kharashi, M.W. Verification of Neural Networks for Safety Critical Applications. In: 2020 32nd International Conference on Microelectronics (ICM), pp. 1–4 (2020). https://doi.org/10.1109/ICM50269.2020.9331504

9. Corsi, D., Marchesini, E., and Farinelli, A. Formal verification of neural networks for safety-critical tasks in deep reinforcement learning. In: Proceedings of the Thirty-Seventh Conference on Uncertainty in Artificial Intelligence, pp. 333–343 (2021). URL: https://proceedings.mlr.press/v161/corsi21a.html

10. Sun, X., Khedr, H., and Shoukry, Y. Formal verification of neural network controlled autonomous systems. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pp. 147–156 (2019). https://doi.org/10.1145/3302504.331180

11. Yuan, X., He, P., Zhu, Q., and Li, X. Adversarial Examples: Attacks and Defenses for Deep Learning. IEEE Transactions on Neural Networks and Learning Systems, 30 (9), 2805–2824 (2019). https://doi.org/10.1109/TNNLS.2018.2886017

12. Khan, M.T., Serpanos, D., Shrobe, H., and Yousuf, M.M. Rigorous Machine Learning for Secure and Autonomous Cyber Physical Systems. In: 2020 25th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA), Vol. 1, pp. 1815–1819 (2020). https://doi.org/10.1109/ETFA46521.2020.9212074

13. Souri, A., Mohammed, A.S., Potrus, M.Y., Malik, M.H., Safara, F., and Hosseinzadeh, M. Formal Verification of a Hybrid Machine Learning-Based Fault Prediction Model in Internet of Things Applications. IEEE Access, 8, 23863–23874 (2020). https://doi.org/10.1109/ACCESS.2020.2967629

14. Pradhan, A., King, J., Pinisetty, S., and Roop, P.S. Model Based Verification of Spiking Neural Networks in Cyber Physical Systems. IEEE Transactions on Computers, 72 (9), 2426–2439 (2023). https://doi.org/10.1109/TC.2023.3251841

15. Good, J.H., Gisolfi, N., Miller, K., and Dubrawski, A. Verification of Fuzzy Decision Trees. IEEE Transactions on Software Engineering, 49 (5), 3277–3288 (2023). https://doi.org/10.1109/TSE.2023.3251858

16. Krichen, M., Mihoub, A., Alzahrani, M.Y., Adoni, W.Y.H., and Nahhal, T. Are Formal Methods Applicable To Machine Learning And Artificial Intelligence? In: 2022 2nd International Conference of Smart Systems and Emerging Technologies (SMARTTECH), pp. 48–53 (2022). https://doi.org/10.1109/SMARTTECH54121.2022.00025

17. Dwork, C., Hardt, M., Pitassi, T., Reingold, O., and Zemel, R. Fairness through awareness. In: Proceedings of the 3rd Innovations in Theoretical Computer Science Conference, pp. 214–226 (2012). https://doi.org/10.1145/2090236.2090255

18. James, G., Witten, D., Hastie, T., Tibshirani, R., and Taylor, J. Tree-Based Methods. In: An Introduction to Statistical Learning. Cham: Springer, pp. 331–366 (2023). https://doi.org/10.1007/978-3-031-38747-0_8

19. de Moura, L., and Bjørner, N. Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer, pp. 337–340 (2008). https://doi.org/10.1007/978-3-540-78800-3_24

20. Pedregosa, F., Varoquaux, G., Gramfort, A., Michel, V., Thirion, B., Grisel, O., Blondel, M., Prettenhofer, P., Weiss, R., Dubourg, V., VanderPlas, J., Passos, A., Cournapeau, D., Brucher, M., Perrot, M., and Duchesnay, É. Scikit-learn: Machine Learning in Python. Journal of Machine Learning Research, 12, 2825–2830 (2011). URL: http://jmlr.org/papers/v12/pedregosa11a.html

21. Becker, B., and Kohavi, R. Adult. UCI Machine Learning Repository (1996). https://doi.org/10.24432/C5XW20

22. Hofmann, H. Statlog (German Credit Data). UCI Machine Learning Repository (1994). https://doi.org/10.24432/C5NC77

23. Tawello. Loan Approval Classification Dataset. Kaggle Dataset (2023). URL: https://www.kaggle.com/datasets/taweilo/loan-approval-classification-data