提出FARMS可验证框架用于自动化计算科学
原文：FARMS: A Verifiable Foundation for Automated Computational Science
自动化计算科学有望通过选择、调整和开发数值方法来加速发现。这一前景需要AI系统能够以明确保证进行解释和复用的数学知识。在此我们提出FARMS，一个将计算数学转化为AI就绪计算知识的忠实且高效的基础。FARMS通过源准备、可复用表示和语义审查，将形式化陈述与源上下文、算法含义和定量保证相连接。在随机数值线性代数和数值偏微分方程的171个目标中，157个被流程接受，各来源每目标平均估计成本为0.85-2.29美元。经Lean检查的从显式源前提推导出的蕴含关系将选定陈述与计算技能相连接，并以热流求解和波响应压缩为例说明。因此，FARMS为可信的自动化计算科学提供了一个经济实惠、可复用的知识基础。作者：Di Wu, Ling Liang, Haizhao Yang 分类：cs.AI,cs.LO