FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean

Technical Summary: FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science

1. Problem Statement

The core challenge addressed in this paper is the autoformalisation gap in scientific domains (e.g., physics). While Large Language Models (LLMs) have made strides in translating informal mathematical reasoning (LaTeX) into formal languages (FL) like Lean4, they struggle with the specialized machinery required for the natural sciences. Specifically:

• Domain-Specific Notation: Modern LLMs struggle with Dirac notation (quantum mechanics) and vector calculus (electromagnetism).
• Semantic Drift: Even when an LLM produces syntactically correct code that compiles, the formal version often loses the original physical meaning (e.g., collapsing a quantum operator into a simple scalar), leading to "verifiable but incorrect" science.
• Library Incompatibility: Existing formal libraries (like Lean’s Mathlib) lack native, high-level support for many physics-specific operations, forcing models to use "shortcuts" that bypass actual physical reasoning.

2. Methodology

The authors propose FormalScience, a domain-agnostic, human-in-the-loop agentic pipeline designed to generate high-quality, formally verified datasets at a low economic cost.

A. The FormalScience Pipeline (Alg. 1):

1. Informal Expansion: Uses few-shot prompting to convert raw mathematical derivations into contextually rich, expanded natural language (NL) question-and-answer pairs.
2. Iterative Code Generation: An agentic loop attempts to generate Lean4 code. It uses a surface guard to reject malformed code and an iterative error-correction loop that uses compiler feedback to fix syntax and semantic errors.
3. Human-in-the-Loop Alignment: Unlike fully automated approaches, a human expert acts as a binary classifier to ensure the formal code remains semantically aligned with the original physics problem. If the expert detects "drift," the agent regenerates the code.

B. Evaluation Framework:
The authors constructed FormalPhysics, a new benchmark of 200 university-level physics problems (Quantum Mechanics and Electromagnetism) with their corresponding Lean4 formal proofs. They evaluated various models (open-source up to 30B and proprietary like GPT-5.1) using three approaches: Zero-shot, Self-refinement, and a multi-stage Agentic pipeline.

3. Key Contributions

• FormalScience Pipeline: A scalable, cost-effective method for experts (without deep formal language training) to produce verified formal datasets.
• FormalPhysics Dataset: A high-complexity benchmark that includes natural language statements, informal proofs, and complete formal proofs, specifically targeting the gaps in current math benchmarks.
• Taxonomy of Semantic Drift: The paper provides the first systematic characterization of how formalization fails in science, identifying four categories:
  • Notational Collapse: Complex operators (e.g., Dirac kets) are reduced to simple scalars.
  • Abstraction Elevation: Physical operations (e.g., vector calculus) are replaced by abstract algebraic properties.
  • Proof Strategy Substitution: The formal proof uses a different mathematical path than the informal one.
  • Implicit Premise Selection: The formal system surfaces hidden logical assumptions (the only "beneficial" drift).

4. Results

• Performance Gap: The human-in-the-loop FormalScience approach achieved 100% formal validity, significantly outperforming the best open-source agentic approach (GPT-OSS-20B), which reached only 31%.
• The Alignment-Validity Trade-off: A critical finding is that increasing a model's ability to produce compilable code often decreases its semantic alignment. Models frequently "cheat" by using mathematical shortcuts to satisfy the compiler while ignoring the underlying physics.
• Agentic Capabilities: The multi-stage agentic approach (using error categorization and "patch agents" for minimal diffs) successfully overcame the alignment-validity trade-off for open-source models, though it still lagged far behind the human-in-the-loop method.
• Drift Prevalence: Notational collapse was found in >75% of Quantum Mechanics proofs, highlighting a massive vulnerability in current AI-driven formalization of physics.

5. Significance

This work is significant because it moves the conversation of autoformalisation from "can the code compile?" to "is the science preserved?" By providing a methodology to build high-quality scientific datasets and a taxonomy to measure semantic loss, the authors provide a roadmap for developing more robust, "physics-aware" AI systems. It highlights that for scientific discovery and verification to be automated, formal libraries must be expanded to include domain-specific machinery, and LLMs must be evaluated on their ability to preserve physical meaning, not just syntactic correctness.