{"paper":{"id":"2609.00062.pdf","title":"RePro: Proof-Verified Benchmark Rewriting for Reliable Evaluation of LLM Mathematical Problem Solving","authors":["Xiyuan Zhou","Zhuoqi Li","Xinlei Wang","Yirui He","Yuhao Wu","Yuheng Cheng","Yan Xu","Junhua Zhao","Jinjin Gu"],"arxiv_id":"","url":"","source_kind":"pdf","ir_version":"1.0"},"generated_at":"2026-09-14T04:13:18.584551+00:00","counts":{"error":0,"warning":2,"info":0},"findings":[{"rule_id":"RL002","severity":"warning","confidence":0.75,"title":"Wrong source cited for 'Llama-3.2–1B/3B': LLaMA: Open and Efficient Foundation Language Models","explanation":"Method attributes 'Llama-3.2–1B/3B' to LLaMA: Open and Efficient Foundation Language Models (2023), but that work's own full text reads as partially supported for this attribution (the cited work is not the origin of the named artefact).\n\nModel rationale: The cited work introduces LLaMA models ranging from 7B to 65B parameters, i.e. an earlier generation of the LLaMA family, not the Llama-3.2-1B/3B variants named in the sentence. It is a closely related but different artefact (different family version/sizes).\n\nEvidence retrieved from the cited work (arxiv lookup, 1520 chars, full text).","paper_location":"Method — sentence citing [26]","evidence":[{"kind":"paper_span","source":"Citing sentence (method)","location":"method","quote":"Specifically, we include Qwen2–0.5B/1.5B, Qwen3–0.6B/1.7B/8B/14B (Yang et al., 2025a), Llama-3.2–1B/3B (Touvron et al., 2023), DeepSeek-R1–1.5B/7B/14B (Guo et al., 2025), and Gemma 3–1B/4B (Team et al., 2025).","url":"","values":{}},{"kind":"external_record","source":"Cited work (full text): LLaMA: Open and Efficient Foundation Language Models","location":"2302.13971","quote":"We introduce LLaMA, a collection of foundation language models ranging from 7B to 65B parameters.","url":"https://arxiv.org/abs/2302.13971","values":{}}],"suggested_action":"Cite the work that actually introduces 'Llama-3.2–1B/3B', or drop the attribution.","target_ids":["ref26"],"suppressed_count":0},{"rule_id":"RL004","severity":"warning","confidence":0.75,"title":"No ablation isolates the Executable Formalization","explanation":"The paper introduces Executable Formalization as one of its own contributions (it is referred to by a numbered contribution), but no reported experiment removes or replaces it. The ablation labels actually present are 'ATP', 'ATP -> DeepSeek-Prover-V2-7B / Kimina-Prover-Preview-Distill-7B / Goedel-Prover-V2-8B', 'rewriter model', 'rewriter -> Qwen3-MAX / Qwen3-32B / Qwen3-8B', 'ATP call limit', 'pass@1 -> pass@3', and none of them corresponds to Executable Formalization, so its individual contribution is not isolated by the experiments as reported.","paper_location":"Method","evidence":[{"kind":"paper_span","source":"Method","location":"","quote":"Executable Formalization converts rewritten instances that pass feasibility screening into machineverifiable formal statements in Lean.","url":"","values":{}},{"kind":"negative_search","source":"every experiment's ablated components and ablation label","location":"","quote":"Searched all 8 extracted experiment(s) for an ablation of 'Executable Formalization'. Ablation labels found: 'ATP', 'ATP -> DeepSeek-Prover-V2-7B / Kimina-Prover-Preview-Distill-7B / Goedel-Prover-V2-8B', 'rewriter model', 'rewriter -> Qwen3-MAX / Qwen3-32B / Qwen3-8B', 'ATP call limit', 'pass@1 -> pass@3'. No label matches 'Executable Formalization' or its tokens (executable, formalization).","url":"","values":{"ablations_found":6.0}}],"suggested_action":"Add a run with Executable Formalization removed or replaced by a simpler alternative, so the claim that it contributes can be separated from the rest of the method.","target_ids":["M2","K1"],"suppressed_count":0}],"top_findings":[{"rule_id":"RL002","severity":"warning","confidence":0.75,"title":"Wrong source cited for 'Llama-3.2–1B/3B': LLaMA: Open and Efficient Foundation Language Models","explanation":"Method attributes 'Llama-3.2–1B/3B' to LLaMA: Open and Efficient Foundation Language Models (2023), but that work's own full text reads as partially supported for this attribution (the cited work is not the origin of the named artefact).\n\nModel rationale: The cited work introduces LLaMA models ranging from 7B to 65B parameters, i.e. an earlier generation of the LLaMA family, not the Llama-3.2-1B/3B variants named in the sentence. It is a closely related but different artefact (different family version/sizes).\n\nEvidence retrieved from the cited work (arxiv lookup, 1520 chars, full text).","paper_location":"Method — sentence citing [26]","evidence":[{"kind":"paper_span","source":"Citing sentence (method)","location":"method","quote":"Specifically, we include Qwen2–0.5B/1.5B, Qwen3–0.6B/1.7B/8B/14B (Yang et al., 2025a), Llama-3.2–1B/3B (Touvron et al., 2023), DeepSeek-R1–1.5B/7B/14B (Guo et al., 2025), and Gemma 3–1B/4B (Team et al., 2025).","url":"","values":{}},{"kind":"external_record","source":"Cited work (full text): LLaMA: Open and Efficient Foundation Language Models","location":"2302.13971","quote":"We introduce LLaMA, a collection of foundation language models ranging from 7B to 65B parameters.","url":"https://arxiv.org/abs/2302.13971","values":{}}],"suggested_action":"Cite the work that actually introduces 'Llama-3.2–1B/3B', or drop the attribution.","target_ids":["ref26"],"suppressed_count":0},{"rule_id":"RL004","severity":"warning","confidence":0.75,"title":"No ablation isolates the Executable Formalization","explanation":"The paper introduces Executable Formalization as one of its own contributions (it is referred to by a numbered contribution), but no reported experiment removes or replaces it. The ablation labels actually present are 'ATP', 'ATP -> DeepSeek-Prover-V2-7B / Kimina-Prover-Preview-Distill-7B / Goedel-Prover-V2-8B', 'rewriter model', 'rewriter -> Qwen3-MAX / Qwen3-32B / Qwen3-8B', 'ATP call limit', 'pass@1 -> pass@3', and none of them corresponds to Executable Formalization, so its individual contribution is not isolated by the experiments as reported.","paper_location":"Method","evidence":[{"kind":"paper_span","source":"Method","location":"","quote":"Executable Formalization converts rewritten instances that pass feasibility screening into machineverifiable formal statements in Lean.","url":"","values":{}},{"kind":"negative_search","source":"every experiment's ablated components and ablation label","location":"","quote":"Searched all 8 extracted experiment(s) for an ablation of 'Executable Formalization'. Ablation labels found: 'ATP', 'ATP -> DeepSeek-Prover-V2-7B / Kimina-Prover-Preview-Distill-7B / Goedel-Prover-V2-8B', 'rewriter model', 'rewriter -> Qwen3-MAX / Qwen3-32B / Qwen3-8B', 'ATP call limit', 'pass@1 -> pass@3'. No label matches 'Executable Formalization' or its tokens (executable, formalization).","url":"","values":{"ablations_found":6.0}}],"suggested_action":"Add a run with Executable Formalization removed or replaced by a simpler alternative, so the claim that it contributes can be separated from the rest of the method.","target_ids":["M2","K1"],"suppressed_count":0}],"ir_summary":{"claims":18,"contributions":3,"method_components":11,"experiments":8,"baselines":3,"datasets":8,"metrics":4,"tables":4,"figures":9,"citations":42,"equations":0,"quantitative_results":718,"has_repository":false},"ir_health":{"observations":[{"code":"numbers-are-identifier-fragments","severity":"note","message":"10 extracted numbers are digits inside identifiers.","detail":"e.g. '1' in 'This suggests\\nthat benchmark reliability', '1' in 'GSM8K\\nMATH LV1 MATH LV2 MATH LV3 MATH LV', '2' in 'GSM8K\\nMATH LV1 MATH LV2 MATH LV3 MATH LV'. Rules that compare numbers across sections can report a contradiction between an identifier and a real value."},{"code":"compile-warning","severity":"note","message":"references: the reference list carries no entry numbers; citation keys are enumeration order [1]..[N], not labels printed in the paper, so a key may not match the [N] used in the body","detail":""},{"code":"compile-warning","severity":"note","message":"semantic extraction: dropped 6 items whose quote was not found in the paper","detail":""}],"errors":0,"warnings":0,"trustworthy":true},"diagnostics":{"source":"/home/oceann/workspace/research-linter/eval/papers/2609.00062.pdf","rules_run":["RL001","RL002","RL003","RL004","RL005"],"rules_skipped":[],"rule_errors":{},"rule_findings":{"RL001":0,"RL002":1,"RL003":0,"RL004":1,"RL005":0},"rule_seconds":{"RL001":0.02,"RL002":0.96,"RL003":4.48,"RL004":0.08,"RL005":0.06},"dropped_no_evidence":0,"demoted_low_confidence":0,"ir_health":{"observations":[{"code":"numbers-are-identifier-fragments","severity":"note","message":"10 extracted numbers are digits inside identifiers.","detail":"e.g. '1' in 'This suggests\\nthat benchmark reliability', '1' in 'GSM8K\\nMATH LV1 MATH LV2 MATH LV3 MATH LV', '2' in 'GSM8K\\nMATH LV1 MATH LV2 MATH LV3 MATH LV'. Rules that compare numbers across sections can report a contradiction between an identifier and a real value."},{"code":"compile-warning","severity":"note","message":"references: the reference list carries no entry numbers; citation keys are enumeration order [1]..[N], not labels printed in the paper, so a key may not match the [N] used in the body","detail":""},{"code":"compile-warning","severity":"note","message":"semantic extraction: dropped 6 items whose quote was not found in the paper","detail":""}],"errors":0,"warnings":0,"trustworthy":true},"notes":["RL001 funnel arithmetic: sentences_with_from=11 endpoint_pairs=1 claims_compared=0 emitted=0 [dropped: not-a-measurement=0]","RL001 funnel delta-column: structured_tables=3 with_exactly_one_delta_column=0 rows_checked=0 emitted=0","RL001 funnel cross-location: quant=718 prose=570 prose_with_metric=62 prose_with_dataset=36 prose_with_metric_and_dataset=0 distinct_buckets=0 emitted=0 [dropped: not-a-measurement=0 not-in-quote=32]","RL001 funnel identifier-drift: settings_checked=2 sections_stating_one_value=0 emitted=0","RL002 citation entailment: attempted 15 of 15 ranked cited claims (57 in-text markers from 42 bibliography entries); 6 cited works could not be identified, 3 had no retrievable text, 0 model quotes failed verbatim verification, 0 were topically unrelated to the retrieved text.","RL002 candidate ranking (why the top 15 were chosen): [22] [introduction, names an artefact (GPQA), title/sentence overlap near zero, no DOI/arXiv id]; [10] [introduction, names an artefact (Z3), title/sentence overlap near zero, unusable title (identity fragile)]; [11] [introduction, absolutist wording, no DOI/arXiv id]; [23] [introduction, names an artefact (DeepSeek-Prover), title/sentence overlap near zero]; [15] [introduction, names an artefact (MATH), title/sentence overlap near zero]; [9] [introduction, names an artefact (GSM8K)]; [11] [introduction, title/sentence overlap near zero, no DOI/arXiv id]; [3] [introduction, title/sentence overlap near zero, no DOI/arXiv id]","RL002 label distribution over 6 classified citations: PARTIALLY_SUPPORTED=2, SUPPORTED=4","RL002 base-rate self-check: not tripped (0/6 = 0% NOT_SUPPORTED, threshold 40%).","RL002 attribution check (case B): 14 candidates name an artefact, 10 of them made the top-N and were checked against their cited source","RL002: 2 citations skipped because the sentence reports this paper's own results (the citation there is a comparison pointer, not evidence for the sentence)","RL002: 1 markers skipped because the claim is jointly attributed to several works","RL002: 1 attributions dropped as family variants (the cited work is an adjacent version in the same family, e.g. 'DeepSeek-Prover' against DeepSeek-Prover-V2) -- not cleared, just not worth an author's time","RL002: 4 duplicate candidates dropped (same reference and claim, or the same artefact attributed twice)","RL002: 6 cited works unresolvable (first 3: [{\"key\": \"[10]\", \"title\": \"Z3: An efficient smt solver\", \"why\": \"bibliography title unusable for identity verification\"}, {\"key\": \"[11]\", \"title\": \"The lean theorem prover (system description)\", \"why\": \"no work record matched the bibliography title\"}, {\"key\": \"[11]\", \"title\": \"The lean theorem prover (system description)\", \"why\": \"no work record matched the bibliography title\"}])","RL003: 3 queries -> 157 unique works (arXiv search 107, category listings 0, scholarly graph 50 [crossref 50], 0 graph works matched to an arXiv id); source errors during retrieval: arXiv 0, graph 0","RL003: parsed the reference list of 5/11 comparable papers (6 unreadable) — that is the PeerUsage denominator","RL003: enriched 2 of 2 candidates with their own abstract (0 unavailable, 0 over budget); 0 dropped as published after this paper","RL003: scholarly graph for this run = crossref","RL003 funnel (418 candidates): already_used_by_the_paper -4, cited_only_from_related_work -12, is_a_dataset -2, is_a_metric -2, peer_usage_below_quorum -122, survey_or_artifact -91, title_names_no_method -183 || kept: citation_context_unknown +35 || survived-cheap-gates 2 -> with-abstract 2 -> comparable 2 -> above-threshold-0.65 0","RL003 candidate: 'Language models are few-shot learners' score 0.451 (T 0.00 D 1.00 M 0.33 P 0.60 R 0.29; 3/5 peers cite it) -> not reported","RL003 candidate: 'Let’s verify step by step' score 0.432 (T 0.00 D 1.00 M 0.33 P 0.40 R 0.71; 2/5 peers cite it) -> not reported","RL003: 2 comparable candidates all scored below 0.65 — nothing to report for this paper","RL004 funnel: components=11 contribution_backed=1 candidates=1 ablations_found=6 matched_by_ablation=0 unmatched=1 experiments=8","RL004 component M1 'Feasibility Screening': covered (filtered earlier)","RL004 component M2 'Executable Formalization': unmatched","RL004 component M3 'Proof-level Verification': excluded:stage-of-a-larger-claimed-component","RL004 component M4 'conservative all-pass policy': covered (filtered earlier)","RL004 component M5 'Target-answer matching after Lean verification': covered (filtered earlier)","RL004 component M6 'Literal answer extraction': excluded:not-a-claimed-contribution","RL004 component M7 'Final-answer checking': excluded:not-a-claimed-contribution","RL004 component M8 'rejection sampling procedure': excluded:not-a-claimed-contribution","RL004 component M9 'Goedel-Formalizer-V2-8B': excluded:not-a-claimed-contribution","RL004 component M10 'Goedel-Prover-V2-8B': covered (filtered earlier)","RL004 component M11 'Qwen3-MAX': covered (filtered earlier)","RL004 rank M2 'Executable Formalization': score=4 [referenced by a numbered contribution +3, substantive description (len=192) +1] confidence=0.75 -> emitted; desc='[kind=mechanism] Converts rewritten instances that pass feasibility screening into machine…'","RL004 funnel: ranked=1 emitted=1 suppressed_by_cap=0 dropped_unverified_quote=0","RL005: repository read, but the paper states no comparable hyperparameter"],"missing_core_rules":[],"seconds":38.49,"llm":{"calls":0,"cache_hits":8,"errors":0,"prompt_chars":0},"sources":{"arxiv":{"requests":2,"errors":0,"cache_hits":45,"available":1},"openalex":{"requests":1,"errors":0,"cache_hits":0,"available":0,"unavailable_reason":"OpenAlex free daily budget exhausted (resets midnight UTC)"},"crossref":{"requests":0,"errors":0,"cache_hits":15,"available":1},"s2":{"requests":0,"errors":0,"cache_hits":0,"available":1},"short_circuited":["crossref","openalex","s2"]},"cache":{"hits":68,"misses":3}},"compile_warnings":["references: the reference list carries no entry numbers; citation keys are enumeration order [1]..[N], not labels printed in the paper, so a key may not match the [N] used in the body","semantic extraction: dropped 6 items whose quote was not found in the paper"]}