autoformalization

The authors introduce Choir, an open, modular protocol for distributed multi-agent autoformalization that decomposes projects into GitHub-based tasks with deterministic trust-gate verification, supporting Lean 4, Isabelle, and Rocq; it includes a preprint and an open-source repo funded by DARPA's expMath program.

This arXiv paper studies how language models decide whether two scientific findings are comparable before resolving contradictions. In a controlled task with unsatisfiable XOR constraints translated into lab reports, GPT-5.6 Sol and Claude Opo 5 recover the best-supported assignment well when constraints are explicit, but models often defer to biological expectations when findings are presented in scientific prose.

华为 Lagrange 数学计算研究中心提出 Sage，一个四阶段分解生成管线加双重信号语义校正循环的自动形式化框架，将答案泄漏率从70.9%降至2.7%，在 Omni-MATH NP 上达到73.3% pass@4，并在新提出的 IMO-Unformalized 基准上零样本达到87.4%验证保真度。

This paper proposes Generative Verification (GenV), a method using generative reward models to detect reference-equivalence failures in autoformalization, addressing vulnerabilities in neurosymbolic systems and improving verification accuracy.

This paper introduces SA-Pass, a method for evaluating semantic alignment in autoformalization, and presents ShadowBench, a Lean 4 benchmark with 178 problems, demonstrating high agreement with expert judgments.

FormalTCS is a benchmark for evaluating large language models on end-to-end theoretical computer science research, revealing significant limitations, especially in autoformalization.

MathForm introduces a framework for mathematical autoformalization using knowledge retrieval and verification-guided refinement, yielding the FormalVerse dataset and an 8B model that outperforms specialized baselines.

LeanFlow is an LLM agent system for translating mathematical papers into formalized Lean projects, evaluated through case studies and benchmarks with Kimi-K2.6 and GPT-5.5, achieving high completion rates within budget constraints.

This position paper argues for theory-level autoformalization, which formalizes entire theories including axioms, definitions, and lemmas as coherent libraries, rather than isolated statements. It discusses the significance, alternative views, open challenges, and proposes paths forward for this shift in formalization research.

Presents an agentic framework using general coding LLMs to autoformalize research-level mathematics into Lean 4 code, evaluated on Putnam problems and STOC conference papers.

Mistral AI releases Leanstral 1.5, an updated Lean 4 formal proof engineering model optimized for automated theorem proving and autoformalization, with 119B total parameters and 6.5B active parameters.

This paper introduces SD-GPS, a solver-driven framework for geometry problem solving that uses autoformalization guided by solver feedback and verified theorem proposing to overcome bottlenecks in neuro-symbolic systems.

This paper introduces a signal-coverage matrix that decomposes type-correctness gains in autoformalization into four strata, revealing the mechanisms behind LLM refinements and showing that headline metrics can obscure which errors are actually resolved.

This paper presents an autoformalization pipeline that translates agent prompts, MCP tool descriptions, and natural language policy documents into formally verified policies using an LLM-based generator-critic loop, achieving better coverage than hand-coded enforcement on MedAgentBench.

This paper presents an architecture that uses formally verified law as a reward signal for training legal AI, adaptively autoformalizing legal rules into a formal calculus and employing a verifier to ensure provable correctness, demonstrated on German and US law examples.

This paper evaluates the robustness of proof autoformalization models in Lean 4 under global and local perturbations, finding that current LLM-based models are sensitive to perturbations and often fail to faithfully reflect local changes.

Introduces PrologMCP, an open-source server that exposes Prolog as a stateful tool via the Model Context Protocol, enabling LLM agents to delegate reasoning to a symbolic solver. Evaluation shows competitive or superior accuracy on deductive reasoning tasks compared to frontier reasoning LLMs.

This paper presents an agent pipeline for formalizing a numerical analysis textbook in Lean 4 and introduces a quality audit framework that evaluates semantic correctness and library reuse beyond kernel acceptance, revealing common unfaithful formalization patterns.

This paper presents a case study of using a large language model (Claude Code) to formalize Grothendieck's vanishing theorem in the Lean theorem prover. It finds that while agents can produce verified code, they struggle with definitions and API design, emphasizing the need for expert review beyond mere compilation.

Researchers from Oxford, Cambridge, MIT, CMU and other institutions conduct a mixed-methods study examining how people integrate AI tools into mathematical proof formalization workflows, finding that participants generally achieve higher formalization accuracy with AI assistance while preferring to maintain high-level human control over the proof discovery process.