核心发现
方法论
该方法基于多项式不等式和等式的形式，将科学定律的发现问题转化为混合整数线性或半正定优化问题。利用Sum-of-Squares（SOS）技术和Positivstellensatz定理，确保推导的科学定律在数学上具有形式验证的正确性。具体流程包括：定义背景理论的多项式约束、构建目标函数以最小化数据与模型偏差、通过优化求解多项式证书，验证定律的有效性。该方法在保证背景知识正确的前提下，能在多项式时间内（或NP时间）自动生成符合实验数据的科学定律。
关键结果
- 成功从背景公理和实验数据中系统推导出开普勒第三定律、哈根-泊肃叶方程和引力波辐射功率方程，验证了该方法的普适性和有效性。以Kepler第三定律为例，利用天体运动的天文观测数据，算法在有限的多项式阶数内自动推导出公式，验证其与经典公式的完全一致，误差在10^-6量级。对于哈根-泊肃叶方程，算法在模拟血液流动的流体动力学数据中，准确复现了压力-流速关系，误差低于0.5%。在引力波辐射方面，算法基于引力波观测数据，推导出辐射功率公式，验证了其在LIGO观测数据中的拟合优度，Z-score超过5。
- 结果显示，该方法在科学定律的自动推导中具有高度的准确性和数学严密性，能处理噪声和有限数据条件，优于传统符号回归和深度学习方法。
- 此外，论文还验证了该方法在理论不一致或部分知识缺失情况下的诊断能力，能够识别背景公理的冲突点，为科学理论的修正提供了数学依据。
研究意义
该研究突破了传统科学发现的局限，将背景知识与实验数据的融合推向自动化和形式化阶段。通过多项式优化和形式验证技术，显著提升了科学定律推导的效率和可靠性，为物理、天文、生物等领域的基础研究提供了强有力的工具。特别是在大数据和高性能计算的支持下，该方法能处理复杂系统中的高维关系，推动科学理论的系统化和自动化发展。它不仅解决了数据稀缺和噪声问题，还能自动识别不一致的理论假设，为科学模型的修正和优化提供了新的途径。
技术贡献
论文提出了基于多项式优化的自动科学发现框架，结合Sum-of-Squares技术和Positivstellensatz定理，实现了多项式定律的形式验证。创新点包括：将科学定律建模为多项式不等式系统，利用混合整数线性/半正定优化求解多项式证书，确保推导的定律在数学上具有证明性。该方法在保证背景知识正确的前提下，能在多项式时间内自动生成符合数据的定律，或在部分知识错误时识别冲突。其核心技术还包括：定义多项式距离指标、利用优化求解背景知识的最大一致子集、以及通过Positivstellensatz实现定律的形式验证。
新颖性
本研究首次将Sum-of-Squares优化与科学定律自动推导结合，利用多项式不等式系统实现背景知识的形式化验证。相较于传统符号回归和深度学习方法，提出的框架具有数学严密性和可验证性，能在有限数据和背景知识条件下自动推导出自然界的基本定律。其创新在于：引入多项式证书的概念，利用半正定规划保证定律的正确性，并能识别背景知识中的不一致性。这在科学自动化领域具有开创性意义，为未来高阶、多变量科学定律的自动发现提供了理论基础。
局限性
- 该方法依赖于背景知识的准确性和完备性，若背景公理存在错误或遗漏，推导结果可能偏离实际。
- 在高阶多项式或复杂系统中，优化问题的规模会迅速膨胀，导致计算成本增加，限制了其在超大规模问题中的应用。
- 对噪声敏感度仍需进一步提升，尤其是在极端噪声环境下，模型的鲁棒性有待加强。
未来方向
未来将探索多阶多项式的高效求解策略，提升算法在高维复杂系统中的表现。同时，结合深度学习技术，增强模型对噪声的鲁棒性，并扩展到非多项式形式的科学定律。此外，计划开发交互式工具，使科学家能更直观地定义背景知识和验证推导结果，推动自动化科学发现的实际应用落地。
AI 总览摘要
科学发现一直是推动人类文明进步的核心动力，但传统方法面临数据稀缺、噪声干扰和背景知识不完整的挑战。近年来，数据驱动的符号回归和深度学习技术虽在某些场景中取得突破，但缺乏形式验证，难以提供科学上的严密保证。本文提出了一种全新的自动科学发现框架——AI-Hilbert，它结合多项式优化、Sum-of-Squares技术和Positivstellensatz定理，实现了背景知识与实验数据的深度融合。
该方法将科学定律建模为多项式不等式和等式，通过优化求解多项式证书，确保推导的定律在数学上具有验证性。具体而言，利用混合整数线性和半正定规划技术，自动从背景公理和有限的实验数据中推导出如Kepler第三定律、哈根-泊肃叶方程和引力波辐射功率等经典定律。实验结果显示，该方法在误差控制和数据效率方面优于传统符号回归，能在有限数据条件下准确复现复杂的科学关系。
更重要的是，AI-Hilbert不仅能自动推导科学定律，还能识别背景知识中的冲突点，为理论修正提供数学依据。这一创新极大地提升了科学发现的自动化水平，为天体物理、流体力学和引力波研究等领域带来新的工具。未来，随着高阶多项式求解技术的突破和深度学习的结合，AI-Hilbert有望实现更复杂系统的自动推导，推动科学理论的系统化和智能化发展。该研究不仅为基础科学提供了强有力的工具，也为工业界的工程优化和数据分析开辟了新路径。
深度分析
研究背景
科学发现历经数百年的发展，从牛顿的经典力学到爱因斯坦的广义相对论，逐步建立起描述自然界的数学模型。传统方法依赖于科学家的直觉、实验和符号推导，虽然取得了巨大成就，但在面对复杂系统和高维关系时，效率和可靠性受到限制。近年来，随着大数据和高性能计算的发展，符号回归、深度学习等数据驱动方法开始崭露头角，试图自动发现自然规律。例如，Bongard和Lipson的Eureqa软件通过遗传编程实现符号回归，成功推导出多个经典公式。然而，这些方法普遍存在数据依赖大、缺乏形式验证、难以处理背景知识冲突等问题。与此同时，Sum-of-Squares优化和Positivstellensatz理论为多项式不等式的形式验证提供了坚实的数学基础。本文结合这两方面技术，提出了AI-Hilbert框架，旨在实现背景知识和实验数据的深度融合，自动推导科学定律，确保其数学上的严密性。
核心问题
核心问题在于如何在有限且噪声较大的数据条件下，结合背景知识自动推导出符合自然规律的多项式公式。传统符号回归方法在数据不足时容易产生偏差，深度学习模型虽能拟合复杂关系，但缺乏可验证性，难以提供科学依据。背景知识的不完整或错误也会导致推导结果偏离实际。现有方法多依赖人工设定模型结构或后续验证，效率低且不具备形式保证。如何利用数学优化技术，将背景知识形式化为多项式约束，并在保证推导正确性的同时，提高数据利用效率，成为亟待解决的问题。
核心创新
本研究的创新点在于：
- �� 将科学定律建模为多项式不等式和等式系统，利用Positivstellensatz定理实现其形式验证，确保推导的定律具有数学证明。
- �� 引入Sum-of-Squares技术，将多项式非负性问题转化为半正定规划，极大提升求解效率。
- �� 设计了多项式距离指标，结合优化目标，自动在背景知识和实验数据之间找到最优匹配关系。
- �� 通过混合整数线性和半正定优化，能在多项式时间内自动生成符合背景知识的科学定律，或识别背景知识中的冲突。
- �� 实现对背景知识正确性和完整性的形式验证，为科学理论修正提供数学依据。
方法详解
- �� 定义背景理论B为多项式等式和不等式集合，描述自然规律的约束条件。
- �� 将实验数据D转化为目标函数，最小化模型预测与实际观测的偏差。
- �� 构建多项式距离指标，衡量候选定律与背景知识的偏差。
- �� 利用Sum-of-Squares分解，将多项式非负性条件转化为半正定约束，形成半正定规划问题。
- �� 通过混合整数线性规划（MILP）或半正定规划（SDP）求解最优多项式证书。
- �� 利用Positivstellensatz定理，验证推导的多项式是否满足背景知识，确保其科学有效性。
- �� 若背景知识存在冲突，利用子集选择算法识别冲突点，修正背景知识或提出新假设。
- �� 最终输出满足数据和背景知识的科学定律，并提供数学证明。
实验设计
- �� 采用天体物理中的天体轨道数据、血液动力学模拟数据和引力波观测数据作为验证集。
- �� 比较基线包括符号回归、深度学习模型和AI-Descartes方法。
- �� 评估指标包括公式的拟合误差（如相对误差、Z-score）、推导公式的数学验证性和背景知识一致性。
- �� 超参数包括多项式最大阶数、SOS证书的阶数限制、优化求解时间限制。
- �� 通过逐步增加背景知识的复杂度，测试算法在不同知识冲突和噪声水平下的表现。
- �� 进行消融实验，验证Positivstellensatz阶数对推导准确率的影响，评估算法在大规模系统中的可扩展性。
结果分析
- �� 在天体物理数据中，算法成功推导出Kepler第三定律，误差低于10^-6，验证了其数学严密性。
- �� 在血液动力学模拟中，准确复现压力-流速关系，误差低于0.5%，优于传统符号回归。
- �� 在引力波观测数据中，推导出辐射功率公式，Z-score超过5，验证了其在实际观测中的适用性。
- �� 通过背景知识冲突检测，成功识别出部分公理的错误或不完整，推动理论修正。
- �� 实验还显示，算法在有限数据和噪声环境下，仍能保持较高的推导准确率（超过85%），优于现有符号回归方法。
应用场景
- �� 物理学中，自动推导基本定律，加速新理论的发现过程。
- �� 生物医学领域，用于建立复杂生物系统的数学模型。
- �� 工程设计中，快速验证设计参数与系统性能的关系。
- �� 长远来看，该方法可应用于自动修正和优化科学模型，推动人工智能在科学研究中的深度融合。
局限与展望
- �� 对背景知识的依赖较强，知识错误或不完整会影响推导结果。
- �� 高阶多项式的优化计算复杂度较高，限制了在超大规模系统中的应用。
- �� 对噪声的鲁棒性仍需提升，极端噪声环境可能导致推导偏差。未来需结合鲁棒优化技术，增强模型稳定性。
通俗解读 非专业人士也能看懂
想象你在厨房里做菜，手边有各种食材（背景知识）和菜谱（实验数据）。传统做菜靠厨师的经验（人工推导），但有时食材不新鲜或配比不对，结果不理想。现在，假设你有一台智能厨师（AI-Hilbert），它可以根据你提供的食材和菜谱，自动计算出最合适的配比和烹饪方法。它用数学的方式，把菜谱转化成一组公式（多项式），并通过优化算法不断调整，直到找到最符合实际的做法。这台智能厨师还能验证这些公式是否合理（形式验证），确保做出来的菜既符合传统口味，又能应对食材的变化。这样一来，不仅节省了试错时间，还能发现一些以前没有想到的美味组合。它的核心在于：用数学和算法，把厨房里的复杂问题变成一组可以自动求解的公式，让我们用最少的试验找到最好的菜谱。
简单解释 像给14岁少年讲一样
想象你在学校的科学实验室里，老师让你找出一个公式，能描述某个自然现象，比如为什么苹果会掉下来。以前，你可能会用老师给的书本知识，或者自己反复试验，但这个过程很慢，也不一定能找到最正确的答案。现在，有一个超级聪明的机器人（AI-Hilbert），它可以帮你用数学的方法，自动找到这个公式。它会把你观察到的苹果掉落的数据和一些已知的科学知识（比如重力定律）结合起来，然后用特别的数学技巧（叫多项式优化）来推导出最符合数据的公式。这个机器人还能告诉你，这个公式是不是符合所有已知的科学规律，确保它是正确的。这样一来，你只需要少量的实验，就能找到正确的自然规律，不用像以前那样反复试验。它就像一个聪明的数学侦探，帮你快速找到自然界的秘密！
术语表
Sum-of-Squares (SOS) Optimization (平方和优化)
一种将多项式非负性问题转化为半正定规划的数学技术，便于在优化中验证多项式的非负性。
用于确保推导的科学定律在数学上成立。
Positivstellensatz (正定定理)
来自实代数几何的定理，提供多项式在特定区域非负的证明条件，是验证多项式定律正确性的基础。
用于形式验证推导出的科学公式。
Polynomial Equalities and Inequalities (多项式等式与不等式)
用多项式表达的数学约束，描述科学定律和背景知识的核心形式。
建模科学定律的数学基础。
Mixed-Integer Linear/Semidefinite Optimization (混合整数线性/半正定优化)
结合整数变量和连续变量的优化技术，用于求解多项式优化问题。
实现科学定律的自动推导。
Background Theory (背景知识)
已知的科学公理、定理和定律，作为推导新公式的基础。
在算法中作为约束条件输入。
Scientific Law (科学定律)
描述自然现象的数学公式或关系，具有普遍性和可验证性。
算法的目标输出。
Polynomial Certificate (多项式证书)
证明多项式在某区域非负的数学表达，用于验证科学定律的正确性。
确保推导的公式具有数学证明。
Axiom (公理)
无需证明的基本假设或规则，用于推导其他定律。
背景知识的组成部分。
Optimization Problem (优化问题)
在给定约束下寻找最优解的数学模型。
推导科学定律的核心步骤。
Inconsistent Background Knowledge (背景知识不一致)
背景公理之间存在矛盾，无法同时满足。
算法能识别并修正此类问题。
开放问题 这项研究留下的未解疑问
- 1 尽管该方法在有限数据和噪声环境下表现良好，但在极端噪声或高阶多项式模型中，鲁棒性和计算复杂性仍需提升。未来研究应结合鲁棒优化和高阶多项式技术，增强模型的稳定性和适应性。
- 2 背景知识的自动提取和验证仍是难点。如何高效地从文献或数据库中自动构建准确的多项式公理体系，是推动该方法普及的关键。
- 3 目前算法主要在理论验证和小规模实例中表现优异，如何扩展到大规模复杂系统，仍需优化算法的求解效率和存储能力。
- 4 对动态系统和非多项式关系的建模能力有限，未来应探索非多项式的形式化表达和对应的优化技术。
- 5 算法在处理多源异构数据时的融合策略不足，需开发多模态数据整合技术，以适应实际复杂场景。
应用场景
近期应用
基础科学定律自动推导
利用背景知识和有限实验数据，快速自动推导天体物理、流体力学等领域的经典定律，减少人工推导时间。
科学模型验证与修正
通过形式验证，检测已有模型中的不一致或错误，辅助科学理论的修正和完善。
工程优化设计
在工程设计中自动验证参数关系，提升设计效率和可靠性，减少试验成本。
远期愿景
自动化科学研究平台
结合大规模数据和背景知识库，建立全自动的科学发现系统，推动人工智能在基础科学中的深度应用。
跨学科理论融合
实现物理、化学、生物等多领域知识的统一建模，推动多学科交叉创新，促进新科学理论的诞生。
原文摘要
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 best fits the data 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 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 Positivstellensatz certificates. The optimization techniques leveraged in this paper allow our approach to run in polynomial time with fully correct background theory under an assumption that the complexity of our derivation is bounded), 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 axioms and experimental data.
参考文献 (20)
Best Subset Selection via a Modern Optimization Lens
D. Bertsimas, Angela King, R. Mazumder
Nonconvex Piecewise Linear Functions: Advanced Formulations and Simple Modeling Tools
Joey Huchette, J. Vielma
Semidefinite Optimization and Convex Algebraic Geometry
Grigoriy Blekherman, P. Parrilo, Rekha R. Thomas
Data-driven discovery of partial differential equations
S. Rudy, S. Brunton, J. Proctor 等
Optical Clocks and Relativity
C. Chou, D. Hume, T. Rosenband 等
Discovering governing equations from data by sparse identification of nonlinear dynamical systems
S. Brunton, J. Proctor, J. Kutz
Partial facial reduction: simplified, equivalent SDPs via approximations of the PSD cone
Frank Permenter, P. Parrilo
Chordal Graphs and Semidefinite Optimization
L. Vandenberghe, Martin S. Andersen
Multivariate Statistics and Machine Learning Under a Modern Optimization Lens
D. Bertsimas
KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
Nathan Fulton, Stefan Mitsch, Jan-David Quesel 等
Information-Theoretic Limits on Sparse Signal Recovery: Dense versus Sparse Measurement Matrices
Wei Wang, M. Wainwright, K. Ramchandran
Automated reverse engineering of nonlinear dynamical systems
J. Bongard, Hod Lipson
Progress in computational mixed integer programming—A look back from the other side of the tipping point
R. Bixby, E. Rothberg
The Elements of Statistical Learning: Data Mining, Inference, and Prediction
D. Ruppert
Semidefinite programming relaxations for semialgebraic problems
P. Parrilo
A nonlinear programming algorithm for solving semidefinite programs via low-rank factorization
S. Burer, R. Monteiro
Locality, Bell's inequality and the GHZ theorem
A. Fahmi
Global Optimization with Polynomials and the Problem of Moments
J. Lasserre
被引用 (20)
The Need for Verification in AI-Driven Scientific Discovery
Bridging the Gap Between Scientific Laws Derived by AI Systems and Canonical Knowledge via Abductive Inference with AI-Noether
Verification and validation for trustworthy scientific machine learning
Scaling function learning: A sparse aerodynamic data reconstruction method for various aircraft shapes
Understanding of Tile Hollow Sound
Physics-assisted feature-augmented metamodels to predict the keyhole geometry in laser additive manufacturing
A multi-subnets physics-informed neural network (Ms-PINN) model for transient heat transfer analysis in materials with heterogeneous microstructures
Automated Modeling Method for Pathloss Model Discovery
SynPAT: A System for Generating Synthetic Physical Theories with Data
AI-Newton: A Concept-Driven Physical Law Discovery System without Prior Physical Knowledge
From reductionism to realism: holistic mathematical modelling for complex biological systems.
A Unified Data-Driven Framework for Efficient Scientific Discovery
Automating the practice of science: Opportunities, challenges, and implications
Symplectic Neural Flows for Modeling and Discovery
Discover physical concepts and equations with machine learning
Context-Aware Reasoning On Parametric Knowledge for Inferring Causal Variables
Automating the Practice of Science - Opportunities, Challenges, and Implications
Decoding complexity: how machine learning is redefining scientific discovery
Using machine learning to find exact analytic solutions to analytically posed physics problems
When AI meets physics: Beyond prediction, towards understanding