Source-linked AI summary
FARMS: A Verifiable Foundation for Automated Computational Science
Di Wu, Ling Liang, Haizhao Yang
TL;DR
Automated computational science needs mathematical knowledge that AI can interpret and reuse with explicit guarantees. FARMS connects formal statements to source context and computational meaning through preparation, reusable representations, and semantic review. Across 171 targets, 157 were accepted, with reported low per-target costs and demonstrations in heat flow and wave-response compression.
Problem
Automated computational science needs mathematical knowledge that AI can interpret and reuse while preserving the conditions supporting computational decisions.
Source: §1 · p. 1Method
FARMS connects formal statements to source context and computational interpretation through source preparation, reusable representations, semantic review, and Lean-checked implications.
Source: §1 · p. 2Results
157 of 171 targets were accepted, with mean estimated costs of US $0.85–2.29 per target across sources, and demonstrations covered heat flow and wave-response compression.
Source: §1 · pp. 2–3Takeaways & Limitations
FARMS links methods to applicability conditions, quantitative guarantees, and source evidence, supporting parameter selection, accuracy assessment, and reuse of numerical results.
Source: §3 · p. 11The evaluated collection covers four sources in two areas, and broader applications will require additional mathematical representations and application-specific checks.
Source: §3 · p. 11
Abstract
from arXiv · showhide
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.
1 Introduction
Automated computational science needs mathematical knowledge that AI can interpret and reuse while preserving the conditions behind computational guarantees. FARMS connects formal statements to source context and computational meaning, and demonstrates checked links to numerical applications.
1 Introduction
- Randomized linear algebra supports large-scale computation through sampling, sketching, and low-rank approximation, while numerical PDEs connect physical models to simulations through discretization, stability, and error analysis.Sketching can produce preconditioners for large systems, and low-rank representations can compress simulation responses for repeated use.Source: §1 · pp. 1–2
- An AI-ready representation must preserve the source conditions that connect a method to its guarantee, including sampling choices, constructible outputs, and success measures.PDE estimates can likewise depend on boundary conditions, regularity, and a particular error norm.Source: §1 · p. 2
- Formal mathematics offers machine-checked representations, but computational science also needs algorithmic operations, quantitative guarantees, and dependencies that support scientific workflows.The introduction frames this need against prior work on formalization and semantic correctness.Source: §1 · p. 2
- FARMS prepares source evidence, uses reusable domain representations, and applies compilation, semantic review, and bounded repair to create AI-ready computing knowledge.Selected statements can be combined through Lean-checked implications into computational skills with explicit applicability conditions.Source: §1 · p. 2
- 157 of 171 targets were accepted, with mean estimated costs of US $0.85–2.29 per target across sources.The demonstrations include a steady heat-flow solve and compression of wave-response libraries.Source: §1 · pp. 2–3
2 Results
FARMS links formal statements to source evidence and computational meaning, then uses semantic review to assess whether they preserve the source. Across numerical applications and 171 formalization targets, it demonstrates reusable, accuracy-bounded skills and efficient knowledge construction.
2.1 Building AI-ready computing knowledge
- FARMS links each formal statement to source context and computational interpretation, with explicit objects, applicability conditions and guarantees.Preparation assembles supporting definitions, assumptions and algorithm descriptions; formalization uses this evidence and a reusable domain library, followed by compilation and semantic review.Source: §2.1 · p. 3
2.2 Preserving computational meaning
- In the low-rank approximation example, semantic review restored omitted rank and logarithm-domain restrictions; a separate matrix-multiplication claim remained unaccepted after a counterexample exposed a missing source condition.FARMS records the latter issue as a source warning rather than silently changing the source claim.Source: §2.2 · pp. 5–7
2.3 From faithful statements to scientific computing
- Lean-checked implications connect selected statements to skills used for heat-flow solving and wave-response compression, with guarantees guiding accuracy decisions.The heat-flow runs met a 10^-6 relative discrete energy-error target; wave-response compression met a 0.01 energy-norm error target under the stated assumptions.Source: §2.3 · pp. 7, 9
2.4 Quantitative results
- 157 of 171 targets were accepted, and mean estimated costs ranged from $0.85 to $2.29 per planned target across four sources.The accepted set includes 154 formalizations without source warnings and three with documented warnings.Source: §2.4 · p. 9
- FARMS treats algorithmic success as requiring both an output constructed by the prescribed algorithm and the requested error bound.In the low-rank example, the compared statement-level AutoformBot formalization retained the error condition but did not require the output to exist.Source: §2.4 · pp. 10–11
3 Discussion
FARMS links mathematical claims to source evidence, applicability conditions, and quantitative guarantees so they can inform computational decisions. The discussion identifies limits in the current collection and outlines directions for extending its coverage and connecting it to scientific agents.
Discussion
- The heat-flow and wave-response examples connect source-linked mathematical knowledge to parameter selection, accuracy assessment, and reuse of numerical results.The evaluated collection also had low per-target costs.Source: §3 · p. 11
- The collection covers four sources in two areas; broader problems will require additional mathematical representations and application-specific checks.Missing context, ambiguous formulations, generation, and semantic review remain obstacles.Source: §3 · p. 11
Future directions
- Integrating textbook knowledge would link equivalent results across sources while preserving differences in assumptions and guarantees.The discussion notes that source-specific notation or generality can leave equivalent results represented multiple times.Source: §3 · p. 11
- Adapting to varied exposition requires improving extraction and retrieval while keeping source claims distinct from repaired claims.Some sources present computational results in prose, derivations, or algorithm descriptions rather than separate theorems.Source: §3 · p. 12
- Adding research articles could expose newer methods and guarantees, with retrieved material still requiring source auditing, formal representation, and review.Source: §3 · p. 12
- Connecting the evolving knowledge base to agents is a longer-term opportunity; constructing new connections and discovering methods remain open research tasks.A community-built collection could make accumulated mathematical knowledge more accessible for trustworthy automated scientific discovery.Source: §3 · p. 12
4 Methods
FARMS evaluates formalization across four sources in randomized numerical linear algebra and numerical PDEs, then connects selected source propositions to executable computational skills. Its heat-flow and wave-response applications show how those skills support verified accuracy decisions and reusable numerical results.
4.1 Source collection
- The 171 targets comprised 32 from Drineas–Mahoney, 35 from Halko–Martinsson–Tropp, 20 from Martinsson–Tropp, and 84 theorems and lemmas from Larsson–Thomée.Source: §4.1 · p. 12
4.2 FARMS workflow
- FARMS packages source statements with definitions, assumptions, and algorithm descriptions, then uses retrieval, reusable representations, compilation, semantic review, and bounded repair to assess formalizations.Acceptance is a final outcome of either “VERIFIED PASS” or “COMPILED WITH SOURCE WARNING”.Source: §4.2 · pp. 12–13
4.3 Models and execution environments
- The principal configuration used Claude through Claude Code, with high effort for most review and formalization roles and medium effort for retrieval planning and explanation.The Retriever also used deterministic document searches, while Lean invoked the compiler directly.Source: §4.3 · p. 13, §4.2 · p. 13
4.4 Connecting formal statements to computational skills
- Selected source propositions remain explicit premises in Lean-checked implications that connect them to task-specific guarantees and executable numerical procedures.The reported connecting proofs excluded “sorryAx” and used only standard logical axioms.Source: §4.4 · pp. 13–14
4.4.1 Steady heat-flow application
- Gaussian preconditioning gave condition numbers of 8.83–8.95 across two conductivity contrasts, versus 99.6 and 964.0 for the diagonal preconditioner.The sketch used 2,048 rows to compress gradient data from 8,192 rows, under the stated source and ideal Gaussian sampling assumptions.Source: §4.4.1 · p. 14
4.4.2 Wave-response compression application
- All three wave-response seeds selected 128 basis directions, with checked Frobenius residuals of approximately 0.00877–0.00938, reducing float64 storage from 24 to 8.375 MiB.The error bound applies to every allowed excitation combination throughout wave evolution.Source: §4.4.2 · pp. 14–15
4.5 Statement-level AutoformBot comparison and resource accounting
- The statement-level AutoformBot adaptation was compared on selected randomized numerical linear algebra targets, with mean resources including planned targets that were not accepted.The comparison retained AutoformBot’s native workflow and supplied the same complete source documents.Source: §4.5 · p. 15