# ProofGap: Benchmarking Step-Level Formal Reasoning with Local Obligations Derived from Natural-Language Solutions

> ProofGap decomposes 26,116 step-level proof gaps from Demidovich exercises, showing local obligations are far more tractable (35% Pass@8) than complete theorems (4%), with general-purpose models now outperforming specialized provers.

- **Source:** [arXiv](https://arxiv.org/abs/2609.29296)
- **Published:** 2026-09-26
- **Permalink:** https://picx.dev/p/KtlGVU
- **Whiteboard:** https://picx.dev/p/KtlGVU/image

## Summary

## Summary (Overview)

- **ProofGap** is a new fine-grained benchmark for step-level formal reasoning, derived from 3,015 exercises in Demidovich's *Problems in Mathematical Analysis*, yielding **26,116 proof gaps**.
- The benchmark decomposes natural-language solutions into individual local proof obligations ($\Gamma \vdash g$), enabling evaluation of local formal proof construction independent of end-to-end proof composition.
- A semantics-aware pipeline translates natural-language solutions into a formal intermediate representation (Relaxed NFL → Core NFL), from which proof-gap generators derive verification conditions.
- Experiments show step-level gaps are substantially more tractable than complete theorems (Pass@8: 31.99–35.39% vs. 2.92–4.28%), and general-purpose models outperform specialized provers on the balanced ProofGap-280 subset.
- The benchmark provides both an original DSL-based version with a lightweight checker and a Lean version with verified ground-truth proofs.

---

## Introduction and Theoretical Foundation

The paper addresses a critical gap in formal mathematics evaluation: existing benchmarks (miniF2F, ProofNet, PutnamBench) evaluate models at the **theorem level**, providing only a coarse success/failure signal. This is insufficient for:

- **Fine-grained diagnosis**: Theorem-level failure cannot distinguish between errors in local inference, autoformalization mistakes, or failures in global proof planning.
- **Process supervision**: Prior work (Lightman et al., 2024) shows step-level feedback provides more effective training signals than outcome-only supervision.
- **Localized verification**: Applications like SAFE (Liu et al., 2025) formalize individual reasoning steps for Best-of-N trajectory selection, requiring trustworthy, localized formal feedback.

**Key motivation**: Mathematical analysis is particularly challenging because local inferences often depend on implicit conditions — domain restrictions, nonzero conditions, sign conditions, and convergence assumptions. MA-ProofBench (Pu et al., 2026) found models achieving near-zero formal proof success despite producing correct natural-language proofs, highlighting the need for finer-grained evaluation.

**Theoretical foundation**: A ProofGap instance is formally defined as a triple:

$$(\Gamma, g, m) \tag{1}$$

where $\Gamma$ is the well-scoped local context, $g$ is the target proposition, and $m$ is an optional strategy annotation. The task requires establishing:

$$\Gamma \vdash g \tag{2}$$

---

## Methodology

### Benchmark Construction Pipeline

The construction proceeds in three stages:

**Stage 1: Relaxed NFL Translation**
- A prompt-based translator converts each problem/solution into **Relaxed Natural Formal Language (Relaxed NFL)**, a parser-readable intermediate representation preserving conditions, goals, proof structure, and method annotations.
- Output undergoes parser validation and representation-consistency screening (checking preservation of assumptions, goals, and proof steps).

**Stage 2: Core NFL Elaboration**
- Relaxed NFL AST is elaborated into **Core NFL**, a normalized representation with explicit proof contexts and variable bindings.
- Transformations decompose compound propositions, disambiguate notation, canonicalize operations, and make free variables explicit.
- Notation normalization includes: $f'$ → $\text{FunDeri}(f, 1, 1)$ (first-order derivative w.r.t. first formal argument).

**Stage 3: Proof-Gap Generation**
- The generator traverses the Core NFL AST, maintaining current proof state $\Gamma \vdash g$.
- Each intermediate proposition $P$ emits obligation $\Gamma \vdash P$ and adds $P$ to the context.
- Each gap is translated to Lean using GPT-5.6-sol, with human-in-the-loop cross-review auditing.

### Lightweight Proof-Checking Framework

- An **18-command domain-specific language (DSL)** with a deterministic checker.
- Features include `autosolve` for deterministic solving and a **514-entry theorem library**.
- A verifier-guided agent workflow uses checker feedback to revise candidate programs.

---

## Empirical Validation / Results

### Full-Set Solvability (RQ1)

**Table 3: Pass@8 (%) on all 26,116 gaps and 3,015 exercise theorems**

| Model | All gaps | Tactic-unsolved gaps | Exercise theorems |
|-------|----------|---------------------|-------------------|
| Goedel-V2-8B | 35.39 | 27.48 | 4.28 |
| DeepSeek-Prover-7B | 33.27 | 25.16 | 3.32 |
| Kimina-Distill-8B | 31.99 | 23.57 | 2.92 |

- Even the strongest prover leaves **64.61% of local obligations unsolved**.
- The strongest standard tactic (aesop) solves only 9.67% of gaps; the tactic union solves 11.20%.
- **Topic-level patterns** (Table 4): Best performance on functions/limits (39.10–44.41%), worst on parameter integrals (18.21–20.43%) — consistent ordering across all three provers.

### Effect of Proof Granularity (RQ2)

- Per-gap Pass@8: **31.99–35.39%** vs. complete-theorem Pass@8: **2.92–4.28%**.
- Mean exercise-level gap coverage: **27.63–31.15%** (Table 5).
- Parameter integrals: models solve 18.21–20.43% of gaps but ≤1.00% of complete theorems.

### Cross-Model Comparison (RQ3)

**Table 7: Pass@k on ProofGap-280 (gap / parent exercise)**

| Model | Pass@1 | Pass@3 | Pass@8 |
|-------|--------|--------|--------|
| **Specialized Provers** | | | |
| Goedel-V2-8B | 29.74/3.97 | 36.35/5.64 | 39.29/7.14 |
| DeepSeek-Prover-7B | 30.28/4.06 | 36.77/5.33 | 39.64/5.71 |
| Kimina-Distill-8B | 30.15/2.41 | 34.69/3.42 | 35.71/4.29 |
| **Open-Weight General** | | | |
| Kimi-K3 | 70.71/7.14 | 76.79/8.21 | 81.07/8.93 |
| DeepSeek-V4-Pro | 52.50/2.86 | 62.14/4.29 | 67.50/5.00 |
| GLM-5.2 | 47.86/1.79 | 61.43/2.50 | 65.00/3.21 |
| **Proprietary General** | | | |
| Claude-Opus-4.8 | 77.50/8.21 | 83.93/13.21 | 87.86/13.93 |
| GPT-5.6-sol | 79.29/12.99 | 84.97/17.61 | 87.86/21.43 |

- Every general-purpose model outperforms every specialized prover at gap level (GLM-5.2 at 65.00% exceeds best specialized at 39.64%).
- GPT-5.6-sol and Claude-Opus-4.8 **tie at 87.86% on gaps** but differ markedly on parent exercises (21.43% vs. 13.93%).

### Diagnostic Resolution (RQ4)

**Table 6: Local progress among theorem-failed exercises (%)**

| Model | Any gap solved | At least half | At least 75% |
|-------|---------------|---------------|--------------|
| Goedel | 78.03 | 22.59 | 4.99 |
| DeepSeek | 75.88 | 20.24 | 4.46 |
| Kimina | 72.39 | 18.79 | 4.68 |

- Theorem-solved exercises have mean gap coverage of **75.07–79.12%** vs. **26.08–29.19%** for theorem-failed exercises.
- **72.39–78.03%** of theorem-failed exercises contain at least one solved gap — refining binary failure into graded local progress.

---

## Theoretical and Practical Implications

**Theoretical significance:**
- Establishes **local formal proof completion** as a distinct evaluation dimension, separable from end-to-end proof composition.
- Demonstrates that theorem-level failure masks substantial local reasoning capability — models can discharge individual inferences while failing to compose complete proofs.
- The benchmark's structure (with 8.66 gaps per exercise on average and 8.33 assumptions per gap) enables fine-grained analysis of which mathematical topics and reasoning patterns pose the greatest challenges.

**Practical applications:**
- **Process supervision**: ProofGap-style obligations can provide machine-checkable training signals for process reward models, extending work like FoVer (Kamoi et al., 2026).
- **Proof verification systems**: The pipeline may support future natural-language proof verification, provided semantic translation and sequential proof composition are handled reliably.
- **Model diagnosis**: The benchmark identifies parameter integrals as a particularly challenging topic (18.21–20.43% gap Pass@8), suggesting specific areas for improvement.

---

## Conclusion

**Main takeaways:**
1. ProofGap provides a fine-grained, scalable benchmark for step-level formal reasoning with 26,116 gaps from 3,015 mathematical analysis exercises.
2. Step-level evaluation reveals substantial local reasoning capability hidden by theorem-level failure (31.99–35.39% vs. 2.92–4.28% Pass@8).
3. General-purpose models now outperform specialized provers on local obligations, though end-to-end proof composition remains challenging for all models.
4. The benchmark enables graded diagnosis of model failures, distinguishing between local inference errors and global proof-planning failures.

**Limitations:**
- Covers only one textbook (Demidovich) in mathematical analysis.
- Evaluation limited to Lean proof assistant.
- Does not directly measure natural-language autoformalization or invalid-step detection.

**Future directions:**
- Extend coverage across mathematical domains and proof assistants.
- Evaluate complete pipelines jointly addressing semantic translation, local proof discharge, and sequential proof composition.
- Use ProofGap-style obligations for training process reward models and improving end-to-end formal reasoning.

---

_Markdown view of https://picx.dev/p/KtlGVU, served by PicX — AI-generated visual whiteboard summaries of research papers._