cs.AIOct 29, 2026

FARMS: A Verifiable Foundation for Automated Computational Science

Authors: Di Wu, Ling Liang, Haizhao Yang

Organizations: Department of Mathematics, University of Maryland, College Park, USA · Department of Mathematics, The University of Tennessee, Knoxville, USA · Department of Computer Science, University of Maryland, College Park, USA

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

Abstract

Automated computational science could accelerate discovery by selecting, adapting and developing numerical methods. This prospect requires mathematical knowledge that AI systems can interpret and reuse with explicit guarantees. Here we present FARMS, a faithful and efficient foundation that transforms computational mathematics into AI-ready computing knowledge. FARMS connects formal statements to source context, algorithmic meaning and quantitative guarantees through source preparation, reusable representations and semantic review. Across 171 targets in randomized numerical linear algebra and numerical partial differential equations, 157 were accepted by the pipeline, with mean estimated costs of US $0.85-2.29 per target across sources. Lean-checked implications from explicit source premises connect selected statements to computational skills, illustrated by a heat-flow solve and wave-response compression. FARMS therefore supports an affordable, reusable knowledge foundation for trustworthy automated computational science.

Figures & tables

Figure 1: FARMS builds AI-ready computing knowledge for automated computational science. a , Source preparation links mathematical statements to supporting definitions, assumptions and algorithm descriptions. Formalization combines this evidence with reusable domain representations, followed by compilation, semantic review and bounded repair. Dashed paths show source re-auditing, repair and rechecking, resolution of review disagreement, and justified abstention. b , The collection comprises 171 targets, shown by domain (inner ring), source (middle) and statement type (outer): 87 from randomized numerical linear algebra and 84 from numerical PDEs. c , Computational structures represented in the collection, including algorithmic constructions and quantitative guarantees.
Figure 2: FARMS refines formalization results and identifies defects in textbook claims. a, Agent interaction during the formalization of a randomized low-rank approximation guarantee. Although the initial candidate compiles, the Semantic referee identifies omitted rank and logarithm-domain restrictions that change the intended claim. Using evidence from the textbook context, the Formalizer restores these conditions. Subsequent compilation and semantic review confirm the refinement, yielding an accepted formal statement. b, Agent interaction during the examination of the sampling optimality claim in randomized matrix multiplication guarantee. The candidate preserves the probability domain stated in the textbook and passes compilation. The Semantic referee nevertheless constructs a counterexample, and calls an independent source review to confirm a missing condition requiring positive sampling probability for every nonzero contribution, and this finding is kept as an explicit source warning. Together, the examples illustrate how FARMS uses source evidence and mathematical evaluation to distinguish repairable formalization errors from defects in the underlying claims.
Figure 3: From faithful formal statements to numerical agent skills. a, Formal statements and connecting proofs form reusable skills that contain applicability conditions and link results to supporting evidence. b, Gaussian bounds and Lax–Milgram support an energy comparison that controls solve accuracy; wave energy conservation and a matrix residual bound support response compression. c, Representative applications of the skills. Left, a Gaussian sketch assists the steady heat-flow solve. All six runs meet the 10−610^{-6} relative discrete energy-norm target in a small number of updates. Right, 128 basis responses support wave predictions for 384 prescribed initial disturbances. The response library shrinks from 24 to 8.375 MiB while meeting the 0.01 energy-norm error target. The skills support accurate PDE solving and reusable response models with checkable error bounds.
Figure 4: Knowledge-construction acceptance, resource use and algorithmic semantics. a, Cumulative selected outcomes for 171 targets; the 157 reported acceptances include three source-warning results (hatched). b, Mean cost and tokens per planned target, including source preparation, generation, review, repair and continuations within each selected logical run. Source and selected-set plots use separate scales. The six-target comparison uses our statement-level adaptation of AutoformBot. c, Randomized low-rank matrix approximation illustrates FARMS’s computing-oriented design. The table contrasts output-existence and accuracy conditions in the two formal statements for the same sample.
More in this topic

AI for Science

AI for Science applies machine learning and AI agents to scientific data, models, experiments, and discovery workflows.

See all 161 papers

Explore similar work

CardsList

  1. ATHENA: Agentic Team for Hierarchical Evolutionary Numerical Algorithms

    Dec 3, 2025Juan Diego Toscano, Daniel T. Chen, George Em KarniadakisScientific Code GenerationScientific ML

    Division of Applied Mathematics, Brown University, Providence, 02912, RI, USA

  2. ReasFlow: Assisting Reasoning-Centric Scientific Discovery in Applied Mathematics via a Knowledge-Based Multi-Agent System

    Jul 15, 2026Yutong He, Daibo Li, Guohong Li +15Multi-Agent LLM SystemsAI Agents for Scientific Discovery

    Peking University · University of Electronic Science and Technology of China · Beijing Normal University +2

  3. Iteris: Agentic Research Loops for Computational Mathematics

    Jun 1, 2026Leheng Chen, Zihao Liu, Wanyi He +1Mathematical ReasoningLarge Language Model-Guided Scientific Discovery

    School of Mathematical Sciences, Peking University · 5Zhongguancun Academy · 2Beijing International Center for Mathematical Research and the New Cornerstone Science Laboratory, Peking University +2