The AI-Descartes system (Nature Communications 14:1777, 2023) demonstrated that symbolic laws such as Kepler's third law, Einstein's relativistic time dilation, and Langmuir's adsorption isotherm can be discovered automatically by combining symbolic regression on experimental data with logical reasoning over a machine-readable background theory, so that the discovered formula is not merely data-fitting but provably derivable from prior axioms. The paper explicitly lists the unresolved issues that stand between this demonstration and a general automation of the scientific method: the reasoner assumes the background theory is correct and complete (abductive repair of missing axioms was envisioned but not implemented); machine-readable axioms for the natural sciences are scarce and extraction from technical text is inadequate; automated theorem proving is plagued by undecidability, difficult arithmetic and calculus reasoning, large run-time variance, and symbolic regression via mixed-integer nonlinear programming becomes prohibitively slow on noisy or large encodings; the reasoning tools have expressivity limits; and the discovery loop lacks an integrated optimal experimental design (OED) module. Subsequent literature (AI-Hilbert, AI-Noether, a 2025 Winter Simulation Conference OED paper by the same group, and related work) has partially addressed only polynomial-expressible fragments of these gaps. The open core — the integrated derivable-discovery loop handling incomplete or imperfect background theories in general logical expressive power, automated axiom acquisition, scalable reasoning beyond the polynomial regime, and OED that jointly selects functional form and parameters, accounting for logical derivability — remains open.

Background

A central goal of AI for science is to discover symbolic laws — closed-form formulas relating measurable quantities — that both fit experimental data and are consistent with what is already known. Two families of methods address halves of this goal. Symbolic regression (SR) searches a space of mathematical expressions for formulas that fit data with low error and low complexity, but it ignores prior knowledge and can return physically meaningless expressions. Logical reasoning over a formalized background theory — a set of machine-readable axioms such as conservation laws — can prove or refute candidate formulas, but needs a source of candidates and of data. AI-Descartes (Cornelio, Dash, Austel, Josephson, Goncalves, Clarkson, Megiddo, El Khadir, and Horesh, Nature Communications 14:1777, 2023) combined the two: an SR component (implemented via mixed-integer nonlinear programming, MINLP — optimization problems with both discrete and nonlinear continuous variables, solved here with the global solver BARON) proposes candidate formulas, and a reasoning component checks each candidate for derivability from the background axioms using the KeYmaera theorem prover (a tool for proving properties of hybrid systems specified in differential dynamic logic). The system recovered Kepler's third law of planetary motion, Einstein's relativistic time-dilation law, and Langmuir's theory of adsorption from small, noisy datasets, connecting data and theory automatically. The paper's discussion section, 'System limitations and future improvements', states that this is 'only a first, although crucial, step towards completing the missing links in automating the scientific method' and enumerates the unresolved issues this task concerns. They are: (1) the reasoning component assumes the background theory is correct and complete, and the proposed remedy — abductive reasoning (abduction: given a logical theory and an observation the theory cannot explain, find additional axioms consistent with the theory that make the observation derivable) — was not implemented; (2) machine-readable axioms for physics and other natural sciences are scarce, and automated extraction of reliable axioms from technical text (e.g., by deep-learning methods over plain or LaTeX/HTML text) remains inadequate for the system's scope; (3) scalability — automated theorem proving is undecidable for the logics involved, reasoning with arithmetic and calculus operators is difficult, prover run-time variance is large, and MINLP-based SR worst-case solution time grows exponentially with the encoding size, especially with noisy data; (4) expressivity limits of the tools — KeYmaera supports differential equations only in the time variable and no higher-order logic, and BARON cannot handle differential equations; (5) the discovery loop lacks an integrated experimental-design module: the paper identifies optimal experimental design (OED — choosing data-acquisition steps that minimize the uncertainty of inferred parameters or predictions under a statistical or information-theoretic criterion) as a needed extension, ideally a framework handling both the functional form and the continuous parameters of a model, and one that 'consistently accounts for logical derivability'. Later work by the same and adjacent groups frames precisely these gaps as the live frontier: AI-Hilbert (arXiv:2308.09474) recasts the reasoning-plus-regression coupling as polynomial optimization with Positivstellensatz certificates (algebraic proofs of infeasibility/validity for polynomial systems) when all axioms and laws are polynomial equalities and inequalities; AI-Noether (arXiv:2509.23004) implements abductive axiom repair, but again only for polynomial-expressible axioms; and a 2025 Winter Simulation Conference paper by six authors including two AI-Descartes co-authors gives a preliminary OED formulation restricted to choosing among a predefined finite set of model classes. None of these addresses the general or integrated problem.

Problem Statement

As stated by the source paper's discussion of unresolved issues, and left open by the subsequent literature, the problem is to extend automated derivable scientific discovery — of the kind demonstrated by AI-Descartes on Kepler's third law, Einstein's time-dilation law, and Langmuir's adsorption theory — beyond its current assumptions. The source paper frames the open work as a set of directions that together complete the discovery loop, all of which are required: (1) relax the assumption that the background theory is correct and complete — its proposed remedy, unimplemented in the source system, is abductive reasoning that, given background axioms and a data-derived candidate law the axioms cannot derive, produces additional explanation axioms (the missing axioms of the incomplete background theory) that are consistent with the original background theory and from which the candidate law is provably derivable — in the general setting of the source system, which uses first-order logical axioms with arithmetic and differential equations, not only axioms expressible as polynomial equalities and inequalities; (2) enable automated acquisition of machine-readable background axioms from technical text at the reliability the reasoning component requires; (3) make the combined symbolic-regression-plus-reasoning search scale — despite the undecidability of proving conjectures in the underlying logics, the difficulty of reasoning with arithmetic and calculus, the large run-time variance of theorem provers, and the exponential worst-case behavior of MINLP-based symbolic regression on noisy or large encodings; (4) extend the expressivity of the reasoning tools beyond differential equations in the time variable only, beyond the absence of higher-order logic, and to differential equations within the optimization-based regression component; and (5) integrate optimal experimental design into the loop, choosing data-acquisition steps that minimize uncertainty under a statistical or information-theoretic criterion, jointly over the functional form and the continuous parameters of candidate models, accounting for logical derivability. The common objective uniting these directions — the loop vision sketched in the source paper's Figure 3 — is an automated discovery system that recovers laws of the Kepler/Einstein/Langmuir type from few, noisy, and actively chosen experiments under realistic — incomplete or imperfect — background theories, with derivations that are themselves verifiable. Partial resolutions exist in restricted fragments (polynomial-expressible axioms for abduction and for scalable reasoning; a predefined finite model-class menu for preliminary OED), but these fragments do not resolve the task: it requires the general and integrated version of the problem — all five directions above addressed jointly, each beyond the restricted fragment in which partial results currently exist, and realized as an integrated system of the kind the objective describes — which remains open. Accordingly, the task is resolved only when a single end-to-end automated demonstration — not per-direction or fragmentary results — recovers the source's law class (Kepler's third law, Einstein's time-dilation law, and Langmuir's adsorption theory) from small, noisy datasets under an incomplete or imperfect background theory with at least one actively chosen experiment, in the source system's logical setting of first-order axioms with arithmetic and differential equations rather than axioms expressible only as polynomial equalities and inequalities, and with machine-checkable derivations; addressing fewer than all five directions does not resolve the task.

References

  1. Cristina Cornelio, Sanjeeb Dash, Vernon Austel, Tyler R. Josephson, Joao Goncalves, Kenneth L. Clarkson, Nimrod Megiddo, Bachir El Khadir, Lior Horesh (2023). 'Combining data and theory for derivable scientific discovery with AI-Descartes.' Nature Communications 14, article 1777. DOI: 10.1038/s41467-023-37236-y. https://doi.org/10.1038/s41467-023-37236-y (preprint: arXiv:2109.01634v4, titled 'AI Descartes: Combining Data and Theory for Derivable Scientific Discovery', https://arxiv.org/abs/2109.01634)
  2. Ryan Cory-Wright, Cristina Cornelio, Sanjeeb Dash, Bachir El Khadir, Lior Horesh (2023, revised 2024). 'Evolving Scientific Discovery by Unifying Data and Background Knowledge with AI Hilbert.' arXiv:2308.09474. https://arxiv.org/abs/2308.09474
  3. Karan Srivastava, Sanjeeb Dash, Ryan Cory-Wright, Barry Trager, Cristina Cornelio, Lior Horesh (2025). 'Bridging the Gap Between Scientific Laws Derived by AI Systems and Canonical Knowledge via Abductive Inference with AI-Noether.' arXiv:2509.23004. https://arxiv.org/abs/2509.23004
  4. Kenneth L. Clarkson, Soumyadip Ghosh, Joao P. Goncalves, Rik Sengupta, Mark S. Squillante, Dmitry Zubarev (2025). 'A Simulation Optimization Approach to Optimal Experimental Design for Symbolic Discovery.' Proceedings of the 2025 Winter Simulation Conference. DOI: 10.1109/WSC68292.2025.11339140. https://doi.org/10.1109/WSC68292.2025.11339140
  5. Elizaveta Ivanchik, Alexander Hvatov (2025). 'Knowledge-aware differential equation discovery with automated background knowledge extraction.' Information Sciences. DOI: 10.1016/j.ins.2025.122131. https://doi.org/10.1016/j.ins.2025.122131
  6. Cristina Cornelio, Takuya Ito, Ryan Cory-Wright, Sanjeeb Dash, Lior Horesh (2025). 'The Need for Verification in AI-Driven Scientific Discovery.' arXiv:2509.01398. https://arxiv.org/abs/2509.01398
  7. Nazanin Ahmadi Daryakenari, Mario De Florio, Khemraj Shukla, George Em Karniadakis (2023). 'AI-Aristotle: A Physics-Informed framework for Systems Biology Gray-Box Identification.' arXiv:2310.01433. https://arxiv.org/abs/2310.01433
  8. You-Le Fang, Dong-Shan Jian, Xiang Li, Yan-Qing Ma (2025). 'AI-Newton: A Concept-Driven Physical Law Discovery System without Prior Physical Knowledge.' arXiv:2504.01538. https://arxiv.org/abs/2504.01538