Technical Summary: CAM-Bench

Problem Statement

Existing formal theorem-proving benchmarks for Large Language Models (LLMs) predominantly focus on Olympiad-style problems and algebraic domains (e.g., MiniF2F, PutnamBench, ProofNet). While these benchmarks have driven progress in formal reasoning, they leave computational and applied mathematics significantly underrepresented.

Problems in applied mathematics (e.g., optimization, numerical linear algebra, numerical analysis) differ fundamentally from isolated theorem statements. They are often context-dependent, relying on:

• Locally introduced definitions, notation, and algorithms.
• Chapter-specific conventions and elementary results.
• Inherited assumptions that are not explicitly stated in the exercise but are required for a faithful formalization.

Current benchmarks struggle to evaluate whether models can track these local assumptions, decompose proofs based on textbook contexts, and apply elementary results that are not yet available as standard lemmas in formal libraries like Mathlib4. There is a need for a benchmark that targets applied mathematics problems where the "local context" is as critical as the theorem statement itself.

Methodology

The authors introduce CAM-Bench, a Lean 4 theorem-proving benchmark comprising 1,000 proof targets derived from 778 textbook exercises in optimization, numerical linear algebra, and numerical analysis. The construction of this benchmark relies on a novel dependency-recovery and formalization pipeline designed to transform context-dependent exercises into self-contained, machine-verifiable targets.

1. Dependency Recovery and Enrichment Pipeline

To address the non-self-contained nature of textbook exercises, the authors developed a recursive dependency expansion procedure (Algorithm 1):

• Recursive Expansion: Starting from a raw exercise, the system extracts references (theorems, equations, algorithms) and recursively retrieves their definitions and dependencies up to a bounded depth.
• Bottom-Up Naturalization: The dependency tree is processed bottom-up. An LLM naturalizer merges enriched representations, resolving local references, standardizing notation, and smoothing transitions to ensure lower-level definitions are incorporated before higher-level dependencies use them.
• Implicit Condition Recovery: The system makes required assumptions explicit (e.g., domain restrictions, positivity, convexity) only when supported by the original problem or recovered context. This enrichment is source-grounded; it does not conjecture missing dependencies but holds them out if they cannot be recovered.
• Multi-Round Review: Enriched statements undergo a validation loop to check for missing assumptions, task drift, and Lean suitability. Repairs are constrained to fix local defects without altering the mathematical objective or inventing unsupported dependencies.

2. Modularization-Driven Lean Formalization

Once an informal target is established, the system converts it into Lean 4 code using a frozen-context, block-wise construction strategy:

• Semantic Block Decomposition: Heterogeneous exercises are decomposed into typed semantic blocks (definitions, optimization problems, algorithms, theorem targets). This separates supporting context from the final theorem goal.
• Incremental Translation: The system translates blocks sequentially. Previously accepted declarations are kept as a frozen, read-only context. This prevents cascading errors and localizes failures to the current block.
• Compiler-Guided and Semantic Repair:
  • Compilation Repair: If a block fails to compile, a fixer uses compiler diagnostics to generate local patches (syntax, type annotations, namespace resolution).
  • Semantic Review: A reviewer compares the compilable candidate against the informal block to ensure semantic fidelity (preserving variables, assumptions, and conclusions). Mismatches trigger semantic rewriting.
• History-Aware Control: The system maintains a history of failed attempts and rejection reasons to prevent oscillation and guide subsequent repairs away from previously failed directions.

3. Benchmark Construction and Validation

The final dataset includes the raw exercise, recovered context, normalized informal theorem, and the final Lean target. Validation occurs at two levels:

• Source-Level: Ensures the informal target is faithful to the textbook exercise and self-contained.
• Lean-Level: Ensures the formal declaration preserves the reviewed informal target. Only 92.5% of candidate declarations were deemed usable after semantic validation, highlighting the difficulty of faithful autoformalization.

Key Contributions

1. CAM-Bench Dataset: A curated benchmark of 1,000 Lean proof targets spanning optimization, numerical linear algebra, and numerical analysis. It provides traceable artifacts from raw exercises to machine-checked Lean targets, filling the gap in applied mathematics evaluation.
2. Dependency Recovery Pipeline: A novel method for constructing faithful Lean targets from context-dependent exercises. It combines recursive dependency expansion, source-grounded enrichment, and constrained repair to handle local definitions and assumptions that are not standard Mathlib4 lemmas.
3. Comprehensive Evaluation and Error Analysis: The paper evaluates frontier LLMs and formalization agents on CAM-Bench. It identifies specific failure modes:
   • Library/API Grounding: Models fail to ground proofs in available Mathlib infrastructure, hallucinating APIs or missing bridge results.
   • Formal Representation: Errors in type discipline, dimension/index mismatches, and coercion failures.
   • Proof Decomposition: Inability to decompose long-horizon proofs into auxiliary lemmas or maintain control over complex optimization/numerical arguments.

Results

Baseline Performance

• Non-Agentic Models: Even the strongest non-agentic baselines (e.g., Deepseek-v4-pro, Claude-sonnet-4-6) achieved low verified Lean accuracy, with the best reaching 19.67% (Pass@32).
• Informal vs. Formal Gap: There is a significant discrepancy between informal correctness (Pass@1 informal accuracy ~70–84%) and verified Lean correctness (<20%). Models capture high-level arguments but fail to satisfy strict Lean syntax, type discipline, and library constraints.
• Agentic Improvement: Agentic proof-search systems (e.g., GPT-5.4 with iterative repair and tool use) significantly improved performance, reaching 44.00% verified accuracy. However, this came at a high token cost (~1.96M tokens vs. ~0.26–0.70M for baselines).

External Agent Evaluation

Two external agentic systems, M2F and Aristotle, were evaluated on 200 sampled instances with an 8-hour time budget:

• M2F: Solved 143/200 instances (71.5%).
• Aristotle: Solved 125/200 instances (62.5%).
• Despite these improvements, the benchmark remains unsaturated. Many failures were attributed to missing mathematical infrastructure, long auxiliary-lemma chains, and optimization-specific reasoning.

Significance and Claims

The paper claims that CAM-Bench serves as a critical complement to existing formal benchmarks by targeting applied mathematics problems that rely on textbook concepts and elementary theorems. Its significance lies in:

1. Evaluating Context-Dependent Reasoning: It tests a model's ability to track local assumptions and reconstruct context, a capability essential for real-world formalization but often bypassed by isolated theorem benchmarks.
2. Diagnosing Systemic Bottlenecks: The results highlight that current LLM-based provers struggle not just with syntax, but with Mathlib grounding, type discipline, and long-horizon proof decomposition.
3. Driving Infrastructure Development: The benchmark suggests that progress in formal applied mathematics requires stronger Mathlib infrastructure (e.g., for matrices, spectra, convexity) and more capable agents that can manage long-horizon proof trajectories.

The authors maintain a modest stance, noting that while agentic systems improve performance, the benchmark remains challenging, and the results should be viewed as estimates of current capabilities rather than a solved problem. The benchmark is intended to be a component of a broader evaluation suite for mathematical reasoning systems.