Combining data and theory for derivable scientific discovery with AI-Descartes

The discovery of accurate and meaningful mathematical models describing natural phenomena is a central goal of scientific inquiry. Traditionally, this involved a combination of domain expertise to propose a functional form and statistical methods (like regression) to fit the model parameters to experimental data. More recently, machine learning approaches, particularly artificial neural networks (ANNs) and symbolic regression (SR), have been employed to automate this process. ANNs, while powerful predictors, often produce "black-box" models lacking interpretability. SR, on the other hand, generates models with explicit symbolic expressions, enhancing interpretability but potentially lacking the ability to integrate prior scientific knowledge. This paper tackles the open problem of incorporating prior knowledge, expressed as general logical axioms, into the model discovery process. The authors present AI-Descartes, a novel system that integrates symbolic regression with automated theorem proving to derive models consistent with both experimental data and a formal background theory. This approach addresses the limitations of purely data-driven methods by ensuring that discovered models are not only empirically accurate but also theoretically grounded. The importance of this lies in generating models that are not only descriptive but also predictive and insightful, offering deeper understanding of the underlying physical processes.

Existing research has explored incorporating prior knowledge into machine learning models, but primarily focusing on constraints on the functional form rather than incorporating general logical axioms representing broader scientific theories. Methods using logic-based descriptions to constrain the output of generative adversarial networks (GANs) for image generation have been explored, as have techniques combining machine learning and reasoning engines to search for functional forms satisfying pre-specified constraints. These works often augment datasets to improve learning efficiency and model accuracy. However, a crucial gap remains in integrating general background-theory axioms (logical constraints encompassing other laws and unmeasured variables) into the model discovery process. The authors acknowledge the work of Schmidt and Lipson on balancing accuracy and complexity in SR, but emphasize the need to go beyond this metric to ensure consistency with established scientific knowledge. This paper addresses this gap by proposing a novel framework that combines SR with formal logic reasoning to achieve this integration.

The authors' automated scientific discovery method aims to discover a symbolic model y = f(x), where x is a vector of independent variables and y is the dependent variable. The model should fit the data, be derivable from a background theory (B), possess low complexity, and have bounded prediction error. The input to the system consists of four elements: 1. **Background Knowledge (B):** A set of domain-specific axioms expressed in first-order logic with equality, inequality, and basic arithmetic operators. The background theory is assumed to be complete and consistent, guaranteeing a unique derivable function fB representing the variable of interest. 2. **Hypothesis Class (C):** A set of admissible symbolic models defined by a grammar, invariance constraints (e.g., A+B = B+A), and constraints on functional form (e.g., monotonicity). 3. **Data (D):** A set of data points providing values for x and y. 4. **Modeler Preferences (M):** Numerical parameters specifying error bounds and complexity limits. The system integrates two main modules: an SR module and a reasoning module. The SR module uses a novel mixed-integer nonlinear programming (MINLP)-based solver to generate multiple candidate symbolic models fitting the data. These models are then evaluated for their distance (β(f)) to the derivable function from the background theory and their distance (δ(f)) to the data. The reasoning module, implemented using KeYmaera X (an automated theorem prover for hybrid systems), assesses the derivability of each candidate model from the background theory. If a model is derivable, it's selected; otherwise, the reasoning module provides quality assessments (based on the distance β) and may suggest acquiring more data or adding constraints. The distance β quantifies the compatibility between the SR-generated function and the function derivable from the background theory (fB). This distance is independent of any specific functional form of fB. The reasoning module can also demonstrate non-derivability by providing counterexamples. The authors also employ Mathematica for certain types of symbolic expression analysis. The system operates as a discovery cycle, inspired by Descartes' scientific method, iteratively generating hypotheses from data, assessing them against theory, and refining the model or acquiring additional data as needed. A key contribution is the introduction of novel measures (pointwise and generalization reasoning errors) to quantify the closeness of a model to a derivable formula.

The proposed system was validated on three problems: Kepler's third law, Einstein's time dilation, and Langmuir's adsorption equation. **Kepler's Third Law:** The system successfully rediscovered Kepler's third law from solar system data and Newton's laws of motion. The reasoning module effectively distinguished between candidate formulae with similar data error, selecting the one generalizing best to a broader range of masses. The authors introduced measures to analyze the quality and generalizability of generated formulae including pointwise reasoning error, generalization reasoning error, and variable dependence, which helped assess the correctness of data-driven formulae from a reasoning perspective. **Einstein's Time Dilation:** While the exact formula wasn't recovered, the reasoning module identified the best-generalizing formula. Furthermore, by analyzing reasoning errors with different axiom sets (Newtonian vs. relativistic), the system helped identify the theory better explaining the phenomenon. This highlights the ability to discriminate between different theoretical frameworks. **Langmuir's Adsorption Equation:** The system generated models fitting experimental data. By relating material-dependent coefficients in the background theory to those in the SR-generated models through existential quantification, the authors could logically prove one of the extracted formulae. This demonstrated the ability to connect data-driven models to a formally axiomatized theory. Across all three cases, the integration of SR and reasoning produced superior models compared to using either method alone, showcasing the synergistic effect of combining data-driven and theory-driven approaches. The authors also discuss various error metrics used to evaluate the quality of the generated formulas, such as numerical error (relative and absolute) and reasoning error (pointwise and generalization). These help assess the model's fit to the data and its consistency with the background theory.

The successful application of the AI-Descartes system to diverse scientific problems demonstrates the value of integrating logical reasoning with symbolic regression for discovering meaningful symbolic models. The results highlight the advantages of combining data-driven and theory-driven approaches. The system produces models that are not only empirically accurate but also consistent with established scientific knowledge, thereby enhancing their predictive power and explanatory potential. The ability to discriminate between competing theoretical frameworks and to rigorously prove the derivability of models from axioms represents a significant advancement in automated scientific discovery. This approach could revolutionize the scientific process by enabling the discovery of models that are both data-driven and grounded in fundamental principles.

AI-Descartes presents a novel framework for automated scientific discovery that successfully integrates symbolic regression and logical reasoning. The system demonstrated its ability to discover and validate scientific laws using diverse datasets and theories, achieving results superior to those obtained using either technique alone. Future work could involve enhancing the system by incorporating abductive reasoning to handle incomplete background theories, improving the efficiency of the SR and reasoning modules, and integrating experimental design techniques to optimize data acquisition. The availability of background knowledge in machine-readable format remains a challenge, but progress in knowledge extraction techniques may address this issue.

The system currently assumes the completeness and correctness of the background theory. Incomplete theories could be partially addressed through abductive reasoning, but this remains an area for future improvement. The computational complexity of automated theorem proving poses a scaling challenge; however ongoing research in neuro-symbolic AI promises to mitigate this. The current implementation of the SR module has limitations in handling certain types of expressions and equations, while the automated theorem prover has limitations in its supported logic and equation types. The availability of well-formulated, machine-readable background theories for diverse scientific domains also remains a significant hurdle.