Technical Summary: Mask-Proof

Problem Statement

While Large Language Models (LLMs) are increasingly capable of mathematical problem solving and research-level proofs, there is a critical lack of scalable, reproducible instruments to measure step-level reasoning in long proofs across diverse sources. Existing evaluation methods suffer from three primary limitations:

1. Answer-Centric Bias: Benchmarks like GSM8K and MATH focus on final answers, failing to evaluate the rigor of the intermediate reasoning process.
2. Costly Expert Grading: Evaluating proof quality often requires human experts, which does not scale and is difficult to reproduce across domains.
3. Context and Dependency Gaps: Real-world research proofs rely on external lemmas, macros, and unstated background facts. Masking steps without recovering these dependencies leads to underdetermined tasks where failures are uninterpretable (confounding reasoning ability with missing information).
4. Verification Difficulty: Automated checking is hindered by notational diversity and equivalent reformulations, making string matching inadequate and symbolic tools insufficient for general guarantees.

Methodology: The Mask-Proof Pipeline

The authors introduce Mask-Proof, an LLM-based automated data curation pipeline designed to transform heterogeneous research proofs into verifiable, self-contained, step-level evaluation problems. The pipeline operates through three core stages:

1. Paper Collection and Proof Extraction

• Source: The pipeline curates recent arXiv submissions (August–October 2025) to minimize pretraining contamination.
• Filtering: It extracts LaTeX sources and filters out trivial proofs (e.g., purely definitional or pattern-completable) to ensure non-trivial reasoning is required.
• Human Audit: All final instances undergo manual auditing by domain experts to verify mathematical correctness, context sufficiency, and the absence of shortcut cues.

2. Automated Data Curation

The pipeline employs Codex CLI to perform two critical tasks:

• Self-Contained Recovery: The system resolves dependencies by traversing internal cross-references (e.g., \ref, \eqref) and expanding user-defined macros. For implicit dependencies (symbols defined elsewhere), it searches the source LaTeX for defining statements and appends them as "Additional Information." This ensures the masked step is solvable using only the provided context.
• Agentic Masking: Instead of random masking, the pipeline uses an agent to select key inference-critical formula steps. These steps are replaced with a [MASK] token. The selection rubric ensures the masked step cannot be solved by local surface cues or shallow pattern matching, forcing the model to synthesize global definitions with local variables.
• Faithfulness: The pipeline decouples step selection from mask application to prevent unintended proof rewriting, ensuring the remaining text remains identical to the original.

3. Automated Evaluation (Mask-ProofJudge)

• Task: Models are tasked with reconstructing the masked formula step.
• Judge: An LLM-based evaluator (GPT-OSS-120B High) assesses semantic equivalence between the model's output and the ground truth.
• Variance Reduction: To handle generation stochasticity, the system samples four solutions per problem and aggregates judgments via majority voting.
• Metric: The primary metric is Avg@4, representing the average correctness over four independent attempts.

Key Contributions

1. Mask-Proof Pipeline: A reproducible, automated framework that converts real-world research proofs into verifiable masked-step tasks, addressing the "what to measure" and "how to score" challenges in step-level evaluation.
2. Mask-ProofJudge: An automatic evaluation framework calibrated against expert judgments, achieving 96.8% agreement with human annotators through variance-reduced voting.
3. Mask-ProofBench: A benchmark comprising 292 curated problems across diverse research areas (e.g., algebraic geometry, topology, PDEs). All instances are manually audited and designed to be self-contained.

Experimental Results

The authors evaluated 17 state-of-the-art LLMs (both standard and reasoning-enhanced) on Mask-ProofBench and a cross-dataset subset derived from IMO-ProofBench.

• Reasoning Capability Boundary: A clear performance boundary emerged at approximately 32% accuracy. All reasoning-enhanced models (e.g., GPT-5.2, DeepSeek-R1) exceeded this threshold, while standard models fell below it. Reasoning-enhanced models outperformed standard counterparts by 12% to 27%.
• Ablation on Self-Containedness: Removing the dependency recovery module caused performance degradation of 11% to 23%, confirming that context completeness is essential for valid evaluation.
• Ablation on Masking Strategy: Random masking inflated scores significantly (e.g., standard models jumping from ~8% to ~50%), effectively eliminating the performance gap between reasoning and standard models. Agentic masking was shown to be necessary to prevent shortcut exploitation and maintain discriminative power.
• Correlation with Experts: When applied to IMO-ProofBench, the Mask-Proof pipeline achieved a Spearman's rank correlation of 0.79 with expert human grading, despite using no human-in-the-loop scoring or custom rubrics.
• Reproducibility: Independent runs of the pipeline showed high consistency in dependency recovery (97.2% recall) and mask selection (89.3% consistency when counting semantically proximate masks).

Significance and Claims

The paper claims that Mask-Proof addresses the "measurement gap" in AI for Science by providing a faithful, reproducible, and comparable method for evaluating step-level mathematical reasoning.

• Scalability: It offers a low-cost alternative to expert grading, enabling the evaluation of in-the-wild research-level proofs.
• Validity: By enforcing self-contained contexts and agentic masking, the benchmark measures genuine inference rather than shortcut exploitation or context copying.
• Generalization: The pipeline successfully generalizes to external datasets (IMO-ProofBench), producing model rankings that align with expert consensus without requiring domain-specific rubric design.

The authors conclude that while limitations exist regarding non-LaTeX sources and potential residual leakage, Mask-Proof establishes a foundation for studying step-level reasoning as a reproducible scientific phenomenon, moving beyond final-answer accuracy to assess the rigor of the proof process itself.