Evolving Scientific Discovery by Unifying Data and Background Knowledge with AI Hilbert
Ryan Cory-Wright, Cristina Cornelio, Sanjeeb Dash, Bachir El Khadir, Lior Horesh
TL;DR
AI-Hilbert offers a principled framework that unifies experimental data and background knowledge expressed as polynomial equalities and inequalities, solving a polynomial optimization problem to discover laws $q(m{x})=0$ that are simultaneously data-consistent and derivable from theory. It leverages sum-of-squares optimization and the Positivstellensatz to obtain certificates of correctness, enabling not only discovery but also formal proofs of consistency with background axioms. The approach demonstrates rediscovery of Kepler's Third Law, Einstein time dilation, Hagen-Poiseuille flow, gravitational wave power, and Bell inequalities under various combinations of complete, incomplete, and inconsistent axioms, and highlights a data-efficiency advantage when relevant theory is supplied. It also defines a distance measure $d^c(q, G\u2229 H)$ to navigate incomplete or conflicting background knowledge and discusses practical considerations for data-to-theory trade-offs and computational scalability. The results suggest AI-Hilbert as a promising step toward reliable, interpretable scientific discovery that can operate in regimes where data are scarce or theory is partial, with clear avenues for extending to nonpolynomial settings and automated hyperparameter tuning.
Abstract
The discovery of scientific formulae that parsimoniously explain natural phenomena and align with existing background theory is a key goal in science. Historically, scientists have derived natural laws by manipulating equations based on existing knowledge, forming new equations, and verifying them experimentally. In recent years, data-driven scientific discovery has emerged as a viable competitor in settings with large amounts of experimental data. Unfortunately, data-driven methods often fail to discover valid laws when data is noisy or scarce. Accordingly, recent works combine regression and reasoning to eliminate formulae inconsistent with background theory. However, the problem of searching over the space of formulae consistent with background theory to find one that best fits the data is not well-solved. We propose a solution to this problem when all axioms and scientific laws are expressible via polynomial equalities and inequalities and argue that our approach is widely applicable. We model notions of minimal complexity using binary variables and logical constraints, solve polynomial optimization problems via mixed-integer linear or semidefinite optimization, and prove the validity of our scientific discoveries in a principled manner using Positivstellensatz certificates. The optimization techniques leveraged in this paper allow our approach to run in polynomial time with fully correct background theory under an assumption that the complexity of our derivation is bounded), or non-deterministic polynomial (NP) time with partially correct background theory. We demonstrate that some famous scientific laws, including Kepler's Third Law of Planetary Motion, the Hagen-Poiseuille Equation, and the Radiated Gravitational Wave Power equation, can be derived in a principled manner from axioms and experimental data.
