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 fits the data best 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 further model notions of minimal complexity using binary variables and logical constraints, solve polynomial optimization problems via mixed-integer linear or semidefinite optimization, and automatically prove the validity of our scientific discoveries via Positivestellensatz certificates. Remarkably, the optimization techniques leveraged in this paper allow our approach to run in polynomial time with fully correct background theory, or non-deterministic polynomial (NP) time with partially correct background theory. We experimentally 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 automatically derived from sets of partially correct background axioms.

翻译：通过简约地解释自然现象并与现有背景理论一致的科学公式的发现，是科学领域的一个关键目标。历史上，科学家通过基于现有知识操作方程、形成新方程并进行实验验证来推导自然定律。近年来，数据驱动的科学发现在拥有大量实验数据的场景中已成为一种可行的替代方法。然而，当数据存在噪声或数据稀缺时，数据驱动方法往往无法发现有效定律。相应地，近期工作结合了回归与推理，以消除与背景理论不一致的公式。但是，在符合背景理论的公式空间中搜索最优拟合数据的公式这一问题尚未得到良好解决。我们提出了一种解决方案，适用于所有公理和科学定律可通过多项式等式与不等式表达的情况，并论证了我们的方法具有广泛适用性。我们进一步利用二进制变量和逻辑约束对最小复杂度概念进行建模，通过混合整数线性或半定优化求解多项式优化问题，并借助Positivestellensatz证书自动证明科学发现的有效性。值得注意的是，本文所利用的优化技术使得我们的方法在背景理论完全正确时能以多项式时间运行，或在背景理论部分正确时以非确定性多项式时间运行。实验表明，一些著名科学定律，包括开普勒第三行星运动定律、哈根-泊肃叶方程以及辐射引力波功率方程，均可从部分正确的背景公理集合中自动推导得出。