kaz29Вестник Казахстанско-Британского технического университетаHerald of the Kazakh-British Technical University1998-66882959-8109Казахстанско-Британский Технический Университет10.55452/1998-6688-2026-23-2-312-325kaz29-2913Research ArticleКОМПЬЮТЕРНЫЕ НАУКИCOMPUTER SCIENCEФОРМАЛЬНАЯ ВЕРИФИКАЦИЯ СПРАВЕДЛИВОСТИ И УСТОЙЧИВОСТИ ДЕРЕВЬЕВ РЕШЕНИЙ С ПОМОЩЬЮ SMT-РЕШАТЕЛЕЙFORMAL VERIFICATION OF DECISION TREE FAIRNESS AND ROBUSTNESS VIA SMT SOLVERhttps://orcid.org/0009-0006-0845-4551БейшекеевА.BeishekeyevA.

Магистрант.

Алматы

Master’s student.

Almaty

a.beishekeyev@kbtu.kzhttps://orcid.org/0009-0008-0044-7159УмаровТ.UmarovT.

PhD.

Ташкент

PhD.

Tashkent

t.umarov@bmu.edu.kzКазахстанско-Британский технический университетКазахстанKazakh-British Technical UniversityKazakhstanБританский университет менеджментаУзбекистанBritish Management UniversityUzbekistan202627062026232312325Copyright © Бейшекеев А., Умаров Т., 20262026Бейшекеев А., Умаров Т.Beishekeyev A., Umarov T.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://vestnik.kbtu.edu.kz/jour/article/view/2913

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

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

As Artificial Intelligence systems are increasingly deployed in safety-critical domains such as healthcare and finance, ensuring their trustworthiness and compliance is paramount. While Deep Neural Networks have received significant attention in formal verification, traditional models such as Decision Trees, often preferred for their interpretability, cannot inherently enforce constraints after training for fairness and stability. This paper presents a novel, comprehensive approach for the formal verification of Decision Tree classifiers using Satisfiability Modulo Theories (SMT). We propose a robust translation scheme that converts trained decision trees into logical constraints, enabling constraint inference that guarantees demographic parity and local robustness at prediction time. We implement this framework by using the z3 SMT solver and validate it on widely recognized fairness benchmarks, including UCI Adult, German Credit, and Loan Approval datasets. Experimental results demonstrate that our constrained model effectively eliminates demographic parity violations with a marginal accuracy trade-off of less than 0.2%. This approach transforms the SMT solver from a simple diagnostic tool into a provably fair inference engine suitable for regulated industries.

машинное обучениедеревья решенийформальные методыSMTMachine LearningDecision TreesFormal MethodsSMTReferencesJiang, H., and Nachum, O. Identifying and Correcting Label Bias in Machine Learning. arXiv preprint (2019). https://doi.org/10.48550/arXiv.1901.04966Jiang, H., and Nachum, O. Identifying and Correcting Label Bias in Machine Learning. arXiv preprint (2019). https://doi.org/10.48550/arXiv.1901.04966Freiesleben, 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-9Freiesleben, 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-9Nauman, 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.3088901Nauman, 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.3088901Matsunaga, 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.00013Matsunaga, 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.00013Zhao, 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.00046Zhao, 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.00046Zhang, 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.3179659Zhang, 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.3179659Katz, 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_5Katz, 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_5Khalifa, 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.9331504Khalifa, 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.9331504Corsi, 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.htmlCorsi, 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.htmlSun, 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.331180Sun, 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.331180Yuan, 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.2886017Yuan, 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.2886017Khan, 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.9212074Khan, 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.9212074Souri, 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.2967629Souri, 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.2967629Pradhan, 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.3251841Pradhan, 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.3251841Good, 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.3251858Good, 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.3251858Krichen, 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.00025Krichen, 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.00025Dwork, 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.2090255Dwork, 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.2090255James, 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_8James, 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_8de 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_24de 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_24Pedregosa, 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.htmlPedregosa, 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.htmlBecker, B., and Kohavi, R. Adult. UCI Machine Learning Repository (1996). https://doi.org/10.24432/C5XW20Becker, B., and Kohavi, R. Adult. UCI Machine Learning Repository (1996). https://doi.org/10.24432/C5XW20Hofmann, H. Statlog (German Credit Data). UCI Machine Learning Repository (1994). https://doi.org/10.24432/C5NC77Hofmann, H. Statlog (German Credit Data). UCI Machine Learning Repository (1994). https://doi.org/10.24432/C5NC77Tawello. Loan Approval Classification Dataset. Kaggle Dataset (2023). URL: https://www.kaggle.com/datasets/taweilo/loan-approval-classification-dataTawello. Loan Approval Classification Dataset. Kaggle Dataset (2023). URL: https://www.kaggle.com/datasets/taweilo/loan-approval-classification-data

The authors declare that there are no conflicts of interest present.