知识卡片：FARMS——面向自动化计算科学的可验证基础

一句话结论

FARMS 提出一套“忠实且高效”的基础设施，把计算数学文献转化为 AI 可解释、可复用且带显式保证的计算知识，并在随机数值线性代数与数值偏微分方程共 171 个目标上实现 157 个被流水线接受，单目标平均估计成本为 0.85–2.29 美元。

事件概述或研究问题

自动化计算科学有望通过选择、适配与开发数值方法来加速科学发现，但其前提是 AI 系统能够理解并复用带有显式保证的数学知识。论文提出的核心问题是：如何将计算数学转化为“AI-ready”的计算知识，并使形式化陈述与来源语境、算法含义、定量保证相互连接。

方法/产品要点

FARMS 通过三个环节构建这一基础：

• 来源准备（source preparation）：处理原始文献来源；
• 可复用表示（reusable representations）：把数学内容组织为可复用的形式；
• 语义审查（semantic review）：对语义层面进行审核。

其目标是把形式化陈述与来源语境、算法含义和定量保证连接起来，并以 Lean 检查由显式来源前提推出的蕴含关系，从而把选定的陈述与计算技能关联。

主要结果或产业意义

• 在随机数值线性代数与数值偏微分方程两个方向的 171 个目标中，157 个被流水线接受。
• 跨来源的单目标平均估计成本为 0.85–2.29 美元。
• 经 Lean 检查的蕴含关系（由显式来源前提推出）把选定陈述连接到计算技能，论文以**热流求解（heat-flow solve）和波响应压缩（wave-response compression）**作为示例说明。
• 作者据此认为 FARMS 为可信的自动化计算科学提供了可负担、可复用的知识基础。

为什么重要

该工作针对的是自动化计算科学中的一个关键瓶颈：AI 不仅需要“读到”数值方法，还需要以可验证的方式理解其前提与保证。FARMS 将形式化陈述、来源语境与定量保证绑定，并通过 Lean 检查建立陈述与计算技能之间的蕴含链，这为“可信”的自动化数值方法选择与开发提供了可审计的知识底座；同时其给出的单目标成本区间，也为这类知识基础设施的规模化可行性提供了初步的经济性参考。

局限与不确定性

• 材料仅覆盖随机数值线性代数与数值偏微分方程两类目标，其他计算数学领域的适用性待核实。
• “平均估计成本”的估算口径、来源构成与可复现细节，材料未展开，待核实。
• 157/171 被接受，其余 14 个目标未被接受的原因与失败模式，材料未说明，待核实。
• Lean 检查覆盖的范围（是全部选定陈述还是部分示例）在材料中表述有限，待核实。
• 论文为 arXiv 预印本（2610.40560v1，2026-10-29），是否经同行评审待核实。

可用于图书/PPT/简报的角度

• 作为“AI for Science 从模型能力走向知识基础设施”的案例：强调可验证性与来源可追溯，而非单纯模型规模。
• 用“形式化陈述—来源语境—算法含义—定量保证”四要素图，说明计算数学知识如何被结构化。
• 以 171→157 的接受率与 0.85–2.29 美元/目标的成本，讨论知识工程建设的经济性与流水线化。
• 以热流求解与波响应压缩两个示例，说明“形式化蕴含→计算技能”的落地链路。
• 与“AI4CDS”类框架对照：前者侧重方法论与责任划分，本条侧重可验证知识底座，可作为互补素材。

与既有脉络的关系

既有卡片多聚焦于数据语料与多模态框架（如 RMISC 的时间序列语料、MedPMC 的医学图文数据系统）或计算设计科学的方法论框架（AI4CDS）。本条增量在于：把“基础”从数据层推进到可验证的数学知识层，引入 Lean 检查与来源前提的显式蕴含，并给出流水线接受率与成本量级，属于面向自动化计算科学的“知识基础设施”方向，与上述数据/框架类工作不重复。

原始材料

• Title: FARMS: A Verifiable Foundation for Automated Computational Science
• Authors: Di Wu, Ling Liang, Haizhao Yang
• arXiv ID: 2610.40560v1（Primary: cs.AI; Categories: cs.AI, cs.LO）
• Published/Updated: 2026-10-29T17:40:57Z
• Abstract URL: https://arxiv.org/abs/2610.40560v1
• PDF URL: https://arxiv.org/pdf/2610.40560v1