Toward Formal Data Set Verification for Building Effective Machine Learning Models
This addresses the need for reliable data verification in ML model building, but it is incremental as it applies existing formal methods to a known bottleneck in data quality.
The paper tackles the problem of ensuring proper data collection for machine learning by proposing a formal approach to verify that a dataset holds specified properties, such as coverage across the input space or class balance, using first-order logic and a prototype tool with the z3 solver, with preliminary results showing feasibility and performance.
In order to properly train a machine learning model, data must be properly collected. To guarantee a proper data collection, verifying that the collected data set holds certain properties is a possible solution. For example, guaranteeing that the data set contains samples across the whole input space, or that the data set is balanced w.r.t. different classes. We present a formal approach for verifying a set of arbitrarily stated properties over a data set. The proposed approach relies on the transformation of the data set into a first order logic formula, which can be later verified w.r.t. the different properties also stated in the same logic. A prototype tool, which uses the z3 solver, has been developed; the prototype can take as an input a set of properties stated in a formal language and formally verify a given data set w.r.t. to the given set of properties. Preliminary experimental results show the feasibility and performance of the proposed approach, and furthermore the flexibility for expressing properties of interest.