  Scientists have long aimed to discover meaningful formulae which accurately
describe experimental data. A common approach is to manually create
mathematical models of natural phenomena using domain knowledge, and then fit
these models to data. In contrast, machine-learning algorithms automate the
construction of accurate data-driven models while consuming large amounts of
data. The problem of incorporating prior knowledge in the form of constraints
on the functional form of a learned model (e.g., nonnegativity) has been
explored in the literature. However, finding models that are consistent with
prior knowledge expressed in the form of general logical axioms (e.g.,
conservation of energy) is an open problem. We develop a method to enable
principled derivations of models of natural phenomena from axiomatic knowledge
and experimental data by combining logical reasoning with symbolic regression.
We demonstrate these concepts for Kepler's third law of planetary motion,
Einstein's relativistic time-dilation law, and Langmuir's theory of adsorption,
automatically connecting experimental data with background theory in each case.
We show that laws can be discovered from few data points when using formal
logical reasoning to distinguish the correct formula from a set of plausible
formulas that have similar error on the data. The combination of reasoning with
machine learning provides generalizeable insights into key aspects of natural
phenomena. We envision that this combination will enable derivable discovery of
fundamental laws of science and believe that our work is an important step
towards automating the scientific method.
