(250c) Model Validation Using Principles of Automated Theorem Proving

Automation has lead to the generation, storage and use of large amounts of data in modern chemical plants. This has led to an increasing interest in data-driven methods of modeling. In prior work in our group, we have been considered the use of control laws to drive the plant toward operating data with the goal that this may aid in developing physics-based models from on-line data. However, it remains unclear what defines a physics-based model. Additionally data driven models are built by minimizing the error between observation and prediction, and hence, requires a means of validation that does not rely on accuracy [1]. In the work of Chen et. al [2], a Bayesian approach to validating data driven models is discussed as an alternative to accuracy of model predictions.

In this work, we present methods of model validation that attempt to use known physical laws of the process in order to validate models. Automated Theorem Proving (ATP) is a method of determining the validity of logical statements known as propositions, given an existing set of true statements, known as axioms. In this framework, models proposed by data-driven model identification techniques take the place of propositions, while features expected from any model of a chemical process, such as mass and energy balances, function as axioms. The first part of this work deals with determining the error rate of a given model when determining how often it satisfies mass and energy balances, termed the axiomatic error. In the second part of this work, we attempt to determine if the space of possible state predictions made by a model fall within the intersection of state predictions that satisfy the given axioms of mass and energy balances. We utilize the results to identify data that a Lyapunov-based economic control law can guide the state to.

References: