Machine learning program verification apparatus and machine learning program verification method

A machine learning program verification method to be executed by an information processing apparatus including a storage device in which a program is stored, the program being created by machine learning, in which a value of an objective variable is output with a value of an explanatory variable as an input, in accordance with a prediction algorithm based on an ensemble tree including a plurality of decision trees, the method comprising:

• creating a decision tree logical expression by logically combining path logical expressions indicating decision tree paths in the decision trees for the program;
• creating a combined logical expression by logically combining a verification property logical expression and an objective variable calculation logical expression with the decision tree logical expression, the verification property logical expression indicating a verification property to be verified for the program, and the objective variable calculation logical expression defining a relationship between a decision tree output value of each decision tree and the value of the objective variable;
• obtaining a satisfiability determination result of the combined logical expression by inputting the combined logical expression to a predetermined satisfiability determiner, and determining, based on the satisfiability determination result, whether the program satisfies the verification property, and
• when a result of the determination indicates satisfaction, obtaining, from a satisfaction solution indicated by the satisfiability determiner, a violation input value that is a value of an explanatory variable that violates the verification property and a violation output value that is a value of an objective variable corresponding to the violation input value.