Skip to content

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

🕒 Published (v1): 2026-04-24 20:47 UTC · Source: Arxiv · Venue: ACL 2026 · link

Why this paper was selected

Agents generate Lean-verified formal proofs from informal physics and math notation

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

💬 Ask ChatGPT✦ Ask Claude

TL;DR

FormalScience is a human-in-the-loop agentic pipeline that converts informal scientific reasoning (LaTeX) into syntactically valid and semantically aligned Lean4 formal proofs. Applied to physics, it produces FormalPhysics—200 university-level problems with 100% formal validity—and evaluates LLM autoformalisation baselines that expose a fundamental alignment-validity trade-off. The work also introduces the first systematic taxonomy of semantic drift in scientific autoformalisation.

Problem

Autoformalising scientific informal reasoning (especially physics with Dirac notation, vector calculus, non-commutative operators) into formally verifiable code is beyond current LLMs: purely automated approaches either compile code that is semantically empty or fail to compile at all. Existing formal math benchmarks (miniF2F, ProofNet, FormalMATH) cover pure mathematics and lack full informal-proof/formal-proof pairs; none address scientific domains.

Method

FormalScience operates in three stages, parameterised formally as follows.

Stage 1 — Informal dataset construction. Given a collection of informal proofs \(D\) and a gold-standard set \(D^* = [(S_1,P_1),\ldots,(S_{N'},P_{N'})]\), a few-shot template \(T_{fs}\) drives a multi-turn LLM session \(M\) to produce paired statement-proof batches: $\(X = \bigoplus_{d \in D} S\!\left[M\!\left(T_{fs}(d, D^*)\right)\right]\)$ A domain expert reviews alignment after each batch before proceeding.

Stage 2 — Iterative formal code generation. The Lean4 compiler \(L(C)\) returns \((0,\varepsilon)\) on success or \((1,e)\) on failure. An LLM agent \(M'\) generates initial code \(C^{(0)} = M'(T_g(x))\) then applies correction template \(T_c\) in a loop \(C^{(t+1)} = M'(T_c(x, C^{(t)}, e))\) until compilation succeeds, written compactly as \(C = R(C^{(0)})\).

Stage 3 — Human alignment classification. After compilation, a human expert acts as a binary classifier \(H(k) \in \{0,1\}\) on each proof's semantic alignment. Failed cases trigger LLM-based re-generation and recompilation (Eq. 5), repeated up to patience \(P\).

The agentic baseline (no human) implements a CodeAgent in the smolagents ReAct framework: surface guard → Lean compilation → error categorisation → structural errors trigger full regeneration; semantic errors (type mismatches, unsolved goals) invoke a patch agent that applies minimal unified diffs. Terminates after 25 ReAct correction cycles.

Key Contributions

  • FormalScience pipeline: domain-agnostic, human-in-the-loop semi-autoformalisation system achieving 100% Lean4 formal validity; constructed by one expert in ~1 month for ~$50 USD.
  • FormalPhysics benchmark: 200 university-level physics problems (quantum mechanics + electromagnetism) with NL statements, LaTeX proofs, and complete Lean4 proofs—the only benchmark with all four tuple components \((s_{NL}, p_{NL}, s_{FL}, p_{FL})\) alongside Herald-Proof.
  • Three-tier LLM evaluation: zero-shot, self-refinement with error feedback, and novel two-stage agentic pipeline (surface guard + patch agent) on FormalPhysics.
  • Semantic drift taxonomy: four categories—Notational Collapse, Abstraction Elevation, Proof Strategy Substitution, Implicit Premise Selection—with quantitative prevalence by physics subdomain.
  • Alignment-validity trade-off characterisation: Spearman/Pearson correlation between FV and mean alignment scores is ~0 (\(p > 0.9\)), confirming a fundamental trade-off in current approaches.

Results

  • FormalScience (GPT-5.1 + Claude-Opus-4.5, human-in-loop): FV = 100%, FQ = 73.5%, LP = 72.0%, MC = 72.5%.
  • Best agentic baseline (GPT-OSS-20B agent): FV = 31%, FQ = 72.5%, LP = 73.0%, MC = 72.0% — 3Ă— lower formal validity than FormalScience, but alignment scores comparable.
  • Zero-shot best (Kimina-7B): FV = 51.5% but FQ = 6.5%, LP = 10.5% (exploits compilation shortcuts with near-zero semantics).
  • Self-refinement: no meaningful improvement over zero-shot in formal validity or alignment under primary judge (GPT-4.1-mini); costs ~2Ă— tokens.
  • FormalPhysics complexity: ~2Ă— more mathematical objects and formulae per example than miniF2F/ProofNet/Lean Workbook; ~33% more than FormalMATH/Herald-Statement.
  • Semantic drift breakdown: Notational Collapse in >75% of QM proofs; Abstraction Elevation in ~25%; Proof Strategy Substitution in ~33%; Implicit Premise Selection in ~25% (only unambiguously beneficial category).
  • Compute cost for agentic baseline: 100+ GPU-hours per model on RTX 5090 (>30 min/proof).

Limitations

  • FormalPhysics is limited to 200 examples; insufficient for fine-tuning LLMs.
  • Lean4 lacks native support for vector calculus and Dirac notation, making true semantic preservation of physics fundamentally unattainable without new Mathlib extensions.
  • Human expert availability is a bottleneck; scalability depends on recruiting motivated domain experts.
  • Agentic baselines require 100+ GPU-hours on consumer hardware (RTX 5090), making systematic ablations expensive.
  • Alignment judges (GPT-4.1-mini, Qwen2.5-Coder-7B) introduce noise and diverge on absolute scores (though relative rankings remain consistent).
  • Physics subdomain coverage is restricted to quantum mechanics and electromagnetism; generalization to other sciences is not empirically validated.
  • The alignment-validity trade-off is documented but not resolved; no approach achieves both high FV and high alignment.

Relevance to Agentic AI / LLM Agents

FormalScience demonstrates a concrete human-in-the-loop agentic architecture where LLM agents interact with a symbolic compiler (Lean4) in a ReAct-style loop, making it directly relevant to the emerging paradigm of neuro-symbolic agents that ground reasoning in formal verification. The paper's finding that iterative tool-calling agents (31% FV) dramatically outperform zero-shot and naive self-refinement, yet still fall 3× short of human-guided pipelines, quantifies the gap between current autonomous agents and human-assisted ones for high-precision formal tasks. The alignment-validity trade-off and semantic drift taxonomy provide a new failure-mode vocabulary applicable to any agentic system that must bridge natural-language intent and formally verifiable output. The two-stage error categorisation (structural vs. semantic errors → full regeneration vs. patch agent) is a transferable architectural pattern for agentic code-repair loops.