FARMS：自动化计算科学的可验证基础

自动化计算科学能够通过选择、调整和开发数值方法来加速发现。这一前景需要人工智能系统能够解读并复用的数学知识，并且具备明确的保证。在此，我们提出 FARMS，这是一种忠实且高效的基础，能够将计算数学转化为适用于人工智能的计算知识。FARMS 通过来源准备、可复用表示和语义审查，将形式化陈述与来源上下文、算法含义及定量保证连接起来。在随机数值线性代数和数值偏微分方程领域的 171 个目标条目中，有 157 个被该流程接受；在不同来源中，每个目标条目的平均估算成本为 0.85–2.29 美元。由 Lean 检查的、基于明确来源前提的蕴含关系，将选定的陈述与计算技能连接起来，并通过热流求解和波响应压缩加以说明。因此，FARMS 为可信的自动化计算科学提供了经济实惠且可复用的知识基础。