(426a) Opportunities for Symbolic Machine Learning and Automated Reasoning in Chemical Engineering
AIChE Annual Meeting
2022
2022 Annual Meeting
Catalysis and Reaction Engineering Division
Data Science & Machine Learning Approaches to Catalysis I: Interpretable and Theory-Guided Machine Learning For Catalysis Design and Understanding
Wednesday, November 16, 2022 - 8:00am to 8:36am
Machine learning algorithms extract patterns from large datasets to generate predictions. Some tools lead to interpretable models, and some learning algorithms are informed by physics, but generally, these are not easily related to the equation-based theories and derivations in the literature. The development of artificial systems that operate on equations and theories could open new avenues for scientific discovery.
Automated reasoning tools, including computer algebra systems, automated theorem provers, and interactive theorem provers, can treat the “stuff†of theory as model inputs and outputs, perform logical transformations from one formula to another, and provide rigorous certifications when derivations are mathematically sound. In this talk, we will highlight several projects in the ATOMS Lab (AI & Theory-Oriented Molecular Science Lab) that demonstrate the value of automated reasoning tools in chemical engineering.
Automated reasoning tools, including computer algebra systems, automated theorem provers, and interactive theorem provers, can treat the “stuff†of theory as model inputs and outputs, perform logical transformations from one formula to another, and provide rigorous certifications when derivations are mathematically sound. In this talk, we will highlight several projects in the ATOMS Lab (AI & Theory-Oriented Molecular Science Lab) that demonstrate the value of automated reasoning tools in chemical engineering.
We illustrate how equation-based models can be generated from data using symbolic regression, then checked against background theory using automated reasoning tools. We also show how automated theorem proving can be used to verify safety in chemical reactors by creating a machine-checkable proof that a concentration threshold (e.g. C(t) < Cmax) is always satisfied (TRUE), or by automatically returning FALSE when the threshold is violated. We also illustrate how recent interactive theorem proving tools are mature enough to formally prove complex mathematical statements, and we highlight the potential for these tools for formally checking theories in our literature, in thermodynamics, kinetics, transport, and molecular science.