(203b) Machine Learning + Automated Reasoning for Theory Discovery

Modern machine learning algorithms find patterns in large datasets, enabling automated search through the high-dimensional spaces of chemicals, materials, reactions, processes, and molecular interactions. However, these data-driven approaches are not easily connected to the equation-based theories that scientists have leveraged and built upon over the past centuries.

We propose a computational framework to discover and derive scientific theories, by integrating two typically distinct areas of computer science: machine learning and automated reasoning. Symbolic regression generates equations that empirically match experimental data. Top equations become "hypotheses" or "conjectures" to be proved or disproved by an automated theorem prover, starting from a set of "axioms" describing the environment under study. We demonstrate this framework by rediscovering and deriving Kepler’s Third Law from astronomical observations, and by rediscovering and deriving Langmuir adsorption from experimental measurements.