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
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−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.
Progress in computational science depends on complex numerical workflows that must faithfully encode physical laws, yet translating conceptual insight into reliable code remains a major bottleneck. Although large language models can generate isolated code fragments, they lack the structured reasoning required to design, verify, and iteratively refine complete scientific pipelines. Here we introduce ATHENA, an agentic framework explicitly designed to emulate scientific research modeled as a knowledge-driven contextual bandit process. Its core loop separates conceptual policy from numerical realization through expert-derived conceptual scaffolding, enabling principled diagnosis, reformulation, and repair of computational strategies. Across scientific computing and scientific machine learning tasks, ATHENA autonomously derives and correctly applies exact analytical solutions, constructs stable numerical solvers, diagnoses ill-posed formulations, and orchestrates hybrid symbolic-numeric workflows. Quantitatively, ATHENA matches and frequently surpasses the accuracy of expert-authored reference solutions reported in the literature on canonical benchmarks. By reframing computation as an object of agentic reasoning, our framework enables autonomous orchestration of heterogeneous algorithms across scientific domains.
Juan Diego Toscano, Daniel T. Chen, George Em Karniadakis
Division of Applied Mathematics, Brown University, Providence, 02912, RI, USA
Recent advances in Large Language Models have fueled autonomous AI agents capable of tackling complex scientific tasks, yet existing automated research systems remain predominantly focused on empirically driven domains with quantitative benchmarks, leaving theory-driven discovery, particularly in mathematically grounded disciplines requiring rigorous proofs and synthesis of domain knowledge, largely underexplored. Key challenges include the difficulty of verifying theoretical reasoning at scale, insufficient reasoning ability for autonomous frontier exploration, and a scarcity of procedural heuristics in the literature. We introduce ReasFlow, an end-to-end autonomous agent system for reasoning-centric scientific discovery that operationalizes a collaborative paradigm where the human expert acts as Principal Investigator while the agent executes rigorous derivations as a capable graduate student. ReasFlow incorporates (i) a robust internal verification loop that audits logical coherence and corrects fundamental errors prior to human inspection, and (ii) an automated knowledge retrieval and self-improvement mechanism that proactively surfaces both declarative facts and overlooked procedural heuristics, substantially reducing expert intervention. The system unifies literature synthesis, algorithm design, theorem proving, experimentation, and manuscript preparation in a single system. Deployed to autonomously generate five complete research papers with rigorous theoretical and empirical content from minimal prompts, ReasFlow consistently achieves the highest evaluation scores among state-of-the-art open-access baselines under a curated LLM-based review rubric. ReasFlow is publicly accessible via the ReasLab platform, providing a collaborative workspace for AI-assisted theoretical research. Github repo: https://github.com/ReasLab/ReasFlow.git.
Yutong He, Daibo Li, Guohong Li +15
Peking University · University of Electronic Science and Technology of China · Beijing Normal University +2
Recent advances in large language models and agentic AI systems have enabled significant progress in mathematical discovery, from solving competition problems to tackling research-level conjectures. However, open problems in computational mathematics have received comparatively less attention: research in this area often requires not only proofs but also numerical experimentation, adversarial constructions, and algorithm design. In this paper, we introduce an agentic research system, Iteris, designed for open problems in computational mathematics. We apply Iteris to two open problems from a recent Simons Workshop collection (arXiv:2602.05394). In these case studies, Iteris generated numerical evidence, constructions, and proof drafts that led, after expert review and correction, to verified results. The first result is a phase diagram for the asymptotic comparison between conjugate gradient and randomized coordinate descent on power-law spectra; the second is a counterexample showing that QR factorization with column pivoting can fail to select well-conditioned submatrices even under low coherence. These case studies suggest that agentic AI systems can participate meaningfully in research workflows for open problems in computational mathematics, while human validation remains essential.
Leheng Chen, Zihao Liu, Wanyi He +1
School of Mathematical Sciences, Peking University · 5Zhongguancun Academy · 2Beijing International Center for Mathematical Research and the New Cornerstone Science Laboratory, Peking University +2