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