AI-Descartes can also distinguish between different sets of background theories. Given high precision atomic clock measurements and either Einstein’s or Newton’s theory, our tool can sort out which theory is more consistent with the data.

Given data on the orbital periods of celestial bodies, the SR module of AI-Descartes generates formulas that fit the data well, while the Reasoning module re-ranks them based on the distance to a given background theory and identifies the one that is closest to being derivable.

We tested AI-Descartes on Langmuir’s 1918 experimental data in an attempt to rediscover his theory of adsorption. Many expressions fit the data well, but only one (f2) is successfully derived from the background theory by the theorem prover.

Our paper is out in @NatureComms! We introduce AI-Descartes, an AI tool that uses both data and background theory for scientific discovery. Symbolic Regression, an #ML technique, generates formulas and an automated theorem prover checks their derivability.