Toward Formal Data Set Verification for Building Effective Machine Learning Models

In order to properly train a machine learning model, data must be properly\ncollected. To guarantee a proper data collection, verifying that the collected\ndata set holds certain properties is a possible solution. For example,\nguaranteeing that the data set contains samples across the whole input space,\nor that the data set is balanced w.r.t. different classes. We present a formal\napproach for verifying a set of arbitrarily stated properties over a data set.\nThe proposed approach relies on the transformation of the data set into a first\norder logic formula, which can be later verified w.r.t. the different\nproperties also stated in the same logic. A prototype tool, which uses the z3\nsolver, has been developed; the prototype can take as an input a set of\nproperties stated in a formal language and formally verify a given data set\nw.r.t. to the given set of properties. Preliminary experimental results show\nthe feasibility and performance of the proposed approach, and furthermore the\nflexibility for expressing properties of interest.\n