Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases

• URL: http://arxiv.org/abs/2607.13292v1
• Date: Tue, 14 Jul 2026 21:58:52 GMT
• Title: Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases
• Abstract summary: We argue for theory-level autoformalization: formalizing complete theories, including all their inter-dependencies, as structured libraries.<n>We examine the significance of this shift, address alternative views, identify open challenges, and propose three promising paths forward.
• Score: 32.96018876882992
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: Autoformalization translates informal natural language into formal, machine-verifiable languages. While most work focuses on individual statements, real formalization efforts are inherently theory-level: they require an entire web of axioms, definitions, and lemmas before target theorems can even be stated. In this position paper, we argue for theory-level autoformalization: formalizing complete theories, including all their inter-dependencies, as structured libraries. We examine the significance of this shift, address alternative views, identify open challenges, and propose three promising paths forward. Our survey of autoformalization is available at https://github.com/marcusm117/Awesome-Autoformalization.

Related papers

• Coherency through formalisations of Structured Natural Language, A case study on FRETish [0.0]
  Formalisation is the process of writing system requirements in a formal language.<n>In this paper we propose a new guideline: Coherency through Formalisations.<n>We analyze NASA's Formal Requirement Elicitation Tool FRET and propose an alternative automated translation of the Controlled Natural Language FRETish to the formal language of MTL.
  arXiv  Detail & Related papers  (2026-05-11T12:30:53Z)
• FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean [7.11696910077237]
  FormalScience is a human-in-the-loop agentic pipeline to produce textitsyntactically correct and textitsemantically aligned formal proofs of informal reasoning for low economic cost.<n>We construct FormalPhysics, a dataset of 200 physics problems and solutions (primarily quantum mechanics and electromagnetism) along with their Lean4 formal representations.<n>We evaluate open-source models and proprietary systems on a statement autoformalisation task on our dataset via zero-shot prompting, self-refinement with error feedback, and a novel multi-stage agentic approach.
  arXiv  Detail & Related papers  (2026-04-24T20:47:22Z)
• From Specification to Architecture: A Theory Compiler for Knowledge-Guided Machine Learning [6.365277569082624]
  Theory-guided machine learning has demonstrated that including authentic domain knowledge directly into model design improves performance.<n>Yet the process by which a formal domain theory is translated into architectural constraints remains entirely manual.<n>We propose the Theory Compiler: a system that accepts a typed, machine-readable domain theory as input and automatically produces an architecture.
  arXiv  Detail & Related papers  (2026-03-15T13:15:31Z)
• 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)
• Subject-Event Ontology Without Global Time: Foundations and Execution Semantics [51.56484100374058]
  The formalization includes nine axioms (A1-A9), ensuring the correctness of executable: monotonicity of history (I1), acyclicity of causality (I2), traceability (I3)<n>The formalization is applicable to distributed systems, microservice architectures, DLT platforms, and multiperspectivity scenarios (conflicting facts from different subjects)<n>Special attention is given to the model-based approach (A9): event validation via schemas, actor authorization, automatic construction of causal chains (W3) without global time.
  arXiv  Detail & Related papers  (2025-10-20T19:26:44Z)
• Towards a Common Framework for Autoformalization [2.487142846438629]
  Autoformalization has emerged as a term referring to the automation of formalization.<n>The goal of this paper is to review - explicit or implicit - instances of what can be considered autoformalization.
  arXiv  Detail & Related papers  (2025-09-11T19:28:56Z)
• StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion [30.51794514312176]
  We identify two key abilities for effective autoformalization.<n>We introduce ThinkingF, a data synthesis and training pipeline that improves both abilities.<n>The resulting 7B and 32B models exhibit both comprehensive formal knowledge and strong informal-to-formal reasoning.
  arXiv  Detail & Related papers  (2025-08-06T13:28:22Z)
• Autoformalizing Euclidean Geometry [74.72212706513318]
  We introduce a neuro-symbolic framework for autoformalizing Euclidean geometry. One challenge is that informal proofs rely on diagrams, leaving gaps in texts that are hard to formalize. We provide automatic semantic evaluation for autoformalized theorem statements.
  arXiv  Detail & Related papers  (2024-05-27T14:35:10Z)
• How Proficient Are Large Language Models in Formal Languages? An In-Depth Insight for Knowledge Base Question Answering [52.86931192259096]
  Knowledge Base Question Answering (KBQA) aims to answer natural language questions based on facts in knowledge bases. Recent works leverage the capabilities of large language models (LLMs) for logical form generation to improve performance.
  arXiv  Detail & Related papers  (2024-01-11T09:27:50Z)
• Provable Limitations of Acquiring Meaning from Ungrounded Form: What will Future Language Models Understand? [87.20342701232869]
  We investigate the abilities of ungrounded systems to acquire meaning. We study whether assertions enable a system to emulate representations preserving semantic relations like equivalence. We find that assertions enable semantic emulation if all expressions in the language are referentially transparent. However, if the language uses non-transparent patterns like variable binding, we show that emulation can become an uncomputable problem.
  arXiv  Detail & Related papers  (2021-04-22T01:00:17Z)

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.