Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance

• URL: http://arxiv.org/abs/2606.14000v1
• Date: Fri, 12 Jun 2026 00:45:42 GMT
• Title: Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance
• Abstract summary: coding agents can formalize entire advanced mathematics textbooks in Lean 4.<n>We introduce a framework for evaluating the quality of agent-produced formalizations beyond compilation.<n>Our results suggest that compilation-based metrics substantially overstate formalization quality.
• Score: 0.3624700141426058
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Recent work has demonstrated that coding agents can formalize entire advanced mathematics textbooks in Lean 4, yet existing efforts concentrate on branches of mathematics already well-represented in mathlib and measure success solely through kernel acceptance. We address both limitations by applying a coding agent to formalize Numerical Methods for Ordinary Differential Equations, a textbook in numerical analysis that is largely absent from mathlib, stressing the agent's capacity to develop new theory from scratch. We further introduce a systematic, reproducible three-dimensional framework for evaluating the quality of agent-produced formalizations beyond compilation: semantic correctness, Mathlib reuse, and cross-file reuse via LLM-as-judge methods. Applying this framework to our own formalization and to the released outputs of RepoProver and M2F, we uncover recurring unfaithful formalization patterns, including incomplete multi-part statements, added weakening hypotheses, and parameter restrictions, that kernel acceptance entirely obscures. Our results suggest that compilation-based metrics substantially overstate formalization quality, and we provide a reproducible audit methodology to support more rigorous evaluation of future autoformalization systems.

Related papers

• From Atomic to Agentic: Towards Interpretable Evaluation of LLMs' Agentic Mathematical Capabilities [103.60384544335072]
  Large Language Models (LLMs) are evolving from performing end-to-end mathematical reasoning to integrating agentic intelligence.<n>Our framework aligns problem-solving agentic behaviors with a structured taxonomy of reusable mathematical atomic capabilities.<n> Experiments reveal that models with similar end-to-end accuracy can exhibit markedly different agentic capability profiles.
  arXiv  Detail & Related papers  (2026-08-27T10:52:06Z)
• MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement [28.062085562858098]
  We introduce MathForm, an autoformalization framework for constructing verified training data.<n>We construct FormalVerse, a Lean 4 dataset containing approximately 367K verified examples.<n>MathForm-8B achieves average Pass@8 rates of 88.06% under Syntax Check and 72.37% under Consistency Check.
  arXiv  Detail & Related papers  (2026-08-14T11:51:12Z)
• MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research [62.221184989046826]
  MathCoPilot is a human-in-the-loop system that embodies a new human--AI symbiotic paradigm for mathematical research.<n>MathCoPilot unifies three core capabilities: an interactive proof blueprint that decomposes a proof into navigable steps the human can directly inspect, direct, and refine; automated proving skill orchestration with adaptive knowledge base search and Lean-integrated iterative verification; and topic-driven paper retrieval and automated formalization into a verified Lean knowledge base.
  arXiv  Detail & Related papers  (2026-07-16T05:22:40Z)
• Multi-agent Autoformalization of Tensor Network Theory [0.21847754147782886]
  We build a team of specialized large language-model agents and present an agent-driven workflow for research-level formalization in theoretical physics.<n>The agents coordinated through a structured mathematical blueprint and periodic human review, orchestrated and executed the full formalization autonomously.<n>For some statements, the agents were able to explore new proof routes that are not part of the standard literature.
  arXiv  Detail & Related papers  (2026-07-08T18:43:33Z)
• Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics [20.90238876313568]
  Large Language Models (LLMs) produce subtle errors that evade human detection.<n>Recent trends indicate that general-purpose LLMs now outperform smaller models explicitly fine-tuned for Lean.<n>We introduce an agentic autoformalization framework powered by general coding LLMs.
  arXiv  Detail & Related papers  (2026-06-30T05:05:03Z)
• Lean-GAP: A Dataset of Formalized Graduate Algebra Problems [3.1963549333419388]
  We develop a scalable pipeline consisting of PDF-to-La Algebra preprocessing, autoformalization into Lean 4, and verification of informal-formal correspondence.<n>Our contributions include (i) the construction of a structured dataset of formalized exercises, (ii) a systematic methodology for formalizing textbook mathematics, and (iii) an analysis of recurring challenges in the formalization process.
  arXiv  Detail & Related papers  (2026-05-20T08:15:43Z)
• Reasoning over mathematical objects: on-policy reward modeling and test time aggregation [120.92237765735813]
  We build and release training data and benchmarks for deriving mathematical objects, the Principia suite.<n>We show how on-policy training can also be used to scale test-time compute via aggregation.<n>We find that strong LMs such as Qwen3-235B and o3 struggle on Principia, while our training recipes can bring significant improvements.
  arXiv  Detail & Related papers  (2026-03-19T13:27:12Z)
• MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics [51.65118519899584]
  We introduce MathlibLemma, the first LLM-based multi-agent system to automate the discovery and formalization of mathematical folklore lemmas.<n>We further construct the MathlibLemma benchmark, a suite of 4,028 type-checked Lean statements spanning a broad range of mathematical domains.
  arXiv  Detail & Related papers  (2026-01-30T15:24:42Z)
• ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
  We propose a Reflective Autoformalization method that integrates semantic consistency evaluation into the autoformalization process.<n>This enables the model to iteratively generate formal statements, assess its semantic fidelity, and self-correct identified errors.<n>Experiments show that ReForm achieves an average improvement of 22.6 percentage points over the strongest baselines.
  arXiv  Detail & Related papers  (2025-10-28T16:22:54Z)
• DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems [14.568293842955065]
  DRIFT is a framework that decomposes informal mathematical statements into smaller, more tractable ''sub-components''<n>It retrieves illustrative theorems to help models use premises more effectively in formalization tasks.<n>We evaluate DRIFT across diverse benchmarks (ProofNet, ConNF, and MiniF2F-test) and find that it consistently improves premise retrieval.
  arXiv  Detail & Related papers  (2025-10-12T21:42:04Z)
• FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
  We present FormalMATH, a large-scale Lean4 benchmark comprising 5,560 formally verified problems spanning from high-school Olympiad challenges to undergraduate-level theorems.<n>We introduce a novel human-in-the-loop autoformalization pipeline that integrates statement autoformalization, semantic verification, and negation-based disproof filtering strategies.<n>Our evaluation of state-of-the-art LLM-based theorem provers reveals significant limitations.
  arXiv  Detail & Related papers  (2025-05-05T15:37:00Z)
• Learning an Effective Premise Retrieval Model for Efficient Mathematical Formalization [29.06255449960557]
  We introduce a novel method that leverages data extracted from Mathlib to train a lightweight and effective premise retrieval model.<n>The model is learned in a contrastive learning framework, in which a fine-grained similarity calculation method and a re-ranking module are applied.<n> Experimental results demonstrate that our model outperforms existing baselines, achieving higher accuracy while maintaining a lower computational load.
  arXiv  Detail & Related papers  (2025-01-21T06:32:25Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  This work proposes Alchemy, a framework for data synthesis that constructs formal theorems through symbolic mutation.<n>For each candidate theorem in Mathlib, we identify all invocable theorems that can be used to rewrite or apply to it.<n>As a result, our method increases the number of theorems in Mathlib by an order of magnitude, from 110k to 6M.
  arXiv  Detail & Related papers  (2024-10-21T08:04:21Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.