17.4 Formal Verifier

Discriminative PRMs may learn incorrect labels, and generative PRMs may produce a fluent but incorrect proof. For the squared error in Section 17.1, humans can easily judge; but when the proof involves dozens of steps of algebra, the evaluation model itself may also make mistakes.

If the problem has already been written in formal languages such as Lean4, Coq, or Isabelle, the candidate proof can be submitted to a proof checker. The checker does not score based on whether the proof "looks reasonable," but rather verifies whether each proof step conforms to the rules of the formal system. This provides more deterministic feedback, but it also introduces a new prerequisite task: natural language problems must first be correctly formalized.

This section follows the line of "natural language problem → formal proposition → candidate tactic → core checker." First, we explain where the determinism comes from, then examine how AlphaProof, AlphaGeometry, and DeepSeek-Prover-V2 search for proofs, and finally discuss the scope of formalization, data, and computational costs.

1. Why Formal Checking Can Provide Deterministic Feedback

Generative PRMs judge whether a sentence is reasonable, still relying on model probability. A formal checker, however, requires the candidate proof to construct a proof term for the target proposition. Let us first compare what is omitted in the same proof when expressed in natural language versus Lean4.

1.1 Differences Between Formal Languages and Natural Languages

Mathematical proofs can be expressed in two languages:

Natural Language (informal):

Proof that √2 is irrational:
Assume √2 = p/q, where p and q are coprime.
Then p² = 2q², so p is even.
Let p = 2k, substitute to get 2k² = q², so q is also even.
This contradicts the assumption that p and q are coprime. Therefore, √2 is irrational.

This is easy for humans to read, but the "so" often omits intermediate lemmas, and the meaning of symbols may depend on context.

Formal Language (Lean4):

theorem sqrt_two_irrational : Irrational (√2) := by
  intro h
  rcases h with ⟨p, q, h1, h2⟩
  -- Assume √2 = p/q
  have h3 : p^2 = 2 * q^2 := by
    have : (√2)^2 = (p/q)^2 := by rw [h1]
    simp at this
    rw [div_pow] at this
    field_simp at this
    linarith
  -- ...
  sorry  -- (placeholder for the proof)

This code is only for illustrative purposes, and the sorry is a placeholder meaning "proof is not provided here." It cannot be considered as a valid verification result. A proof submitted to a verifier must remove the sorry and allow the Lean kernel to check each tactic step incrementally. If the check passes, it means that the proof terms generated by the tactics conform to the rules under the current axioms, theorems, and formalized proposition. It cannot guarantee that the natural language original problem has been correctly translated, nor can it rule out assumptions introduced by the selected axioms.

1.2 Characteristics of Lean4 Verifier

Several features of Lean4 make it suitable for providing process feedback:

• Deterministic Checking: Given a formal system, axioms, and a correct implementation, the system checks whether the representation of a proof satisfies the rules.
• Automation: The compilation process is automatic, requiring no human judgment.
• Extensibility: New mathematical structures and theorems can be defined.
• Community Support: Mathlib has already formalized university-level mathematics.

1.3 The Limits of Formalization

However, formalization also has its costs:

• Domain-Specific: Lean4 is primarily used for mathematics. Other domains (natural language reasoning, code logic) lack mature formalization systems.
• Data Scarcity: Lean4 code is relatively scarce, leading to insufficient pre-training data for LLMs on Lean4.
• High Barrier to Entry: Writing Lean4 code requires specialized training, and most mathematicians are not familiar with it.

2. How AlphaProof and AlphaGeometry Search for Proofs

A proof checker can only answer "Is this step in compliance with the rules?" and will not actively suggest the next step. To automatically solve new problems, a strategy model is needed to generate tactics, a value model to estimate the state of a proof, and a search mechanism to try different approaches.

In July 2024, DeepMind announced AlphaProof and AlphaGeometry 2 which collectively solved four problems from the International Mathematical Olympiad (IMO) 2024, achieving scores in the silver medal range. AlphaProof is responsible for formalizing proofs in algebra and number theory, while AlphaGeometry 2 handles geometry problems.

2.1 Architecture of AlphaProof

AlphaProof integrates the reinforcement learning style of AlphaZero, proof search, and the Lean checker:

┌────────────────────────────────────────────────────┐
│ 1. Problem Formalization: Translate mathematical problems into Lean4           │
│                                                                                   │
│ 2. AlphaZero-style Search:                                                         │
│    - Policy Network: Recommends the next Lean4 tactic                            │
│    analogously to the policy network in AlphaZero.                                │
│    - Value Network: Evaluates the current proof state                            │
│    - Search Algorithm: Allocates computation among candidate tactics              │
│                                                                                   │
│ 3. Lean4 Verifier: Automatically verifies each tactic                             │
│                                                                                   │
│ 4. Self-Play Training: Trains the policy and value networks using search results  │
└────────────────────────────────────────────────────┘

It follows the structure of AlphaGo Zero, which "proposes actions through policy, evaluates states through value, and uses search to generate better training targets." In Go, the actions are placing stones; in formal proof, the actions are tactics. The proof state, termination conditions, and data generation methods remain different from those in a game of Go.

2.2 How AlphaProof Constructs the Training and Search Loop

Design I: Constructing a Formalized Training Problem

Natural language problems must first be converted into Lean propositions. During the training phase, DeepMind uses a formalizer to convert approximately one million informal problems into formalized ones, forming training databases of varying difficulty. The six official competition problems from IMO 2024, however, are manually translated by experts, and it is not acceptable to mix automatically formalized training data with competition inputs.

The formalizer may misinterpret quantifiers, variable scopes, or implicit conditions. Lean can only check whether "the translated proposition is provable," so the system also needs to independently verify whether the formal proposition accurately reflects the original problem.

Design II: Large-Scale Training with Lean4

The training database includes both automatically converted formal propositions from natural language problems and related problems generated during the search process. AlphaProof attempts to prove or disprove these propositions, and the results passed by Lean are then used to update the policy. Public materials do not provide sufficient details to reproduce the full data ratio.

Design III: Lean Checking Enters the Search Loop

Each node corresponds to the current proof state, and each action corresponds to a candidate tactic. The Lean checker first eliminates invalid actions, and the trajectories that complete the proof become reinforcement learning signals. Public descriptions describe this process as a combination of the AlphaZero algorithm and proof search, without the need to limit it to a particular undisclosed MCTS implementation.

2.3 Performance of AlphaProof

In the six problems of IMO 2024, AlphaProof solved two algebra problems and one number theory problem, while AlphaGeometry 2 solved one geometry problem. Combined, the two systems scored 28 points (out of a maximum of 42), reaching the silver medal range for that year. Failures on the remaining problems may occur at different stages, such as formalization, candidate generation, or search budget, and cannot be attributed solely to the final failure.

2.4 How AlphaGeometry Handles Geometry Problems

To address the shortcomings of AlphaProof in geometry, DeepMind released AlphaGeometry 2—a specialized formal system for solving geometry problems.

AlphaGeometry 2 combines a neural language model with a symbolic reasoning engine: the language model proposes auxiliary constructions, and the symbolic system performs deduction and verification. Synthetic geometry problems enrich the training data, while auxiliary lines enable the system to open proof paths that would otherwise be inaccessible.

In the IMO 2024, after receiving human-formalized problems, AlphaGeometry 2 completed the 4th problem in 19 seconds. This case illustrates that dedicated formal systems can quickly check and compose geometric relationships, but the conversion from natural language to formal input remains outside the system's boundaries.

3. How DeepSeek-Prover-V2 Generates Verifiable Proofs

AlphaProof demonstrates that search and the verifier can collaborate. Open-source work must also answer questions about how to construct training data, how to decompose complex theorems, and how to use binary pass signals for reinforcement learning. DeepSeek-Prover-V2 provides another set of verifiable implementations.

DeepSeek-Prover-V2 (2025.04) is DeepSeek's open-source work on formal PRM. Its goals are:

• To train an open-source model using Lean4 + RL that can solve math competition problems
• To advance the industrial usability of formal PRM

3.1 Method of Prover-V2

DeepSeek-Prover-V2 starts from natural language proof sketches, breaks down complex theorems into smaller sub-goals, and completes each with a dedicated proof model.

Improvement One: Recursive Proof Search

Prover-V2 employs recursive theorem proving — breaking a difficult theorem into several sub-goals, which are further decomposed until the sub-goals can be independently proven.

Main Goal: Prove A
  ├── Sub-goal 1: Prove B (If B holds, then A holds)
  │     ├── Sub-sub-goal 1.1: Prove C
  │     └── Sub-sub-goal 1.2: Prove D
  └── Sub-goal 2: Prove E

This decomposition transforms a long proof into small lemmas with clear dependencies. Earlier sub-goals can serve as premises for subsequent sub-goals, and the verified local proofs are finally combined to form a complete proof.

Improvement Two: Binary Reward

Prover-V2 uses a binary reward system: a reward of 1 for a successful proof and 0 for a failed one. For the same formalized proposition and proof, the result from Lean4 is deterministic. If the natural language problem is incorrectly formalized, even if the proof passes, the reward still corresponds to an incorrect proposition. Therefore, the checker reduces the noise in proof verification but cannot eliminate errors in data and translation.

Improvement Three: Generating Training Data with Verified Proofs

DeepSeek automatically generates a large amount of Lean4 theorems and proofs for training. The generation process includes:

• Using an LLM to generate Lean4 propositions from natural language math problems
• Using the proof model to recursively solve sub-goals
• Taking the found proofs as training data

3.2 Prover-V2's Performance

The paper reports that the 671B model achieves 82.4% Pass@32 on MiniF2F-test, and reaches 88.9% when the candidate budget is increased to Pass@8192. It also solves 47 out of 658 problems in PutnamBench. The significant difference in the number of candidates means that the 88.9% cannot be interpreted as the success rate of a single proof attempt. It indicates that increasing the formal proof search budget can cover more problems, while the computational cost also increases with the number of candidates.

4. Where Can Formal Verification Be Applied

Formal checking makes the judgment of "whether a step is correct" more reliable, but it does not automatically formalize all problems. Before applying formal verification, one must sequentially check: whether the task can be defined precisely, whether perceptual or natural language input can be reliably translated, and whether the cost of proof search is acceptable.

The feedback from formal PRM is more deterministic, but applying it requires the following conditions:

4.1 Domain-Specific Constraints

Lean4 is mainly used for mathematics. For other domains:

• Code Logic: Tools like Dafny, F*, and Coq can be used, but they require the specification and invariants to be written first.
• Natural Language Reasoning: Only some tasks can be translated into logical constraints, and open-ended problems are difficult to fully formalize.
• Multimodal Reasoning: Perceptual results themselves carry uncertainty, and typically only the symbolic reasoning part can be formalized.

Therefore, the current best coverage is in mathematical proofs and program verification with clear specifications; open-ended language tasks can only be formalized for parts with well-defined boundaries.

4.2 Scarcity of Formalized Data

The corpus and theorem library of Lean4 are much smaller than general natural language corpora, and "code lines" cannot be directly converted to "text tokens." As a result, the model's ability to learn tactics, library interfaces, and proof patterns is limited by the coverage of the data, making it prone to failure in syntax, theorem retrieval, and proof search. The quality of automatic formalization and the cost of checking further limit the number of problems that can be covered.

4.3 Translation Cost

Formalizing PRM requires translating the task into Lean4. A single error in quantifier or type translation may lead the checker to prove a proposition different from the original problem. Reliable systems need to preserve the correspondence between natural language and formal propositions, and semantic deviations must be detected by human review, testing, or another translation verification system.

4.4 Training Cost

Proof search repeatedly generates tactics and invokes the Lean checker. As the number of branches and the depth of the proof increase, the number of checks also rises rapidly. The actual cost depends on caching, parallelism, the theorem library, and the search budget; public data is insufficient to summarize all systems with a fixed multiple.

4.5 How to Expand the Coverage of Formal Checking

Expanding the coverage requires separately addressing the three issues of input translation, proof generation, and domain specification.

Automatic Formalization

Letting LLMs learn to automatically translate natural language into Lean4 is the direction of research such as AlphaProof's formalizer and Autoformalization with Large Language Models.

Lean4 and LLM Hybrid

A middle-ground approach is to let LLMs first propose natural language reasoning steps, then translate the key lemmas that can be formalized into Lean4 for checking. Steps not formalized still need to be evaluated separately; the entire natural language reasoning cannot be considered proven just because some lemmas pass.

Extension to Other Domains

Code can be checked with tools like Dafny, F*, etc., for specifications and invariants. Physical and biological tasks can only be handed over to formal systems when objects, assumptions, and rules can be precisely defined. Perceptual data and open semantics still require probabilistic models or human judgment.

Neural-Symbolic Integration

Language models are responsible for proposing lemmas and candidate steps, while formal systems are responsible for checking rules. Between the two, failure information must be preserved: which tactic is invalid, which subgoal remains unsolved, and whether the natural language proposition is translated consistently. Only when the "generate—check—refine" loop is complete can formal feedback guide the next search.

Summary

Formal PRM uses systems like Lean4 to check candidate proofs. AlphaProof and DeepSeek-Prover-V2 demonstrate that language models can be responsible for proposing candidates and guiding the search direction, while proof checkers are responsible for verifying formal rules.

The boundaries of formal feedback are also clear: Lean data is much less than natural language corpora, automatic formalization may alter the problem's meaning, and proof search requires a large number of candidates. It is suitable for tasks with precise rules and cannot directly replace the outcome rewards or model evaluation in open language tasks.

Thus far, we have reviewed the three approaches to PRM:

• Discriminative PRM (17.2): High labeling cost, but low inference cost
• Generative PRM (17.3): Can explain reasoning, but depends on the evaluation model's capability
• Formal PRM (17.4): Deterministic feedback, but only covers tasks that can be formalized

The next two sections will return the evaluator to the generation process: Section 17.5 uses step scores to guide Beam Search, ToT, and MCTS; Section 17.6 compares multiple complete reasonings and aggregates the answer.