Research On Local Interpretability Of Random Forest Based On Satisfiability Module Theory

In recent years,machine learning has shown its great development prospects in the field of security because of its superior computing power.At the same time,the interpretability of machine learning has also become a key concern.Interpretability can reveal the decision-making principle of machine learning,enhance its reliability and help optimize the model.It has great significance.However,at present,most methods for interpretability still regard machine learning model as black box model and do not go deep into the model for internal analysis,which has great limitations.Because of its nonlinear structure,tree model is more difficult to be analyzed than neural network model,and there is little interpretability analysis for tree model.Therefore,interpretability analysis for tree model is also a huge challenge.Equipped with characteristic of rigorous logic,formal methods have been widely used in the verification of machine learning properties.Based on this,this paper does researches on the local interpretability of random forest based on formal methods,mainly focusing on the feature importance of samples and counterfactual samples generation.Specifically,this paper makes three novel contributions:1.In this paper,a coding method of random forest decision-making process based on satisfiability module theory is proposed,which can intuitively understand the internal operation mode of random forest2.In this paper,the concept of abductive interpretation based on minimal unsatisfiable core is proposed.The SMT solver is used to analyze and solve the coded random forest decision formula.According to the minimal unsatisfiable core calculated,it can reflect the characteristics that have an important impact on the prediction results of samples in the decision-making process.The experimental results show the feasibility and accuracy of using the formal method to deeply analyze the interpretability problems of the model.3.In this paper,an optimal counterfactual sample generation method based on minimal unsatisfiable core is put forward.It provides new insight for counterfactual analysis.The experimental results prove the superior performance and good results.The real loan data set is used for case analysis to provide appropriate and easy to implement suggestions for users who fail to make loans,that is,to improve users' application conditions according to counterfactual samples,so as to make the next loan successful,so as to show its practicability in reality.The interpretability method based on formal method can go deep into the model for analysis,which introduces a new perspective for the analysis of black box model.Simultaneously,it gives new value to the minimal unsatisfiable core in the satisfiability module theory,that is,it can analyze and study the interpretability of machine learning from two different angles according to the minimal unsatisfiable core,which provides a new and practical interpretable method for the field of interpretability.