Technical Summary: Visored: A Controlled-Natural-Language Prover for LLM-Generated Mathematics

Problem Statement

Large Language Models (LLMs) have demonstrated increasing capability in mathematical reasoning, yet they remain prone to hallucination. Consequently, AI-generated proofs are only as trustworthy as the verification process. While automated theorem provers (ATPs) and whole-proof models (e.g., those targeting Lean or Rocq) have achieved high pass rates on benchmarks like miniF2F, they typically require an already formalized statement as input. The critical bottleneck lies in autoformalization: the translation of informal mathematical prose into machine-checkable form.

This translation is non-trivial because informal mathematics relies on shared background, implicit side conditions (e.g., $x \neq 0$), and notational abuse that readers fill in automatically. A direct translation to a formal language requires committing to specific library lemmas, subtypes, edge-case conventions, and coercions (e.g., $\mathbb{N}$ vs. $\mathbb{Z}$ vs. $\mathbb{R}$) that leave no trace in the source text. Errors in these decisions rarely manifest as compiler errors but rather as "silent semantic drift," where a statement compiles but no longer reflects the original intent.

Methodology

Visored is a research prototype designed to bridge the gap between informal mathematical writing and formal verification by introducing a dependently-typed intermediate representation (IR) that sits between LaTeX and low-level provers like Lean.

Core Architecture

The system operates as a pipeline (Figure 2 in the paper) consisting of the following stages:

1. Controlled Natural Language (CNL) Input: Visored accepts a controlled subset of mathematical English embedded in LaTeX. The vocabulary (sentence templates like "Let...", "Assume...", "Then..." and LaTeX commands) is defined by external .lpcsv specification files, allowing the surface language to be extended without modifying the parser.
2. Syntax and Semantics: The input is parsed into a syntax tree and then elaborated into a Typed AST (sem AST). This stage resolves names, assigns types and kinds, and enforces well-definedness at type-check time. Following the PVS tradition, partial functions (e.g., $1/x$, $\sqrt{x}$, $\log x$) carry implicit hypothesis arguments (e.g., $x \neq 0$, $x \ge 0$) that must be discharged before the expression is accepted.
3. Mid-Level IR (MIR): The typed AST is lowered to Visored MIR, the substrate for the solver.
4. Cost-Bounded Solver: The solver discharges "Then..." obligations and well-definedness conditions using a rule-driven, cost-bounded engine (named "Miracle"). It employs a database of backward and forward rules (inspired by ProofGrader) and specialized tactics (e.g., algebraic normalizers, chain solvers) to close routine steps that mathematicians typically omit.
5. Optional Lean Emission: Accepted proofs can be transpiled into Lean 4. This is an optional downstream stage for external kernel verification. The transpilation process involves replaying the normalisation history and managing coercion witnesses between number systems.

Design Philosophy

Visored is built on two primary observations:

1. LLM Fluency: LLMs are trained overwhelmingly on informal mathematics. A CNL surface stays close to the domain where LLMs are already fluent, avoiding the need for the model to learn low-level prover syntax (tactics, library lemma names) from scratch.
2. Tractability: Bridging natural and formal reasoning is more tractable than full automated theorem proving. By having the LLM supply the proof outline in CNL, the solver only needs to close small, obvious steps, a task well within the reach of modern agentic engineering.

The system treats the "upward" semantic parsing (LaTeX $\to$ Visored) as the hard problem, handled by the LLM, while the "downward" projection (Visored $\to$ Lean) is a deterministic, mechanical process.

Key Contributions

• Dependent-Type IR for Autoformalization: Visored introduces a semantically rich IR where every decision with no surface trace in LaTeX (subtypes, library lemmas, edge-case conventions, casts) is made explicit.
• Spec-Driven Extensibility: The CNL surface is defined by external configuration files rather than hard-coded parsers, allowing the vocabulary to be tuned to specific mathematical conventions (textbook, competition, research) without recompiling the system.
• Localized Diagnostics: Unlike systems that provide a single accept/reject verdict after a full Lean compilation, Visored provides localized diagnostics at the stage of elaboration or solving. This allows for a "verify-and-revise" loop where an LLM can pinpoint and fix specific errors.
• Well-Definedness Enforcement: The system enforces well-definedness (e.g., ensuring $x \neq 0$ before $1/x$) via implicit hypothesis arguments discharged by the solver, rather than relying on the target prover's totalization conventions.
• Integration of Existing Schools: Visored synthesizes elements from Mizar/Naproche (CNL surface), PVS (well-definedness at type-check time), Lean/Rocq (dependent types), and ProofGrader (cost-budgeted rule-driven solving) into a single LLM-facing pipeline.

Experimental Results

The authors report a coverage study on the miniF2F-valid split (244 problems), which served as both the development and evaluation set.

• Performance: An LLM coding agent (Claude), guided by a skill document describing the CNL surface, produced Visored-checked proofs for 222 out of 244 problems (91%).
• Breakdown:
  • Induction: 100% (8/8)
  • Algebra: 98% (86/88)
  • Number Theory: 97% (66/68)
  • AMC/AIME: 93% / 87%
  • IMO (Olympiad): 35% (7/20)
• Failure Analysis: The unsolved problems were attributed to gaps in Visored's rule database (e.g., missing AM-GM inequality, lack of finite-field types, trigonometric identities) or regressions in the prototype, rather than the LLM's inability to find the proof strategy. The authors explicitly state that the agent failed to solve these because the necessary "machinery" was not yet implemented in the system.
• Transpilation Cost: The current sparse emission scheme results in highly verbose Lean output, with a median line-count ratio of $\approx 250\times$ compared to hand-written Lean proofs, and a tail reaching $\approx 25,000\times$. This is due to the replay of normalization steps and coercion witnesses.

Significance and Claims

The paper positions Visored not as a competitive automated theorem prover, but as a proof-of-concept for a new infrastructure for checking and organizing AI-produced informal mathematics.

• Modest Claims: The authors explicitly state they do not claim competitive automated theorem proving, nor do they extrapolate results to held-out test splits. The 91% coverage is presented as a lower bound on what the design can express, not a tuned pass rate.
• Shift in Bottleneck: The work supports the view that the binding constraint in AI mathematics is shifting from "generating ideas" to "verifying and organizing them at scale."
• Utility Modes: Visored is designed to function in four modes:
  1. Inference-time verifier: A real-time checker for LLM outputs.
  2. Autoformalizer loop: A mechanism for LLMs to rewrite proofs based on localized diagnostics.
  3. Dense reward signal: Providing per-step feedback for Reinforcement Learning (RL).
  4. CNL data generator: Creating a renewable corpus of formally checked, naturally reading proofs.

The paper concludes that the combination of a CNL surface, a dependently-typed IR, and a rule-driven solver creates a pipeline where failures are localized and actionable, offering a more reliable route from informal prose to kernel-checked proofs than current direct autoformalization approaches. The unsolved problems represent a backlog of missing rules and machinery, not a fundamental limitation of the design.