Evolving scientific discovery by unifying data and background knowledge with AI Hilbert

The paper addresses how to derive new scientific laws that are simultaneously consistent with experimental data and with background theoretical knowledge, particularly when existing methods either rely solely on theory or solely on data. The authors argue that a disciplined integration of background axioms (expressible as polynomial equalities/inequalities) with observed data can accelerate and improve scientific discovery, especially as traditional discovery rates slow while global optimization capabilities have advanced. The research proposes framing discovery as polynomial optimization with formal guarantees using sum-of-squares (SOS) and Positivstellensatz certificates, enabling principled validation of derived laws. The study’s purpose is to create AI-Hilbert, a framework that unifies data and theory to produce provably derivable or approximately derivable laws, reduce data needs via theory-constrained search, and diagnose inconsistency in background knowledge.

The paper situates AI-Hilbert within prior work on automated scientific discovery and symbolic regression. Existing approaches often use deep learning or genetic programming (e.g., AI Feynman, Eureqa, PySR, Bayesian Machine Scientist) and may produce spurious or unprovable laws, especially with limited or noisy data. AI-Descartes integrates theory only as a post-hoc filter of data-derived expressions, leaving data and theory disjoint. Symbolic regression via global MINLP or genetic programming lacks polynomial-time guarantees and formal proofs. In contrast, SOS-based methods from real algebraic geometry allow formal certification of derivability and tractable searches at bounded degree. The literature on SOS hierarchies, semidefinite programming, and interior-point methods provides the computational backbone, while prior results on VC-dimension and shape-constrained regression motivate data-efficiency via theory constraints.

AI-Hilbert formulates scientific discovery as a polynomial optimization problem combining background theory and data. Inputs are a tuple (B, D, C(A), d): B is background theory as polynomial equalities h_j(x)=0 and inequalities g_i(x)≥0 over variables x∈R^n; D is experimental data over a measurable subset of variables x_1,…,x_t (with x_1 as a dependent variable); C(A) are constraints and hyperparameters (e.g., degree bounds on target polynomial q and on proof certificates, sparsity/axiom subset constraints, and a trade-off parameter between theory and data); d(·) is a distance between a candidate polynomial law q and the theory set G∩H, defined via an inner optimization using SOS multipliers and optional binary selectors to model best-subset axiom selection. The core optimization (Problem (10)) minimizes a weighted sum of empirical discrepancies |q(x_i)| over data plus λ times the distance d(q,G∩H), subject to constraints that enforce inclusion of the dependent variable and exclusion of unmeasured variables, and degree bounds on q. If the theory is complete, an alternative feasibility formulation (Problem (12)) finds q such that q equals an SOS combination of the axioms, potentially requiring no data. Using Putinar’s Positivstellensatz, if d=0 then q is derivable from B via certificates q=a_0+∑ a_i g_i+∑ b_j h_j with SOS multipliers a_i and polynomial multipliers b_j; if d>0 the method returns approximate certificates and a discrepancy polynomial r(x). The computational pipeline: (1) Formulate the polynomial program using PolyJuMP/SumOfSquares.jl, including binary variables for axiom selection when needed; (2) Reduce to semidefinite (or linear, if only equalities) optimization via SOS relaxation at a fixed degree; (3) Solve via mixed-integer conic/semidefinite solvers (e.g., Mosek, Gurobi). The degree of q and of multipliers trades off expressivity and tractability; bounded-degree SOS yields polynomial-time solvable SDPs under regularity when axioms are consistent, whereas inconsistent theories induce mixed-integer SDPs (NP-hard) but often solvable efficiently in practice. The method supports implicit laws q(x)=0, appropriate when explicit polynomial y=f(x) is unavailable. Complexity control includes degree limits, sparsity/cardinality constraints on axioms, and L1 coefficient norm regularization of q.

- The framework can recover known scientific laws and produce formal certificates of derivability from axioms, sometimes without any numerical data when background theory is complete. - Hagen–Poiseuille equation: Starting from simplified Navier–Stokes in cylindrical coordinates, a quadratic velocity Ansatz, and boundary conditions, AI-Hilbert recovers u(r)∝(r^2−R^2) by solving Problem (12) with low-degree multipliers, producing explicit polynomial multipliers validating the derivation. - Radiated gravitational wave power (Peters–Mathews law): From Kepler’s law, a linearized GR power expression, and trigonometric constraints (x^2+y^2=1 with x=cosφ, y=sinφ), AI-Hilbert derives P ∝ G^4 m_1^2 m_2^2 (m_1+m_2)/ (c^5 r^5) (presented via an equivalent certified polynomial identity). The SOS search used multipliers up to degree 20 with variable degree caps, generating 416,392 candidate monomials; the instance took ~14,368 s to write to memory and 6.58 s to solve in Mosek on a 640 GB RAM system. Polynomial multipliers are provided, certifying correctness. - Einstein’s relativistic time dilation: With five relativistic axioms plus one inconsistent Newtonian axiom, and experimental light-clock data, AI-Hilbert selects a consistent subset (cardinality t=5) and derives −c^2 f + c^2 f^2 + f_0^2 v^2 = 0, equivalent to f/f_0 = sqrt(1 − v^2/c^2). Solved in 6.04 s with Gurobi 9.5.1. Certificates verify derivability from the selected axioms. - Kepler’s Third Law: Given center-of-mass, gravitational, centrifugal, force-balance, and period–frequency relations, plus an incorrect candidate formula, AI-Hilbert under sparsity (≤5 axioms) and d=0 recovers m_1 m_2 G p^2 = m_1 d_1 d_2 + m_2 d_1 d_2 + 2 m_1 d_1 d_2 (equivalent to the classic form after variable definitions), with a MILP containing 18,958 continuous and 6 binary variables. Explicit multipliers are reported. - Theory–data trade-off: Experiments show that adding relevant axioms reduces data requirements (consistent with VC-dimension arguments). With missing axioms, the method still recovers Kepler’s law from noiseless data using L1-regularized formulations and feasibility tolerances. - Comparative performance: On a test set, AI-Hilbert outperforms purely data-driven baselines (AI Feynman, PySR, Bayesian Machine Scientist) and AI-Descartes (which filters data-derived expressions using theory) in recovering target laws, especially under limited or noisy data. - Additional demonstrations include the use of SOS certificates to verify bounds in probabilistic/quantum-style inequalities (e.g., a tight upper bound of 4 for a stated inequality), illustrating generality beyond physics laws.

AI-Hilbert directly addresses the research goal of unifying data and background theory to discover scientifically valid laws with formal guarantees. By embedding axioms as polynomial constraints and searching over implicit polynomial laws with SOS-based certificates, the approach ensures that discovered formulas are consistent with theory (or quantifies the deviation) while fitting experimental data. This joint treatment reduces the effective hypothesis space, thereby improving data efficiency and mitigating spurious discoveries common in data-only methods. The framework can also diagnose and resolve inconsistencies by selecting subsets of axioms best supported by data. Empirical validations on canonical physics problems (fluid dynamics, gravitation, relativity, celestial mechanics) show the method can rediscover complex laws, often providing exact derivations or certified approximations at moderate computational cost. The discussion highlights the method’s generality (implicit representations, certificate-based validation), computational tractability at bounded degrees, and its potential to form the basis of more reliable, theory-aware scientific discovery pipelines.

The paper introduces AI-Hilbert, a principled framework for scientific discovery that unifies experimental data with background polynomial theory using SOS/semidefinite and mixed-integer optimization. Main contributions include: (1) a formulation that discovers implicit polynomial laws q(x)=0 while simultaneously producing Positivstellensatz certificates of (approximate) derivability; (2) mechanisms to handle incomplete or inconsistent theories via axiom subset selection and a tunable distance-to-theory metric; (3) empirical demonstrations recovering canonical laws (Hagen–Poiseuille, gravitational wave power, Einstein’s time dilation, Kepler’s third law) with quantitative performance details; and (4) complexity control through bounded-degree certificates and sparsity. Future work includes extending beyond polynomials to encompass differential/integral and transcendental operators via polynomial/trigonometric approximations, automating hyperparameter tuning for trade-offs among fit, theory fidelity, and complexity, and improving scalability using Newton polytope reductions, chordal sparsity or partial facial reduction, and alternatives to IPM-based SDP solvers such as Burer–Monteiro factorizations or SOCP inner approximations.

- Polynomial expressibility: The current framework assumes background theory and target laws can be expressed (or approximated) as polynomial equalities/inequalities; many domains involve non-polynomial operators (differential, integral, transcendental), requiring extensions or approximations. - Computational scalability: SOS-to-SDP reformulations with interior-point methods can be memory-intensive. Reported limitations include practical bounds around n≈15 variables and certificate degree d≈20, with large models incurring heavy problem generation time and memory usage. - Complexity with inconsistent axioms: Inconsistent theory introduces mixed-integer semidefinite optimization, which is NP-hard in general (though often tractable empirically). Performance can vary with problem structure and solver capabilities. - Hyperparameter sensitivity: The approach requires setting degree bounds, regularization weights, and axiom subset cardinalities; currently, selection is manual and problem-dependent. - Implicit representation degeneracy: Multiple equivalent implicit polynomials may represent the same law, requiring additional constraints or complexity penalties (e.g., L1 on coefficients) to favor parsimonious forms.