Verification and synthesis of cyber physical systems with machine learning and constraint-solver-driven learning

Abstract

In a computer-implemented method, computer program product, and computer system, program code executing on a processor(s) generates input-output pairs, to form a training set for machine learning and generates a machine learning model of a cyber physical system by utilizing a machine learning algorithm and the training set to train the machine learning model. The program code converts the trained machine learning model into an equivalent constraint and optimizes objective functions subject to the constraint by utilizing one or more constraint solvers to compute an input-output pair. The program code determines if the computed input-output pair, is within an error tolerance and based on determining that it is, either utilizes it as a solution or adds it to the training set (and continues training). If the pair is not within the tolerance, the program code utilizes it as a solution or adds it to the training set (and continues training).