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

A central challenge in science is to explain natural phenomena using experimental data and existing theoretical knowledge. While the scientific method has yielded significant advancements, the rate of new law discovery is stagnating relative to the investment. This stagnation, partly due to the depletion of readily discoverable low-hanging fruit (laws expressible as simple polynomials), necessitates more sophisticated methods. This paper addresses this challenge by presenting AI-Hilbert, a novel framework that leverages recent progress in global optimization to systematically search for new scientific laws. AI-Hilbert integrates experimental data and theoretical knowledge, represented as polynomial equations and inequalities, to overcome limitations of purely data-driven or theory-driven approaches. The increasing scalability of global optimization methods, coupled with advancements in polynomial optimization and sum-of-squares techniques, makes this approach computationally feasible. Unlike many machine learning techniques that may generate unprovable or unverifiable laws, AI-Hilbert provides formal proofs of the derived laws' consistency with background theory and experimental data. This formal verification ensures the reliability and explainability of the discovered scientific laws, a critical aspect often lacking in purely data-driven discovery methods. The framework's potential extends to resolving inconsistencies within existing theoretical axioms by identifying subsets of axioms that best explain the data. AI-Hilbert offers a systematic and scalable pathway to uncovering new laws of nature, especially those involving higher-degree polynomials, which are typically beyond the reach of traditional scientific methods.

The paper reviews existing approaches to scientific discovery, contrasting traditional methods, machine learning techniques, and previous AI-driven approaches like AI-Descartes. Traditional methods proceed linearly from hypothesis generation (based on theory) to testing via data, while machine learning primarily relies on pattern identification within large datasets. AI-Descartes inverts this paradigm, starting with data and validating against theory. However, the paper highlights that these existing methods often struggle to integrate theory and data effectively, leading to potential inconsistencies or an inability to handle incomplete or noisy data. The authors note that existing automated approaches often rely on deep learning, which lacks formal proof capabilities and is prone to errors. The review sets the stage for AI-Hilbert, which aims to bridge the gap by integrating both theory and data seamlessly, offering a rigorous and verifiable pathway to scientific discovery. The scalability of modern optimization solvers is also discussed, emphasizing the current technological readiness for searching over the space of potential scientific laws.

AI-Hilbert formulates scientific discovery as a polynomial optimization problem. The input consists of: (1) background theory (B), expressed as polynomial equalities and inequalities (axioms); (2) experimental data (D); (3) constraints and bounds (C(A)) depending on hyperparameters (A); and (4) a distance function (d) quantifying the distance between a proposed law and the background theory. The goal is to discover an unknown polynomial formula q(x) that is consistent with both B and D. This is achieved by minimizing a weighted sum of discrepancies between q(x) and the data, and the distance between q(x) and its projection onto the set of laws derivable from B. The algorithm, AI-Hilbert, comprises three steps: (1) Formulation: The background theory, data, constraints, and distance function are combined to create a polynomial optimization problem (P_r). (2) Reduction: P_r is reduced to an equivalent semidefinite (or linear, if only equalities are present in B) program (P_r^sd) using sum-of-squares optimization techniques. (3) Solution: P_r^sd is solved using a mixed-integer conic optimization solver to obtain the polynomial q(x). The solution, q(x) = 0, represents the discovered scientific law, along with polynomial multipliers α and β that serve as a certificate proving the consistency of q(x) with B. The distance function d(q, G∩H) measures the closeness of q to the set of laws derivable from the background theory. The Positivstellensatz, a fundamental result in real algebraic geometry, is used to provide a formal proof of the correctness of the derived laws. AI-Hilbert allows for control over the tractability of the optimization problem by bounding the degree of the polynomials used in the certificates. The framework can handle incomplete or inconsistent background theories. In case of inconsistency, AI-Hilbert identifies subsets of consistent axioms that best explain the data using best subset selection. The methodology incorporates a trade-off between the amount of available background theory and the amount of experimental data needed; more theory reduces the search space and potentially decreases the data requirements. The choice of hyperparameters influences the balance between fidelity to data, fidelity to theory, and the complexity of the model.

The paper demonstrates AI-Hilbert's ability to rediscover several well-known scientific laws, showcasing its effectiveness in integrating data and theoretical knowledge. These demonstrations include: 1. **Hagen-Poiseuille Equation:** AI-Hilbert successfully derives the velocity profile for laminar fluid flow in a pipe using a simplified version of the Navier-Stokes equations, a degree-two polynomial velocity assumption, and a no-slip boundary condition. The derivation confirms the expected velocity profile, highlighting the method's capability in handling differential equations. 2. **Radiated Gravitational Wave Power Equation:** This demonstrates AI-Hilbert's ability to handle complex physical phenomena. The derivation integrates Kepler's Third Law, a linearized equation from general relativity, and a trigonometric identity. The solution precisely matches the known equation, showcasing the framework's capacity to combine diverse axioms and yield accurate results. This particular derivation was computationally intensive, requiring significant computational resources. 3. **Einstein's Relativistic Time Dilation Law:** The derivation involved a set of consistent relativistic axioms and an inconsistent Newtonian axiom, showing how AI-Hilbert can distinguish between valid and invalid axioms. By incorporating experimental data from light clock experiments, the system correctly selects the relativistic axioms and derives Einstein's time dilation formula. This validates the ability to handle inconsistent background theories and use data to select the correct axioms. 4. **Kepler's Third Law of Planetary Motion:** AI-Hilbert successfully derived Kepler's Third Law using a complete set of background knowledge axioms, including an incorrect candidate formula. By integrating experimental data, the algorithm correctly identifies and excludes the incorrect formula, leading to the accurate derivation. AI-Hilbert's scalability is demonstrated by the fact that it solves this problem more efficiently than Kepler's own four-year effort. 5. **Kepler's Law with Missing Axioms:** This experiment investigates the trade-off between data and theory. AI-Hilbert successfully reconstructs Kepler's Third Law even when some axioms are removed from the background theory, demonstrating that sufficient data can compensate for incomplete theoretical knowledge. The results show a clear trade-off: fewer axioms require more data points for successful derivation. These findings illustrate the versatility of AI-Hilbert in handling various complexities, including differential equations, inconsistent axioms, and incomplete theoretical knowledge, underlining its potential to become a powerful tool for scientific discovery.

AI-Hilbert offers a significant advancement over existing scientific discovery methods by seamlessly integrating experimental data and background knowledge within a formally verifiable framework. The ability to handle both complete and inconsistent sets of axioms, coupled with the capacity to automatically provide proofs of validity using the Positivstellensatz, addresses key limitations of previous methods. The successful derivation of several fundamental scientific laws demonstrates AI-Hilbert's efficacy and potential to accelerate scientific discovery in areas where data is scarce or theoretical knowledge is incomplete. The framework's scalability, although currently limited by computational constraints, offers a promising avenue for future advancements in scientific discovery. By systematically searching for polynomial relationships consistent with both data and theory, AI-Hilbert offers a rigorous and principled approach that can uncover new laws of nature, even those involving higher-degree polynomials that are challenging to find using conventional methods. This ability to deal with higher-degree polynomials extends the reach of symbolic discovery beyond what is currently feasible with existing techniques.

AI-Hilbert presents a novel framework for scientific discovery that integrates experimental data and background knowledge expressed as polynomials. The successful derivation of established scientific laws demonstrates the framework's effectiveness and potential to expedite the process of scientific discovery. Future research directions include extending the framework to handle non-polynomial operators, automating hyperparameter optimization, and improving scalability through techniques like exploiting Newton polytope properties, employing presolving techniques, and exploring alternative optimization methods. AI-Hilbert represents a significant step towards more efficient and reliable automated scientific discovery.

The current implementation of AI-Hilbert is limited by the computational cost of solving large-scale semidefinite programs. The use of primal-dual interior-point methods, while efficient for smaller problems, becomes computationally expensive with a large number of variables and high-degree polynomials. Currently, the framework is primarily applicable to systems that can be reasonably represented using polynomial equalities and inequalities. Future work is needed to extend the scope to other types of background knowledge and mathematical structures. The choice of hyperparameters still requires user input, although future development could automate this process. The quality of the derived formula depends significantly on the quality and completeness of the background theory and the availability of sufficient data. While the framework offers robust verification using Positivstellensatz certificates, the interpretation and relevance of the results still need careful scientific scrutiny.