Farms builds a trustworthy knowledge base for automated computing science
FARMS: A Verifiable Foundation for Automated Computational Science
Artificial IntelligenceLogic in Computer Science
Summary
Scientists want to use AI to help pick and improve math methods for computers to solve scientific problems faster. The authors created a tool called FARMS that turns complex math statements into a form AI can understand and trust, linking these statements back to their original sources and proofs. FARMS was tested on many math problems related to linear algebra and differential equations, and it successfully verified most of them efficiently and cheaply. This helps make automated problem-solving in science more reliable and easier to reuse. The authors show examples where their system connects math knowledge with real computational tasks like heat flow and wave response.
What this means in practice
- •For software engineers in scientific computing: Verify and reuse mathematical foundations in scientific computing software to improve reliability and debugging.
- •For simulation software developers: Integrate automatically verified numerical algorithms into simulation tools to ensure correctness and establish quantitative guarantees.
- •For automated ai tooling teams: Create AI systems for automated discovery that safely select and adapt numerical methods with formal proof links.$Commercial implications: Enables commercial AI platforms to offer provably correct computational method selection for scientific software, increasing trust and efficacy.
Authors
Di Wu, Ling Liang, Haizhao Yang
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.