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 prove the validity of our scientific discoveries in a principled manner using 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 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 background axioms and experimental data.

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