摘要

从原子核与电子的相互作用预测物质的结构、性质和反应，是第一性原理研究的核心目标，但统一的微观模型并不自动带来高效计算，也不等同于化学知识的公理化。随着机器学习被用于势能面逼近、控制方程发现、证明搜索与实验设计，数据驱动方法与演绎方法的关系需要超越“经验拟合替代理论”或“机器学习猜测、形式系统验收”的简单分工。本文采用专题式批判性叙述综述，围绕结构约束学习、可导出的规律发现、学习—验证闭环、统计有效推断及跨尺度有效理论，比较代表性研究的对象、假设、证据类型与适用边界。本文指出，经验准确性、统计有效性、结构一致性、数值误差控制和形式正确性是相互关联但不可替代的评价维度；符号表达不等于机制解释，逻辑可导出不等于物理适用，保守或等变的模型也不自动获得分布外可靠性。以反应网络、吸附动力学和学习粗粒化为案例，本文进一步讨论参数可识别性、误差传播和闭合性，提出以条件化知识单元、可审计证据链及实验—逻辑双重反馈组织科学发现。在此基础上，本文辨析反应网络条件定理、验证反馈驱动的形式语言搜索、近似有效域、最小有效状态与机制区分实验五类研究机会，区分已有成果、待检验设想及构成实质性突破的证据标准，并给出反应网络定理发现的集成研究设计。机器学习与形式化方法的深层协同，应体现为共同构造可复用的中间理论，而非追求脱离假设与实验的全能预测器。

**关键词：**科学机器学习；公理化；形式化验证；可导出科学发现；不确定性量化；计算化学；有效理论

1 引言：从“能够预测”到“能够积累可靠知识”

能否从原子的结构推出物质的性质、结构与反应，是理解现代科学方法的一条重要线索。Dirac在1929年强调，相关基本规律与实际求解多电子问题之间存在巨大距离[1]。Anderson随后提出的“More Is Different”则提醒人们：接受微观还原，并不意味着复杂体系可以不经新的概念与组织原则而直接重建[2]。两者并不矛盾：前者涉及统一理论的基础，后者涉及从基础到有效描述的建构问题。

机器学习为这一建构过程增加了新的工具。它既可以逼近昂贵的物理计算，也可以搜索控制方程、提出候选证明或选择下一次实验。然而，预测能力的提升没有消除“什么算作知识”的问题。一个在测试集上准确的模型，可能违反基本约束；一个通过形式检查的定理，可能依赖不适用的物理假设；一个拟合简洁的公式，也可能只是多个观测等价解释之一。关于人工智能科学发现中验证需求的近期讨论，已经把数据一致性、背景知识和可导出性之间的连接作为明确议题[3]。

本文的中心问题因而不是机器学习与公理化孰优孰劣，而是：**二者如何共同产生既有经验依据、又有明确推理边界，并能跨问题复用的科学知识？**围绕这一问题，本文区分知识的发现方式、成立依据和现实适用性，比较不同研究路线的保证对象，并以化学展示各层证据如何衔接。第11节进一步将综述结论转化为五类AI可推进的研究问题，第12节给出知识组织、集成研究设计与评价协议。

本文属于专题式批判性叙述综述，不是遵循预注册流程的系统综述，也不报告文献计量意义上的覆盖率。选文围绕“科学机器学习与物理约束”“符号发现与理论推导”“机器学习与形式验证”“统计保证”“化学及粗粒化”五组主题，以代表性原始研究、正式出版版本及官方证明器文档为主要依据，并沿核心工作的参考文献补充基础研究。文献核验截至2026年10月9日；正式出版时间与预印本时间不一致时优先采用正式版本。在五组主题之外，本文围绕网络结构判据、文法约束贝叶斯优化、反例驱动符号回归、近似有效性与结构保持粗粒化进行定向补充检索。新增机会判断以已检索代表性文献为边界，不构成对研究空白的穷尽性确认。本文提出的证据分类、条件化知识单元及研究议程属于综合分析，不宣称已经存在一个实现全部环节的通用系统。

2 概念框架：发现、证明与适用性并非同一维度

2.1 第一性原理、公理化与形式化的边界

第一性原理预测关注如何从选定的基本物理模型得到具体体系的结果；公理化关注研究对象、基础假设、定义和推理规则的组织；形式化则把这些内容表达为精确对象，使推导或程序性质能够接受机器辅助分析乃至检查。三者可以合作，但不存在自动的蕴含链：“使用薛定谔方程”不等于“没有近似”，“得到符号公式”不等于“建立公理体系”，“证明被机器接受”也不等于“现实满足模型”。

公理化还不要求从最低层粒子开始。Lieb与Yngvason以绝热可达性及其结构公理建立熵理论，表明宏观描述本身可以成为严格演绎的对象[4]。因此，化学既可以研究电子结构的严格数学基础，也可以在反应网络或热力学层次上建立公理体系；后者不必等待前者全部完成。

对于数据提出的候选规律$\varphi$和背景理论$T$，至少应区分三种关系：$\varphi$在观测上拟合良好；$T$与$\varphi$相容；$T\vdash\varphi$，即存在在指定演绎系统中的推导。相容性远弱于可导出性。若背景假设自相矛盾，经典逻辑中的可导出性甚至可能失去区分作用。因此，检验公式时必须同时审查假设、推导和目标命题，不能以“没有与已知知识冲突”代替“已经从已知知识证明”。这一差别也是理解AI-Descartes与AI Hilbert的关键。

2.2 五种证据不是从低到高的单一阶梯

为比较不同研究，本文采用表1的分析框架。它是针对本文问题的分类，而非一个已有的通用认证标准。

表1 不同证据的保证对象与不可替代性

证据类型	典型问题	主要条件	不能据此自动宣称
经验检验	在已测条件下是否准确？	数据质量、独立评估、实验可重复性	对所有未观测条件成立
统计保证	覆盖率、风险或估计误差受到何种控制？	抽样、可交换性或其他分布条件	每个个体都具有相同条件保证
结构保证	守恒、对称性或正性是否由模型结构保证？	正确的变量与模型假设	预测数值和机理必然正确
数值保证	离散化、截断、舍入和求解误差有多大？	算法与方程的明确条件	被求解模型充分描述现实
形式保证	指定命题是否由假设严格推出？	精确规格、证明规则与可信检查基础	物理前提真实、目标翻译无误

这五种证据分别可见于结构化势能模型、严格数值分析、形式验证和统计推断等研究。它们并不互斥：一个神经网络可以有准确的经验表现，同时满足严格结构约束；某种概率保证本身也可以被形式化。相反，具有解析表达式的模型，可能没有可靠实验依据。真正需要报告的是“哪些性质在什么条件下有保证”，而不是笼统称模型“可信”或“已验证”。

3 第一性原理化学为何仍然需要中间理论

3.1 统一模型、存在定理与可用求解器

在通常的非相对论库仑模型中，体系哈密顿量可写为

$$\hat H=\hat T_e+\hat T_N+\hat V_{ee}+\hat V_{eN}+\hat V_{NN}, \qquad \hat H\Psi=E\Psi.$$

其中包含电子与原子核的动能及其相互作用。Hohenberg–Kohn理论在明确条件下把基态问题与电子密度泛函联系起来[5]。物质稳定性研究则在相应费米子库仑模型中建立随粒子数线性增长的能量下界，说明严格微观分析能够给出重要宏观约束[6]。但存在性、唯一性或稳定性定理，并不自动给出任意分子与环境下的高效算法，更不提供所有化学概念的现成定义。

近似与严格性也不是对立项。玻恩—奥本海默近似把电子与核运动的尺度差异转化为有效描述；Hagedorn与Joye在特定条件下构造了具有指数小误差估计的时间依赖近似[7]。这表明，需要问的不是“是否使用近似”，而是近似参数、成立条件和误差边界是否明确。

计算复杂度进一步约束了对通用求解器的期待。Schuch与Verstraete研究了相互作用电子模型的复杂性及其对密度泛函可计算性的限制[8]；Liu等证明了特定两粒子约化密度矩阵的$N$-可表示性判定问题具有QMA完全性[9]。这些是指定输入形式、精度和问题族下的最坏情况结论，不等于每个实际分子都难算，也不能把“尚无理由期待通用高效算法”改写成已经证明量子计算对化学普遍无效。

3.2 从量子状态到化学对象存在概念与尺度连接

给定组成并没有唯一指定实验结果。结构预测需要区分可能构型、给定温压下的稳定状态，以及特定制备过程能在观察时间内到达的状态。即使电子计算准确，结构搜索、自由能采样和竞争反应也仍可能决定结论。

分子结构问题进一步体现了上层概念的非平凡性。Sutcliffe与Woolley对完整量子描述与通常分子结构概念之间的关系提出了基础性讨论；Mátyus的pre-Born–Oppenheimer研究则探索电子与原子核同时量子化时的结构描述[10,11]。这些工作不支持把“分子结构只能从外面塞进去”作为无争议结论。核间距离和关联可以研究，但化学家使用的稳定构型、键连接与分子身份，需要结合局域化、时间尺度及有效描述理解。

因此，机器学习最值得介入的并非仅是加速一个巨大方程，而是帮助构造和检验多个中间层：势能、反应坐标、速率、反应网络及宏观状态变量。每个中间层都同时具有经验任务和理论任务。

4 理论约束学习：从拟合惩罚到结构化求解

4.1 已知结构应尽可能进入模型，而非全部交给数据重学

Behler–Parrinello势将神经网络用于高维势能面表示，为以学习模型替代昂贵电子结构评估提供了重要路线[12]。NequIP进一步将三维欧氏群等变性编码进图神经网络，在其研究体系中获得较高数据效率[13]；MACE通过高体阶等变消息传递改善精度与计算代价的平衡[14]。这些工作说明，物理结构可以改变假设空间，而不只是作为训练结束后的解释。

以标量势能$E_\theta(R)$为例，若对相关平移、旋转及同类原子置换保持适当不变性，并通过$F_\theta=-\nabla_R E_\theta$定义力，那么相应等变关系和保守力结构可在连续数学模型层面得到约束。但这不证明势能值准确，也不意味着实际浮点实现、数值积分与分布外构型已整体通过形式验证。一个对称但错误的势能面仍然可能给出错误的反应势垒。

此外，硬约束只应施加于确实适用的性质。如果目标体系包含外场、开放边界或被遗漏的自由度，错误的对称性或守恒假设可能成为无法通过增加数据消除的偏差。结构设计的价值与风险来自同一来源：它排除了某些候选模型。

4.2 物理信息损失不等于形式保证

物理信息神经网络（physics-informed neural networks，PINNs）把微分方程残差及初边值条件加入学习目标，从而在数据与物理方程之间建立联合优化[15]。但有限配置点上的残差损失较小，并不自动证明整个连续区域上的方程误差较小。Krishnapriyan等展示了对流、反应和扩散类问题中的训练失败，并分析了损失病态与优化困难[16]。

这一批评不应被扩大为“PINNs不可能严格分析”。Mishra与Molinaro在适当方程稳定性和采样条件下，把泛化误差与训练误差等量联系起来，提供了明确的理论界[17]。这使文献比较的重点从是否使用神经网络，转向具体方程、残差范数、稳定性常数、采样规则和优化结果能否共同支撑误差结论。

因此，至少应区分三种情况：把约束作为损失中的软惩罚；通过结构使某种性质恒成立；对具体求解结果提供经过验证的误差界。三者可以组合，但不能互相冒充。

4.3 机器学习也可以直接充当物理方程的数值表示

Pfau等使用神经网络量子态计算激发能与振子强度，展示了神经网络作为量子求解表示、而非仅对实验标签做回归的作用[18]。这类工作使“机器学习是经验方法，第一性原理是演绎方法”的二分失去准确性。

作为数学说明，若$\psi_\theta$属于给定自伴哈密顿量的适当定义域，且期望值被精确计算，则变分原理给出

$$E[\psi_\theta]=\frac{\langle\psi_\theta,\hat H\psi_\theta\rangle} {\langle\psi_\theta,\psi_\theta\rangle}\geq E_0.$$

但是，随机采样得到的能量估计并非每次都严格高于$E_0$；仅有上界也不构成双侧误差证书。这一例子说明，可靠性需要从数学对象一直追踪到计算估计，而不能只借助“变分”或“第一性原理”的名称。

5 从数据规律到可导出发现：符号表达只是起点

5.1 方程发现的进展与归纳边界

SINDy在预先给定的候选函数库中，通过稀疏识别发现动力学方程[19]；AI Feynman利用量纲、对称性和可分离性等结构缩小符号回归搜索空间[20]。两者的重要贡献不是取消先验，而是把“哪些规律值得搜索”组织为可操作的归纳偏置。其边界也因此包括变量选择、函数库或表达式语法、噪声处理，以及观测是否足以区分候选模型。

有限拟合本身无法唯一确定普遍规律。若$f$通过有限观测点$x_1,\ldots,x_n$，则

$$g(x)=f(x)+a\prod_{i=1}^{n}(x-x_i)$$

在相同点上也给出完全相同的值，却可在其他位置产生差异。这一代数例子并不是对某种学习算法的反驳，而是说明：从数据推广必然依赖模型类别、复杂度偏好、机制假设或新增实验。符号形式提升了可读性，但不会自动消除归纳的不确定性。

5.2 AI-Descartes与AI Hilbert：理论不只参与筛选，也参与构造

AI-Descartes将符号回归与自动推理结合，利用背景理论评价候选公式的可导出性及相关偏差，并在包括Langmuir吸附模型在内的案例上展示了这一流程[21]。相较于单纯按拟合误差排序，它引入了另一维信息：两个经验表现接近的表达式，可能与理论具有完全不同的关系。其能力依赖输入理论、搜索语法和推理工具；不能把案例中的重发现等同于从原始数据自主建立完整物理学。

AI Hilbert把数据与半代数形式的背景知识统一进优化框架，使用多项式优化及平方和等证书工具，构造同时受数据与可导出性约束的规律[22]。与先产生候选再检验的思路相比，其特点在于更紧密地把推导证据纳入求解过程；限制则来自表示语言、证书阶数与优化规模，不能把它理解为对任意微分方程、积分和逻辑命题的通用证明器。

对这两条路线的比较表明，理论至少可以在搜索前、搜索中和搜索后发挥作用：规定允许的表达式，参与候选生成，或区分相近的经验解释。另一方面，数值优化产生的候选证书，与在独立证明器中检查过的精确证明仍应区分。若需要端到端形式保证，还须明确数值容差、证书重构和最终检查的处理方式；这是本文由证据分类得到的要求，而非断言上述系统已经实现了全部步骤。

5.3 可导出性不等于因果机制成立

一种规律可以在已有模型中被证明，却无法由当前数据判定该模型是否是唯一机制解释。反过来，观测上的跨环境稳定性可以帮助因果识别，但仍需要明确的干预与结构假设。Peters等的 invariant prediction 研究展示了如何利用环境间不变性建立因果识别和置信陈述[23]，而不是从任何相关关系直接读出因果方向。

因此，综述中应分别评价公式恢复、机制识别和理论推导。把某个已知公式重新拟合出来，是有意义的算法检验；证明该公式由给定背景推出，是另一种成果；发现此前未知且经新实验检验的规律，则需要额外证据。三者不能仅以“自动科学发现”一个标签混合计数。第11.2节据此进一步讨论：如何利用验证过程中的反例、未完成状态和计算成本来指导形式语言搜索，而不只是评价最终表达式。

6 学习与形式验证：把启发式发现和可信检查分离

6.1 候选可以不可信，检查机制必须有明确边界

Proof-carrying code把程序与可检查的安全证据一起交付，为“复杂生成、相对独立检查”的组织方式提供了经典范例[24]。反例引导归纳合成则让候选生成器与验证器交互：验证器寻找违反规格的输入，再把反例交给生成器改进候选[25]。

将这一思想用于学习系统，不意味着机器学习自己宣称“已经验证”即可。Reluplex对特定ReLU网络性质进行可满足性模理论（SMT）求解，展示了对已训练模型检查规格的路径[26]；Neural Lyapunov Control将控制器及Lyapunov函数学习与形式反例搜索结合，研究指定区域内的稳定性[27]。这些工作的保证对象是明确的模型、区域与规格，而非所有真实环境。

还必须保留“未知”结果。随机测试没有找到反例，不等于验证完成；验证器超时，也不等于命题为假。合理的系统应分别记录已获证明、已获反例以及尚未解决，并说明结论依赖的算术语义和数值容差。

6.2 证明搜索能力与证明可信度可以解耦

Lean 4以精确的逻辑表达和证明检查支持复杂的自动化过程[28]。AlphaProof进一步把强化学习与形式证明反馈结合，在数学推理任务上展示了以机器可检查结果训练搜索策略的能力[29]。其意义不是神经网络内部推理已经天然正确，而是候选证明可以接受外部规则检查。

但是，形式检查只对输入的命题负责。自动形式化可能遗漏量词、边界条件或目标对象；随意加入假设也可能使本来困难的命题变成无意义推论。Lean官方文档明确区分可接受的基础公理与需要审计的附加公理，并说明新增公理并不会自动得到一致性保证[30]。因此，面向科学的证明系统还需要检查“形式化的命题是否就是原来的科学主张”，并记录公理依赖、库版本及未完成证明占位符。

6.3 形式方法也能够处理数值分析，而非只处理符号演算

科学计算常被误认为不适合严格验证，因为结果通常是近似数值。Immler在Isabelle/HOL中建立经过验证的常微分方程求解工具，并将其用于Lorenz吸引子相关的严格计算[31]。该工作说明，截断、舍入、区间包含与程序执行可以成为证明链的一部分。

这提供了一种比“神经网络给出公式，证明器证明公式”更宽的结合方式：学习系统寻找高效近似或有利区域划分，经过验证的数值算法为特定结果建立包络。能否扩展到高维化学体系仍需研究，但不存在原则上只能在经验数值与纯符号证明之间二选一的必要。

7 统计推断与实验：严格性不要求消除一切概率

7.1 概率命题可以严格证明，但量词不能改变

Lei等建立的分布无关回归预测推断，为保形预测提供了重要基础[32]。在相应可交换性、校准与构造条件下，可得到

$$\Pr\{Y_{n+1}\in C_D(X_{n+1})\}\geq 1-\alpha.$$

这是关于校准数据与新样本随机性的边际覆盖保证，不等于对每个固定$x$都有相同条件覆盖，更不是模型对每一个分子的“正确概率”。Barber等证明了无额外分布条件时非平凡条件覆盖的限制[33]；其后关于非可交换数据的研究，则通过新的条件与误差分析处理偏离，而非允许任意分布变化仍无条件有效[34]。

这对分子模拟尤其重要：轨迹中的相邻构型、主动采样选出的困难样本，以及部署中出现的新反应区域，并不能默认视为相同机制产生的独立样本。把随机划分测试集上的覆盖率直接外推为整条反应轨迹的可靠性，是对保证对象的改变。这里的批评来自统计条件与模拟任务的对照，而非否定保形方法在有适当设计时的价值。

7.2 黑箱预测与有效推断并不矛盾

Prediction-powered inference利用预测结果辅助估计总体量，同时用可靠标注数据校正误差，并在规定条件下给出有效置信推断[35]。它表明，一个模型即使没有可解释的内部机理，也可以被纳入严格的科学推断程序。

以总体均值为例，对独立于评估样本训练的固定预测器$f$，若有同分布的未标注输入$\widetilde X_i$和标注样本$(X_j,Y_j)$，可考虑

$$\widehat\mu= \frac{1}{M}\sum_{i=1}^{M}f(\widetilde X_i) +\frac{1}{n}\sum_{j=1}^{n}\bigl(Y_j-f(X_j)\bigr).$$

在期望存在等条件下，两项期望相加等于$\mathbb E[Y]$。这是对偏差校正思想的简化说明，不表示重复使用训练数据无需处理，也不表示任何置信区间都自动具有精确有限样本覆盖。其启示是：科学可信性有时来自预测器外围的抽样和校正设计，而不要求把预测器本身变成完整理论。

7.3 模型校准不能代替模型适用性检验

Kennedy与O’Hagan在计算机模型校准中显式区分模型输出、模型差异和观测误差，为这一边界提供了经典框架[36]。贝叶斯后验反映的是给定模型与先验条件下的推断；后验区间很窄，并不自动说明模型差异可以忽略。

因此，对化学模型至少要区分参考量子方法误差、学习代理误差、采样误差及实验测量误差。使用密度泛函计算生成大量训练标签，可以提高某种参考模型的求解效率，但标签数量增长不会自行消除该参考模型对现实的系统偏差。实验并不是完成形式证明后可以删除的最后一步，而是判断整套假设是否适用的持续依据。

8 代表性路线比较：理论参与方式与保证边界

表2 代表性工作的协同机制与证据边界

路线与代表工作	学习或搜索的对象	理论／验证的作用	主要边界
NequIP、MACE[13,14]	原子间势及局域表示	在结构中编码等变关系	对称性不保证全局能量精度
PINNs及误差分析[15,17]	方程解或未知参数	残差约束；条件化误差估计	连续域控制依赖稳定性、采样和优化
SINDy、AI Feynman[19,20]	稀疏方程与符号表达式	函数库、量纲等约束搜索	拟合与符号简洁性不等于机制证明
AI-Descartes[21]	候选科学公式	检查其与背景理论的推导关系	依赖理论内容及推理能力
AI Hilbert[22]	规律及推导证书	将数据与半代数证书联合优化	受表示语言和证书阶数限制
Neural Lyapunov Control[27]	控制器与稳定性证书	验证条件并反馈反例	仅针对指定动力学与区域
AlphaProof[29]	形式证明	检查器反馈驱动学习与搜索	不自动保证科学命题翻译正确
保形预测与预测辅助推断[32,35]	预测集合及总体统计量	给出条件明确的统计有效性	非逐点、无条件分布外保证

上述工作不能用一个“是否神经符号”标签充分比较。真正影响科学用途的是：背景知识在哪里进入流程，学习的对象是什么，证据由谁产生和检查，哪些误差没有被覆盖，以及流程失败时是否能定位原因。也不应预设形式证明总是最昂贵或最优的终点；对于某些实验估计任务，统计设计比把预测网络全部形式化更切合目标。

9 化学案例：把结构、推理与实验连接起来

9.1 反应网络：可学习速率与可证明结构

对封闭、定容体系，设浓度向量为$x$，化学计量矩阵为$S$，可学习的反应速率为$r_\theta(x,T)$。采用

$$\dot x=S\,r_\theta(x,T).$$

若$c^\mathsf TS=0$，则沿模型解有

$$\frac{\mathrm d}{\mathrm dt}(c^\mathsf Tx)=0.$$

这说明速率可以交由数据拟合，而某些守恒量能够由结构对所有参数保证。这里采用的矩阵约定下，守恒量对应$S$的左零空间。然而，该结果不证明速率正确、反应集合完整或浓度非负；正性还需要速率在边界满足适当条件。把所有速率都设为零也满足上式，足以说明“守恒”与“准确”不可混淆。

更强的上层结论来自化学反应网络理论。Feinberg的缺陷零定理在质量作用律、弱可逆及缺陷为零等条件下，给出每个正化学计量相容类中正平衡的唯一性和相关局部稳定性[37]。其中缺陷为$\delta=n_c-\ell-s$，分别涉及反应复合物数、连接类数和化学计量子空间维数。它并不是一般多稳态问题的完整判据，更不负责从电子结构中发现网络本身。

网络的发现属于另一层任务。第一性原理纳米反应器通过加速分子动力学探索没有预先指定的反应路径[38]；Chemoton 2.0把量子化学计算组织成自动反应网络探索流程[39]。因此可形成“物理计算／学习发现候选网络—动力学拟合—网络性质推导”的合作，但前一步遗漏关键反应时，后一步在候选网络上成立的定理并不能弥补这一遗漏。沿此区分，第11.1节将网络实例预测与条件定理发现作为两个不同层次的研究目标。

9.2 势垒、自由能与误差传播

Proppe与Reiher研究了带噪声反应网络中的机理推断，把动力学相关性、敏感性与不确定性纳入机制分析[40]。这一方向的重要性在于，能量误差不是停留在单次评估中的孤立数字，它可能改变下游反应选择和速率。

作为条件化的数学示例，假设采用速率模型$k=A\exp[-\Delta G^\ddagger/(RT)]$，且比较中前因子$A$保持相同，则

$$\left|\log\frac{\widetilde k}{k}\right| \leq\frac{\varepsilon}{RT} \quad\text{当}\quad |\widetilde{\Delta G}^\ddagger-\Delta G^\ddagger|\leq\varepsilon.$$

在298 K附近，$RT\ln10$约为1.36 kcal/mol，因而该量级的活化自由能差异对应约一个数量级的速率差。这是所写模型下的传播关系，不是对所有方法的典型势垒误差作统计断言。

同理，若结构A与B的自由能计算具有已证明的误差界，只有当

$$\widetilde G_A+\varepsilon_A<\widetilde G_B-\varepsilon_B$$

时，才能据此推出$G_A<G_B$。这样的排序证书仍只覆盖两个候选结构及给定模型，不证明搜索中不存在第三个更稳定构型。这使“局部误差控制”和“搜索完整性”成为必须分别报告的指标。

9.3 吸附模型：形式分析应反过来指导实验

Langmuir吸附理论提供了一个从简单假设产生可检验关系的经典例子[41]。以下采用理想化单类位点动力学作推导说明，假设$p\geq0$且$k_a,k_d>0$：

$$\dot\theta=k_a p(1-\theta)-k_d\theta.$$

稳态给出$\theta_{\mathrm{eq}}=Kp/(1+Kp)$，其中$K=k_a/k_d$。数据拟合可以提出这一曲线，演绎分析则说明它依赖什么动力学模型，并可证明相应单调性与稳态唯一性。

更重要的是，仅靠稳态数据只能识别比值$K$，不能分别识别$k_a$与$k_d$。在该模型中，固定压力下的动态弛豫率为$\lambda=k_a p+k_d$；因此动态观测能提供稳态曲线缺少的信息。这一可识别性分析直接影响实验选择，而不是在论文末尾附加一个正确性说明。

Clarkson等关于符号发现的贝叶斯实验设计研究，把区分候选关系所需的信息纳入下一次测量选择[42]。从这一视角看，形式反例和实验反例具有不同作用：前者揭示某个声明不由指定模型保证，后者揭示模型与现实之间的不充分对应；二者都应能触发模型修订。

10 更深的协同：发现并检验有效中间变量

10.1 不只是学习答案，还要学习怎样描述问题

Champion等把表示学习与稀疏动力学识别结合，探索能够同时简化坐标和控制方程的潜在空间[43]。Wang与Gómez-Bombarelli的粗粒化自编码器研究则把学习映射与分子有效模型联系起来[44]。这些工作把研究对象从“已知变量之间的函数”扩展到“哪些变量值得保留”。

这一目标与化学的中间概念直接相关：反应坐标、局部环境或有效状态变量应当压缩微观信息，但不能丢失决定目标性质的部分。与此同时，Mori的投影方法表明，消去自由度后通常会出现记忆项与涨落作用[45]。因此，学习一个低维平衡势，不能自动保证低维动力学闭合，更不能自动保证反应时间正确。

10.2 闭合误差、长期误差与信息保留必须同时检查

以下给出本文用于组织问题的条件化数学示例，不把它当作已解决一般化学粗粒化的结论。设微观离散演化为$F$，学习到的宏观变量为$z=\phi(x)$，宏观演化为$G$。若在相关且对微观演化不变的区域$\Omega$内，对每个$x$均有

$$\|\phi(F(x))-G(\phi(x))\|\leq\varepsilon,\qquad x\in\Omega,$$

且$G$在比较轨迹经过的区域具有Lipschitz常数$L$，令$z_{n+1}=G(z_n)$，则投影轨迹误差满足

$$e_n:=\|\phi(F^n(x_0))-z_n\| \leq L^ne_0+\varepsilon\sum_{j=0}^{n-1}L^j.$$

它说明局部拟合误差还必须经过动力学传播分析：当$L>1$时，上界可能快速增大。小的一步损失并不保证长时间预测可靠。

闭合本身也不是充分目标。常数映射$\phi(x)=0$可以产生平凡的闭合关系，却丢失全部有用信息。若目标可观测量为$O(x)$，还需要存在宏观读出$o(z)$，使$|O(x)-o(\phi(x))|\leq\delta$。若$o$具有Lipschitz常数$L_o$，则可得到目标误差上界$\delta+L_o e_n$。这将“变量有用”“动力学近似”和“误差传播”连接成了同一个需要证据支撑的问题。

实际研究不一定能获得全域严格上界，可以先在明确分布或局部区域内建立统计或数值保证；关键是不能把它们未经说明地改写成全域定理。如果闭合失败，应允许增加状态变量、记忆或随机性，而不是只增加网络规模。第11.4节进一步讨论如何把这一原则转化为最小有效状态与必要记忆的研究问题。

11 从现有进展到AI可突破的研究问题

前述研究说明，机器学习与形式化方法的协同具有多种实现方式，但能够自动执行更多步骤，并不等于获得了更多科学知识。本文进一步区分两类成果：科学突破表现为新的定理、机制、有效描述或修正既有认识的反例；方法突破表现为在明确任务与资源预算下，更高效、更可靠地获得此类知识。二者可以相互支持，却应独立评价。以下五个方向是基于代表性文献及前述分析提出的研究议程，不是已被证明可行的统一方案，也不意味着相邻研究尚无人开展。

11.1 反应网络的条件定理与结构判据发现

反应网络提供了一个适合结合组合搜索、数值探索与严格推导的研究层次。Yao等研究全开放质量作用律网络，改进正反馈环与多重稳态之间的相关结果，提出生成非多重稳态网络的确定性操作，并利用相应数据及网络表示训练图注意力模型[46]。该工作同时包含理论成果和机器学习分类，但不能据此声称其中的定理由AI自主发现。因此，单纯训练新的图网络预测多重稳态性，已不足以代表这里设想的突破。

更具知识价值的目标是从实例分类推进到条件定理：给定一种网络变换或局部结构，寻找保证目标性质保持的充分条件，并研究哪些条件可以削弱。候选命题可以示意为“对网络族$\mathcal N$中的任意网络，只要结构条件$C$成立，则对允许的参数集合均有性质$P$”。这里必须明确动力学类别、参数量词和相容类；正稳态唯一性、稳态存在性以及多个稳定稳态是不同目标，不应混为一项分类标签。

AI可用于生成候选网络与结构条件、从证书或反例中提取模式，以及寻找便于推广的中间引理。验证过程则分别提供可检查的成立证据、明确反例或未知状态。例如，系统提出“某类扩展保持非多重稳态性”后，反例可以推动其增加连接限制，或缩小动力学适用范围；但新条件是否超出既有理论，需要进一步进行文献和逻辑关系核查。

这一方向的实质性成果可以是覆盖已有判据未直接覆盖情形的新充分条件、具有适用边界的构造定理，或揭示某种推广失败的最小反例。不能把有限规模上的枚举通过自动提升为任意规模网络族的定理，也不能把数值求解器未找到第二个平衡点标为“不存在”。在数据层面，应区分有证书的标签、数值候选和未知实例；在评价层面，应按结构族、生成操作或网络规模隔离数据，避免近重复样本掩盖真正的泛化难度。

11.2 反例与证明反馈驱动的形式语言搜索

将科学模型或命题表达为受文法约束的符号对象，可以使发现问题进入组合优化框架。BOSS已经用字符串核构造高斯过程代理，并在具有语法约束的字符串空间中进行贝叶斯优化[47]。Błądek与Krawiec则把形式约束、SMT验证及反例反馈融入符号回归的遗传编程[48]。结合第5节的AI Hilbert可知，文法搜索、学习与验证的简单串联并非空白；需要回答的是验证反馈如何实质性改变搜索效率与知识产出。

第一类问题是反例的可迁移利用。反例不应只有一个扣分作用；其涉及的边界、符号结构或参数关系，可能对其他候选具有信息价值。但学习到的相似性只能指导搜索，不能未经证明就把一类相似表达式全部排除。严格剪枝必须以相应的蕴含关系为依据，启发式降权则应保留其可能出错的身份。

第二类问题是联合建模规律价值与验证成本。有用但难证明的候选，不应因短预算超时就被标为错误；容易证明的恒真命题，也不应因为廉价而占据全部搜索。第三类问题是跨行动的预算分配：下一步可以是提出新表达式、寻找反例、增加高精度参考计算，或继续一个尚未完成的证明任务。

为组织上述问题，本文提出一个待研究的成本敏感目标：

$$a_{\mathrm{next}}\in\arg\max_{a\in\mathcal A} \frac{\mathbb E[\Delta U\mid a,\mathcal H]}{\mathbb E[C(a)\mid\mathcal H]}, \qquad \mathbb E[C(a)\mid\mathcal H]>0.$$

其中，$\mathcal H$为已有数据、证书和反例历史，$\mathcal A$为允许的搜索与验证行动，$\Delta U$表示按预先规定标准评价的有用知识增量，$C$为行动成本。这是候选设计原则，不是已证明最优的算法；尤其需要研究知识效用如何衡量、超时这种未完成观测如何建模，以及收益与成本估计错误怎样影响决策。

可信评价应在相同总预算下，与普通文法约束贝叶斯优化、遗传搜索、仅在末端验证的方法及已有反例驱动算法比较。指标应联合考虑独立有效结论数、预定适用域覆盖、验证成本和未知状态校准，而不能只报告拟合误差。还应禁止通过把有效域缩成训练点、向前提直接加入目标结论或生成大量等价表达式来提高“成功率”。若要主张科学突破，最终还需说明发现了什么此前未知且经独立检查的知识。

11.3 近似模型、有效域与误差证书的联合发现

许多化学有效理论的价值，不在于绝对精确，而在于以较低成本保留目标性质。因此，AI发现的对象可以从单独的公式扩展为“简化模型、适用条件、误差界与证据”的组合。Srivastava等对Michaelis–Menten准稳态近似的分析区分了渐近准确性与相对于其他近似的优势性，说明经典模型的有效条件仍可形成新的数学研究[49]。Haasdonk等则已通过严格后验误差估计连接全阶、降阶和机器学习代理模型[50]；因此，为代理模型附加误差估计本身也不能被视为未经探索的创新。

更进一步的研究目标，是同时搜索简化形式与非平凡的有效域，而不是预先固定近似之后只训练误差预测器。给定完整参考模型、参数$\theta$、初态集合$I$及目标可观测量$O$，可以寻找低成本的简化模型，使

$$\underset{\substack{\theta\in D,\ x_0\in I\\t\in[t_0,T]}}{\text{sup}} \left\|O(x_{\mathrm{full}}(t;\theta,x_0)) -O_{\mathrm{red}}(z(t;\theta,x_0))\right\| \leq\varepsilon.$$

这里简化初态的构造、时间区间、范数和参数域均属于命题的一部分；$t_0$允许将初始快速阶段与后续演化分开分析。该式给出的是候选研究规格，不宣称一般体系都能获得这样的全域证书。AI可搜索变量变换、消元方式、候选尺度参数和不等式；分析工具或经过验证的数值程序负责检查相应条件与误差关系。

潜在成果包括扩大已有近似的有效范围、收紧误差界、延长经过控制的时间范围，或者识别此前未被充分描述的失效机制。必须防止通过任意缩小$D$获得平凡保证，应把域覆盖、简化代价和误差作为共同评价目标。还应区分相对于参考方程的近似误差与参考方程对现实的模型差异：有限实验数据不能独自证明未知真实规律上的全域上界，物理适用性仍需独立经验支持。

11.4 最小有效状态、必要记忆与动力学闭合

第10节将信息保留、闭合误差和长期误差分开，进一步引出了一个比预测精度更深的问题：对给定目标、允许误差及时间范围，哪些状态变量或历史信息不可省略？Hernández等提出的数据驱动粒子动力学，把结构保持学习、隐变量与随机动力学结合，用于非平衡体系的粗粒化，并在其建模框架中约束热力学结构[51]。因此，学习隐变量并加入物理约束已有明确先例；更强的目标是说明一个表示何以充分，以及在规定的表示类别中更小的表示何以不足。

作为说明，考虑一阶反应链$A\xrightarrow{k_1}B\xrightarrow{k_2}C$，其部分动力学为

$$\dot A=-k_1A,\qquad \dot B=k_1A-k_2B.$$

两个微观状态可以具有相同的当前$B$而具有不同的$A$，从而产生不同的$\dot B$。因此，对包含这些状态的集合，一般不存在精确的单变量自治方程$\dot B=g(B)$。这是一项由示例方程直接得到的基础事实，并非本文提出的新结果。它表明，预测失败可能来自状态不充分，而不是函数逼近能力不足。

在更一般的模型中，AI可以比较增加状态、保留历史、学习记忆核与引入随机描述等方案。但需要先区分拟合不足、观测噪声和遗漏自由度；仅用更强的时序网络降低测试误差，不能证明已经识别了必要记忆。这里的“最小”必须相对于允许的函数类别、观测方式、初态集合和误差容许量定义，不能通过任意编码把高维信息藏进一个实数后宣称完成降维。

这一方向可分阶段形成成果：在受限问题族中识别必需状态；构造保留目标可观测量的近似闭合；研究状态维数、记忆长度与预测误差之间的关系；进一步建立某类较小表示无法达到目标精度的下界。线性系统和小型非线性反应网络便于核对这些命题，分子动力学则提供更具物理价值但验证更困难的后续场景。序列模型、状态空间模型和记忆核只是候选工具，科学贡献应体现在获得了什么必要信息与有效描述，而不是使用了哪个架构名称。

11.5 面向机制区分的主动实验与理论修订

提高产率或最小化某个预测误差，与识别真实机制并非同一目标。Clarkson等已把贝叶斯实验设计用于符号发现，联合考虑函数形式和连续参数的不确定性[42]。因此，将主动采样接到符号回归之后，并不自动形成新的研究方向。更具理论价值的问题是：在目前允许的测量与干预条件下，两个竞争机制是否可区分；如果可以，怎样以较低代价获得区分证据；如果不可以，需要增加哪类观测或改变何种干预。

第9.3节吸附模型展示了这种区别：稳态关系只能确定参数比值，而动态弛豫提供额外信息。下一步的算法目标可以是自动识别类似的信息缺口，而不是持续增加同类测量。AI负责提出候选机制、搜索实验条件并整理新证据；可识别性分析和形式推导负责判断候选模型的观测等价关系及其逻辑后果。

机制比较必须处理每个模型的参数不确定性与重新拟合空间。仅比较两组固定参数下的最大预测差异，可能夸大可区分性；合理设计需要在给定观测噪声、实验约束和允许参数范围下进行评估。模拟研究可以测试选择策略，却不能单独证明发现了真实化学机制。与实验团队合作时，还应把代价、安全和测量可实现性纳入条件，而不是把不可执行的最优干预当作有效方案。

有意义的突破可以表现为同等预算下排除更多错误机制、获得更稳健的机制置信判断，或者证明现有观测方案不足并提出必要的新观测。实验不一致应允许触发参数、模型结构或适用条件修订，而不是被强行吸收到同一预测器中。这使数据反馈与逻辑反馈真正共同影响理论，而不仅仅共同评价一个固定模型。

11.6 五个方向的比较与协同关系

表3概括上述方向的研究对象和成果标准。它不是对未来成功率的定量预测，也不把这些方向认定为未被研究的空白。与电子结构精度改进相比，前两个方向更直接利用组合对象、形式语言和反例；近似有效域与必要记忆方向关注层次之间的连接；主动实验则把推理边界转化为新的经验问题。

表3 AI可推进的研究问题、代表性基础与实质性成果标准

研究方向	已有基础	值得进一步争取的成果	不足以单独构成突破的结果
网络条件定理	结构理论与图学习[37,46]	新判据、构造定理、边界反例	仅提高同分布分类准确率
验证反馈搜索	BOSS、反例驱动回归、AI Hilbert[22,47–48]	相同总预算下更高的有效知识产出	将验证器简单接到搜索末端
近似与有效域	准稳态分析、认证模型链[49–50]	更宽有效域、更紧界或新失效条件	无法控制的误差预测分数
最小状态与记忆	坐标发现、粗粒化及记忆理论[43–45,51]	充分性证据、必要信息或受限下界	更换时序架构后误差降低
机制区分实验	可识别性与贝叶斯实验设计[42]	更少实验下的机制区分或不可识别性结论	仅在固定参数下最大化分歧

这些方向可以组合，但不宜在初始项目中同时放开所有未知量。先固定动力学类别、目标性质与证据标准，再逐步增加表达能力，更有利于识别算法贡献和科学贡献。尤其应允许一个项目只获得可靠的方法结果，或只得到一个有价值的反例，而不以“自主科学突破”的名称掩盖结果层次。

12 面向可验证科学的研究议程与实施路径

12.1 以条件化知识单元替代孤立预测值

综合前述文献，本文建议将可积累的知识表示为“主张、模型、假设、适用域、经验依据、证明或证书、误差说明及版本依赖”的组合。该提议借鉴可检查证据、可导出发现和不确定性分析，不宣称是一项全新且已实现的通用标准。

一个有效知识单元不仅记录“反应更快”或“结构更稳定”，还应说明比较的是哪一种量、在哪些温压和模型下、依据哪一批数据，以及尚未覆盖哪些误差。当上游模型或背景假设改变时，依赖它的结论应被标记为需要重新审查，而不是继续以脱离来源的事实流通。

这种组织方式也允许证据异质：某个守恒关系有形式证明，某个参数只有置信区间，某条新反应路径仍是待验证假设。知识可以逐步积累，而不必等待所有环节同时获得最强保证。

12.2 建立实验反馈与逻辑反馈的双重修订机制

实验反馈检查经验适用性，逻辑反馈检查推导、规格与模型内部性质。机器学习可以在两者之间提出候选解释、反例区域和实验方案，但应保留反馈来源的区别。实验不一致不能自动定位为某条公理错误，形式证明失败也可能只是验证器能力不足。

一个实用流程因此需要同时允许参数更新、模型结构修改、假设收缩、目标重新形式化和追加实验，而不只是反复训练同一个网络。为避免理论成为封闭过滤器，系统还应保留违反既有假设但具有稳定实验支持的现象，作为可能需要扩展理论的线索，而不是一律当作脏数据删除。

12.3 评价体系必须同时测量“发现什么”和“保证什么”

未来基准不宜只统计预测误差或证明通过率。至少应联合记录经验精度、分布变化下的表现、假设完整性、证据适用域、形式化目标一致性，以及训练、验证和实验的总成本。对于验证任务，还应区分已证明、已反驳和未知，避免把超时隐藏成成功或失败。

更有区分度的任务应包含：可拟合但不可识别的机制、缺少关键反应的候选网络、不一致的背景假设、罕见事件主导的性质，以及一步预测准确但长期闭合失败的模型。目标不是故意制造困难，而是检验系统能否发现自己的证据边界。

12.4 一个集成切口：反应网络条件定理发现

为使五个方向具有可执行的连接，本文建议以“反例与证明反馈驱动的反应网络条件定理发现”作为受控研究切口。这是由综述综合提出的研究设计，不是已完成实验或已经发现的新定理。可先固定质量作用律、某类小型网络和一个目标性质，再选择有限的图条件、参数不等式或网络变换语言，避免同时搜索全部机制、全部物理假设和全部证明系统。

第一阶段检验基础能力：恢复一组已知判据，对人为删去必要条件的命题寻找反例，并要求系统在证据不足时保留未知。第二阶段围绕既有判据的覆盖边界生成候选条件，检查是否取得更广覆盖或更弱前提。第三阶段尝试从有限实例推广到网络族，整理可复用引理，并对候选新结果进行针对性查重和独立证明检查。已有公开网络数据与代码可作为实例来源[46]，但标签的来源和保证层次必须重新审计。

方法目标与科学目标应分别检验。前者是在相同总计算预算下提高有用证书获得效率，基线包括普通文法搜索、BOSS类贝叶斯优化及已有反例驱动方法[47–48]；后者是得到经过独立核查的新判据、一般化定理或关键反例。如果算法没有全面领先但得到重要新定理，仍可能有独立科学价值；如果只有搜索效率改进，则应如实定位为方法贡献，而不是预先承诺突破。

12.5 评价协议、资源预算与证据审计

表4给出与上述设计配套的最低评价要求。这是建议的研究协议，不是现有社区标准。资源统计应覆盖候选生成、参考计算、证明搜索、失败尝试与实验代价，不能只报告模型推理时间。允许使用大模型辅助编码、命题草拟和证明搜索，但必须保留输入、程序、依赖版本与候选修改记录，以定位最终结论究竟依赖什么。

表4 面向可验证发现的评价与审计要求

评价维度	建议记录内容	需要排除的伪提升
科学增量	与已知结果的关系、条件削弱、适用范围、独立核查	将已知结论或等价改写计为新发现
搜索效率	统一预算、有效证书数、总耗时、反例利用与消融	隐藏验证和高精度参考计算成本
证据可靠性	成立、反驳、未知分别记录；证书可复查	把未找到反例或超时当成证明
泛化与覆盖	按结构族隔离；规模、参数和条件外测试	近重复泄漏，缩小有效域换取高通过率
语义及假设	原命题与形式命题对照、公理依赖、量词和版本	漏掉边界条件，将结论写入假设
现实适用性	模型差异、测量噪声、可执行实验及复现	将仿真或内部证明等同实验机制确认

新颖性审查也不能仅依赖模型自评或关键词检索。网络中的新操作可能是既有一般定理的特例；一个短证明可能只是改变了定义；一个更紧误差界也可能以更强假设为代价。应检查结论之间的蕴含关系、覆盖集合与成本差异。在研究资源有限时，优先为高复用、高影响的证据链建立严格检查，而不必把所有辅助软件一次性全部形式化。

研究最终应允许多种诚实的停止结果：得到新结论及证据；得到表明候选不成立的反例；发现现有数据无法识别机制；或者在预算内仍然未知。后三种结果若能够明确界定知识边界，同样可以指导后续工作。面向科学发现的系统应擅长减少无根据的确定性，而不是仅提高肯定回答的比例。

13 结论

数据科学、机器学习、公理化与形式化方法并不是同一层面的替代品。机器学习可以扩大模型、变量、规律和证明的搜索能力；公理化组织研究对象与假设；形式化使指定推导和程序性质可检查；统计推断处理有限数据中的不确定性；实验持续检验模型与现实的对应关系。

现有文献已经显示多种有效结合：把物理结构编码进模型，在符号发现中加入推导约束，让学习器与验证器交换反例，把黑箱预测纳入有效统计推断，以及学习可简化动力学的中间表示。但这些结合的保证对象并不相同，尚不能合并成对真实体系无条件可靠的通用发现器。

本文进一步把研究机会归纳为五类：发现保证反应行为的条件，利用验证反馈改进符号搜索，联合发现近似与有效域，识别必要状态和记忆，以及设计能够区分机制的实验。它们的共同目标不是生成更多看似合理的输出，而是获得条件更明确、证据可审查、边界可定位的新知识。科学发现与方法改进应分别评价，未能在预算内证明的命题应保持未知，内部逻辑正确性也不能代替实验适用性。

对化学而言，最有建设性的目标不是以机器学习取代理论，或把所有经验立即改写为定理，而是逐步建立跨层次、可复用且保留适用条件的知识结构。**第一性原理规定从什么模型出发，有效理论选择在哪个层次描述，学习与算法帮助求解和发现，形式化说明推导为何成立，统计与实验界定我们有多大理由把结论用于现实。**这种分工只有在双向反馈、误差传递和假设审计中连接起来，才可能形成能够累积而非仅能生成的科学知识。

参考文献

[1] Dirac P A M. Quantum mechanics of many-electron systems[J]. Proceedings of the Royal Society A, 1929, 123(792): 714–733. DOI: 10.1098/rspa.1929.0094.

[2] Anderson P W. More Is Different[J]. Science, 1972, 177(4047): 393–396. DOI: 10.1126/science.177.4047.393.

[3] Cornelio C, Ito T, Cory-Wright R, et al. The need for verification in artificial intelligence-driven scientific discovery[J]. Philosophical Transactions of the Royal Society A, 2026, 384(2317): 20240591. DOI: 10.1098/rsta.2024.0591.

[4] Lieb E H, Yngvason J. The physics and mathematics of the second law of thermodynamics[J]. Physics Reports, 1999, 310(1): 1–96. DOI: 10.1016/S0370-1573(98)00082-9.

[5] Hohenberg P, Kohn W. Inhomogeneous Electron Gas[J]. Physical Review, 1964, 136: B864–B871. DOI: 10.1103/PhysRev.136.B864.

[6] Lieb E H, Thirring W E. Bound for the Kinetic Energy of Fermions Which Proves the Stability of Matter[J]. Physical Review Letters, 1975, 35(11): 687–689. DOI: 10.1103/PhysRevLett.35.687.

[7] Hagedorn G A, Joye A. A Time-Dependent Born–Oppenheimer Approximation with Exponentially Small Error Estimates[J]. Communications in Mathematical Physics, 2001, 223: 583–626. DOI: 10.1007/s002200100562.

[8] Schuch N, Verstraete F. Computational complexity of interacting electrons and fundamental limitations of density functional theory[J]. Nature Physics, 2009, 5: 732–735. DOI: 10.1038/nphys1370.

[9] Liu Y K, Christandl M, Verstraete F. Quantum Computational Complexity of the N-Representability Problem: QMA Complete[J]. Physical Review Letters, 2007, 98: 110503. DOI: 10.1103/PhysRevLett.98.110503.

[10] Sutcliffe B T, Woolley R G. On the quantum theory of molecules[J]. The Journal of Chemical Physics, 2012, 137: 22A544. DOI: 10.1063/1.4755287.

[11] Mátyus E. Pre-Born–Oppenheimer molecular structure theory[J]. Molecular Physics, 2019, 117: 590–609. DOI: 10.1080/00268976.2018.1530461.

[12] Behler J, Parrinello M. Generalized Neural-Network Representation of High-Dimensional Potential-Energy Surfaces[J]. Physical Review Letters, 2007, 98: 146401. DOI: 10.1103/PhysRevLett.98.146401.

[13] Batzner S, Musaelian A, Sun L, et al. E(3)-equivariant graph neural networks for data-efficient and accurate interatomic potentials[J]. Nature Communications, 2022, 13: 2453. DOI: 10.1038/s41467-022-29939-5.

[14] Batatia I, Kovács D P, Simm G N C, et al. MACE: Higher Order Equivariant Message Passing Neural Networks for Fast and Accurate Force Fields[C]. Advances in Neural Information Processing Systems, 2022, 35: 11423–11436.

[15] Raissi M, Perdikaris P, Karniadakis G E. Physics-informed neural networks: A deep learning framework for solving forward and inverse problems involving nonlinear partial differential equations[J]. Journal of Computational Physics, 2019, 378: 686–707. DOI: 10.1016/j.jcp.2018.10.045.

[16] Krishnapriyan A S, Gholami A, Zhe S, et al. Characterizing possible failure modes in physics-informed neural networks[C]. Advances in Neural Information Processing Systems, 2021, 34.

[17] Mishra S, Molinaro R. Estimates on the generalization error of physics-informed neural networks for approximating PDEs[J]. IMA Journal of Numerical Analysis, 2023, 43(1): 1–43. DOI: 10.1093/imanum/drab093.

[18] Pfau D, Axelrod S, Sutterud H, et al. Accurate computation of quantum excited states with neural networks[J]. Science, 2024, 385(6711): eadn0137. DOI: 10.1126/science.adn0137.

[19] Brunton S L, Proctor J L, Kutz J N. Discovering governing equations from data by sparse identification of nonlinear dynamical systems[J]. Proceedings of the National Academy of Sciences, 2016, 113(15): 3932–3937. DOI: 10.1073/pnas.1517384113.

[20] Udrescu S M, Tegmark M. AI Feynman: A physics-inspired method for symbolic regression[J]. Science Advances, 2020, 6(16): eaay2631. DOI: 10.1126/sciadv.aay2631.

[21] Cornelio C, Dash S, Austel V, et al. Combining data and theory for derivable scientific discovery with AI-Descartes[J]. Nature Communications, 2023, 14: 1777. DOI: 10.1038/s41467-023-37236-y.

[22] Cory-Wright R, Cornelio C, Dash S, et al. Evolving scientific discovery by unifying data and background knowledge with AI Hilbert[J]. Nature Communications, 2024, 15: 5922. DOI: 10.1038/s41467-024-50074-w.

[23] Peters J, Bühlmann P, Meinshausen N. Causal inference by using invariant prediction: identification and confidence intervals[J]. Journal of the Royal Statistical Society: Series B, 2016, 78(5): 947–1012. DOI: 10.1111/rssb.12167.

[24] Necula G C. Proof-carrying code[C]. Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1997, 106–119. DOI: 10.1145/263699.263712.

[25] Solar-Lezama A, Tancau L, Bodík R, et al. Combinatorial sketching for finite programs[C]. Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems, 2006, 404–415. DOI: 10.1145/1168857.1168907.

[26] Katz G, Barrett C, Dill D L, et al. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks[C]. Computer Aided Verification. Lecture Notes in Computer Science, 2017, 10426: 97–117. DOI: 10.1007/978-3-319-63387-9_5.

[27] Chang Y C, Roohi N, Gao S. Neural Lyapunov Control[C]. Advances in Neural Information Processing Systems, 2019, 32.

[28] de Moura L, Ullrich S. The Lean 4 Theorem Prover and Programming Language[C]. Automated Deduction – CADE 28. Lecture Notes in Computer Science, 2021, 12699: 625–635. DOI: 10.1007/978-3-030-79876-5_37.

[29] Hubert T, Mehta R, Sartran L, et al. Olympiad-level formal mathematical reasoning with reinforcement learning[J]. Nature, 2026, 651: 607–613. DOI: 10.1038/s41586-025-09833-y.

[30] Lean Documentation Contributors. Axioms[EB/OL]. The Lean Language Reference. 访问日期：2026-10-09. 官方文档路径：lean-lang.org/doc/reference/latest/Axioms/.

[31] Immler F. A Verified ODE Solver and the Lorenz Attractor[J]. Journal of Automated Reasoning, 2018, 61: 73–111. DOI: 10.1007/s10817-017-9448-y.

[32] Lei J, G’Sell M, Rinaldo A, et al. Distribution-Free Predictive Inference for Regression[J]. Journal of the American Statistical Association, 2018, 113(523): 1094–1111. DOI: 10.1080/01621459.2017.1307116.

[33] Barber R F, Candès E J, Ramdas A, et al. The limits of distribution-free conditional predictive inference[J]. Information and Inference: A Journal of the IMA, 2021, 10(2): 455–482. DOI: 10.1093/imaiai/iaaa017.

[34] Barber R F, Candès E J, Ramdas A, et al. Conformal prediction beyond exchangeability[J]. The Annals of Statistics, 2023, 51(2): 816–845. DOI: 10.1214/23-AOS2276.

[35] Angelopoulos A N, Bates S, Fannjiang C, et al. Prediction-powered inference[J]. Science, 2023, 382(6671): 669–674. DOI: 10.1126/science.adi6000.

[36] Kennedy M C, O’Hagan A. Bayesian Calibration of Computer Models[J]. Journal of the Royal Statistical Society: Series B, 2001, 63(3): 425–464. DOI: 10.1111/1467-9868.00294.

[37] Feinberg M. Chemical reaction network structure and the stability of complex isothermal reactors—I. The deficiency zero and deficiency one theorems[J]. Chemical Engineering Science, 1987, 42(10): 2229–2268. DOI: 10.1016/0009-2509(87)80099-4.

[38] Wang L P, Titov A, McGibbon R, et al. Discovering chemistry with an ab initio nanoreactor[J]. Nature Chemistry, 2014, 6: 1044–1048. DOI: 10.1038/nchem.2099.

[39] Unsleber J P, Grimmel S A, Reiher M. Chemoton 2.0: Autonomous Exploration of Chemical Reaction Networks[J]. Journal of Chemical Theory and Computation, 2022, 18(9): 5393–5409. DOI: 10.1021/acs.jctc.2c00193.

[40] Proppe J, Reiher M. Mechanism Deduction from Noisy Chemical Reaction Networks[J]. Journal of Chemical Theory and Computation, 2019, 15: 357–370. DOI: 10.1021/acs.jctc.8b00310.

[41] Langmuir I. The adsorption of gases on plane surfaces of glass, mica and platinum[J]. Journal of the American Chemical Society, 1918, 40(9): 1361–1403. DOI: 10.1021/ja02242a004.

[42] Clarkson K L, Cornelio C, Dash S, et al. Bayesian Experimental Design for Symbolic Discovery[C]. Recent Developments in Industrial and Applied Mathematics. ICIAM2023 Springer Series, 2026, 1: 139–148. DOI: 10.1007/978-981-95-1446-5_7.

[43] Champion K, Lusch B, Kutz J N, et al. Data-driven discovery of coordinates and governing equations[J]. Proceedings of the National Academy of Sciences, 2019, 116(45): 22445–22451. DOI: 10.1073/pnas.1906995116.

[44] Wang W, Gómez-Bombarelli R. Coarse-graining auto-encoders for molecular dynamics[J]. npj Computational Materials, 2019, 5: 125. DOI: 10.1038/s41524-019-0261-5.

[45] Mori H. Transport, Collective Motion, and Brownian Motion[J]. Progress of Theoretical Physics, 1965, 33(3): 423–455. DOI: 10.1143/PTP.33.423.

[46] Yao S, Sadeghimanesh A, England M. Understanding Multistationarity of Fully Open Reaction Networks[J]. Bulletin of Mathematical Biology, 2025, 87: 176. DOI: 10.1007/s11538-025-01537-8.

[47] Moss H B, Beck D, González J, et al. BOSS: Bayesian Optimization over String Spaces[C]. Advances in Neural Information Processing Systems, 2020, 33: 15476–15486. arXiv: 2010.00979.

[48] Błądek I, Krawiec K. Counterexample-Driven Genetic Programming for Symbolic Regression With Formal Constraints[J]. IEEE Transactions on Evolutionary Computation, 2023, 27(5): 1327–1339. DOI: 10.1109/TEVC.2022.3205286.

[49] Srivastava K, Eilertsen J, Booth V, et al. Accuracy Versus Predominance: Reassessing the Validity of the Quasi-Steady-State Approximation[J]. Bulletin of Mathematical Biology, 2025, 87: 73. DOI: 10.1007/s11538-025-01451-z.

[50] Haasdonk B, Kleikamp H, Ohlberger M, et al. A New Certified Hierarchical and Adaptive RB-ML-ROM Surrogate Model for Parametrized PDEs[J]. SIAM Journal on Scientific Computing, 2023, 45(3): A1039–A1065. DOI: 10.1137/22M1493318.

[51] Hernández Q, Win M, O’Connor T C, et al. Data-driven particle dynamics: Structure-preserving coarse-graining for emergent behavior in nonequilibrium systems[J]. Proceedings of the National Academy of Sciences, 2026, 123(20): e2519631123. DOI: 10.1073/pnas.2519631123.