{"id":"d018ecbb-94a9-470a-8530-635f9cbcf0ae","arxiv_id":"2507.11275","paper_version":1,"verdict":"REJECT","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"high","formal_verification":"none","parameter_count":3,"one_line_summary":"An LLM-based error-feedback pipeline produces FMC, a dataset of 3,922 Olympiad problems aligned with 9,787 Lean statements, claimed to be a challenging ATP benchmark.","lead":"The paper builds an automated pipeline that turns Olympiad math problems into Lean formal statements using large language models, then releases the resulting dataset of problems and formalizations. The dataset is offered as a benchmark for automated theorem provers, with the caveat that the pipeline's own validation is demonstrably imperfect.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Semantic-consistency filtering is not reliable enough to certify dataset quality: the paper's own Appendix A/B.3 and Table 4 document incorrect formalizations passing the checker, so the 81.74% semantic consistency and 64.46% quality figures do not establish a trustworthy benchmark.","rationale":"I read the paper in good faith as making two separable contributions: an automatic, training-free autoformalization pipeline with error feedback, and a curated benchmark dataset. The benchmark claim is the central claim and it requires that each Lean statement faithfully represents its paired natural-language problem. That requirement is not established. Formal verification is weak here because every statement ends in 'by sorry', so Lean only confirms the statement is well-typed, not that it matches the intended mathematics. The backtranslation plus consistency-check step is therefore the only semantic filter, and the paper's own evidence shows this filter admits incorrect formalizations: the geometry example in Section 4.2, the f(240) and candy-distribution examples in Appendix A, and the magician-cards example in Appendix B.3. Table 4 independently quantifies the inconsistency-checker's accuracy at 74.1% for DeepSeek-R1, which is far too low to support an 81.74% semantic-consistency claim in the absence of human validation. The 64.46% above-average quality rating is produced by an LLM with no reported human verification or agreement metric, so it cannot convert a noisy pipeline into a certified benchmark. A random-sample human audit would settle the question concretely; the repository availability makes such an audit feasible. This concern matches the reader's weakest assumption, and the resulting verdict should remain unchanged rather than being relaxed. I credit the authors for clearly documenting failure cases and for reporting the consistency checker's accuracy, but this documentation undermines rather than supports the benchmark-quality claim.","tokens_in":17448,"tokens_out":5208,"duration_ms":61097,"concrete_test":"Independently sample 100 entries at random from the released FMC dataset and have two human experts in formal mathematics classify each Lean statement for semantic equivalence to its paired natural-language problem, with a third expert adjudicating disagreements. Report the error rate with a 95% confidence interval; if the human-identified error rate exceeds about 5%, the 81.74%/64.46% quality claims and the benchmark-suitability conclusion fail. As a complementary check, run the released consistency-check prompt with DeepSeek-R1 on the Appendix A.2 f(240), A.1 candy-distribution, and B.3 magician statements and record whether the checker marks each as 'Same: true'; if it does, the checker demonstrably admits known-bad formalizations. The repository link in the paper makes these checks feasible.","verdict_should_be":"UNCHANGED","load_bearing_attack":"FMC's central claim is that 3,922 Olympiad-level natural-language problems are aligned with 9,787 Lean statements and form a high-quality benchmark; this depends on the DeepSeek-R1 consistency checker actually excluding semantically wrong formalizations. That dependence is load-bearing and the paper itself shows it fails. Section 4.2 (Fig. 2) gives a geometry formalization that passed both formal verification and consistency checks although the triangle constraints and the equality condition are missing. Appendix A.2 presents a formalization of 'Find f(240)' that passed the checks but asserts the wrong value f(240)=38808; A.1's candy-distribution formalization uses k(k+3)/2 instead of the correct triangular-number rule; and A.1's semiperimeter recursion only encodes two levels, not infinite iteration. Appendix B.3's magician-cards statement omits the distinct-pair condition and the counting goal, yet it appears in FMC. Since proofs are placeholders ('by sorry'), Lean verification only checks that statements typecheck; it provides no check of mathematical equivalence to the original problem. The checker's own reliability is quantified in Table 4: for DeepSeek-R1, accuracy is 74.1%, precision is 69.8%, and recall is 93.8% on an evaluation set, so roughly a quarter of its consistency decisions are wrong. The 81.74% consistency pass rate is therefore not a validated semantic-correctness rate, and the 64.46% quality rating is LLM-generated without reported human validation or inter-annotator agreement. The conclusion's acknowledgment that misjudgments still occur during consistency checks confirms the limitation. The benchmark-quality conclusion is unsupported by the evidence.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes an automatic, training-free autoformalization pipeline that translates natural-language Olympiad problems into Lean statements using LLMs with error feedback. The pipeline combines formal translation, Lean formal verification, backtranslation, and an LLM-based consistency check. Using this pipeline, the authors construct the FMC dataset, reported as 3,922 natural-language problems aligned with 9,787 Lean statements, and claim 81.74% semantic consistency and 64.46% above-average quality. They further study the formalization and consistency-check capabilities of DeepSeek-R1, GPT-4o-mini, and Claude 3.7 Sonnet, and benchmark three automated theorem provers on the dataset. The central claim is that FMC is a high-quality, Olympiad-level benchmark for automated theorem provers.","tokens_in":17849,"tokens_out":3581,"duration_ms":42844,"significance":"If the central claims were established, the work would be useful: a large, automatically constructed Lean dataset from competition problems could support training and evaluation of theorem provers. The paper has concrete strengths: the pipeline is fully automatic and training-free, the ablation studies on few-shot learning, error feedback, and sampling are informative, and the appendix is unusually transparent in documenting formalization failures. However, the load-bearing validation is not established. The paper's own appendix and Table 4 show that the consistency checker passes mathematically incorrect formalizations and has only 74.1% accuracy on the authors' evaluation set, so the measured 'semantic consistency' cannot be read as semantic correctness. The 64.46% quality figure is an LLM-generated rating of research interest, not of mathematical fidelity. Consequently, the dataset's value as a benchmark is not supported by the evidence presented.","major_comments":[{"comment":"The reported 81.74% consistency-check pass rate is presented as the pipeline's 'formalization accuracy,' but the consistency checker has only 74.1% accuracy and 69.8% precision on the paper's own evaluation set (Table 4). The paper's Appendix A and B.3 give multiple statements that passed both formal verification and the consistency check yet are mathematically wrong. Since the proofs are placeholders ('by sorry'), Lean verification only confirms that the statements typecheck and does not establish mathematical truth. The 81.74% figure therefore cannot be interpreted as a validated semantic-correctness rate, and it does not support the central claim that the dataset is reliable enough to be a benchmark.","section":"§4.3, Table 1, Table 4"},{"comment":"The appendix documents examples that passed the pipeline but are mathematically incorrect. In §A.1, the candy-distribution formalization uses k*(k+3)/2 instead of the triangular-number pattern k*(k+1)/2 and omits the condition that n must be a power of two; the semiperimeter example encodes only two recursion levels rather than infinite iteration. In §A.2, the formalization of 'Find f(240)' asserts the incorrect value f(240)=38808. In §B.3, the magician-cards statement omits the requirement that the two pairs of boxes be distinct and omits the counting goal entirely. These are not边缘 examples: they are the paper's own case studies of failures, and at least the §B.3 statement appears in the final dataset. This directly contradicts the claim that passing formal verification and consistency check indicates a correct formalization.","section":"§A.1, §A.2, §B.3"},{"comment":"The geometry example in Figure 2 is explicitly described as a failed formalization that nevertheless passed both formal verification and the consistency check: the triangle angle-sum constraint and the equality-condition goal are missing. Although geometry problems are later excluded from the dataset, this example demonstrates that the consistency checker cannot reliably detect omitted implicit conditions. Since many Olympiad problems rely on such implicit constraints, the failure is not confined to geometry, and it undermines the use of the consistency check as a quality filter.","section":"§4.2, Figure 2"},{"comment":"The quality assessment that yields 64.46% 'above average or higher' is performed by an LLM (DeepSeek-R1) using criteria such as research relevance, interdisciplinary potential, and innovativeness. No human validation, inter-annotator agreement, or error analysis is reported, and the criteria do not measure mathematical correctness or fidelity to the original problem. This rating therefore does not support the claim that the dataset is high-quality for automated theorem proving.","section":"§4.3, 'Dataset Construction and Evaluation'"},{"comment":"The benchmark experiments measure provers' success on the formal Lean statements in FMC. Because the formal statements have unproved bodies ('by sorry') and because the semantic alignment between the natural-language problems and the Lean statements is not reliable—as the appendix demonstrates—a prover's pass rate on FMC does not measure its ability to solve the original competition problems. The comparison with MiniF2F, ProofNet, and FormalMATH is therefore ambiguous, and the claim that FMC is 'competitive as a benchmark' is not supported.","section":"§5.5, Table 8"}],"minor_comments":[{"comment":"There are several typos and inconsistent spellings: 'Automformalization' in the title of §2.3, 'Olympaid' in §2.3, 'balances bwtween' in the conclusion, and 'it's' instead of 'its' in the introduction. The model name is spelled both 'Deepseek-R1' and 'DeepSeek-R1'; please standardize.","section":"Throughout"},{"comment":"For each case study in Appendix A, please state explicitly whether the shown formalization is included in the final FMC dataset or was excluded. This is important for interpreting the examples as evidence about the dataset itself.","section":"Appendix A"},{"comment":"The consistency-check prompt asks the model to determine whether two problems are the same in 'mathematical essence,' but the paper does not report any calibration or threshold analysis for this binary judgment. Adding a small human-labeled evaluation set with agreement rates would strengthen the reliability claims.","section":"§3.4"}],"recommendation":"reject","confidential_remarks":"The paper is transparent about the limitations of its pipeline, and the appendices are honest about failures. However, the central claim—that FMC is a high-quality benchmark, supported by 81.74% semantic consistency and 64.46% quality ratings—is directly undercut by the evidence the paper itself provides. The consistency checker is not reliable enough to certify semantic correctness, and the quality ratings are LLM-generated and do not measure mathematical fidelity. These are load-bearing issues that cannot be fixed by presentation changes within the current scope. A substantially revised version that narrows the claims to an autoformalization-pipeline study, adds human validation of a sample, and reports error rates on the final dataset could be reconsidered."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"First thing you should know: this paper is a real step forward for autoformalization engineering, but its central quality claim doesn't hold up. The FMC dataset (3,922 natural-language problems, 9,787 Lean statements) and the error-feedback pipeline are useful, and the authors are unusually candid about failures. But the paper's own appendix shows the consistency check passing mathematically wrong formalizations, so the 81.74% semantic consistency and 64.46% 'above-average' quality figures can't be taken at face value.\n\nWhat's actually new: the error-feedback loop — feeding both Lean error messages and consistency-check failures back into the translation prompt — is a simple and effective addition over Lean Workbook. The model comparison (DeepSeek-R1 vs GPT-4o-mini vs Claude 3.7) is thorough, and the cross-validation design (different models for formalization vs. checking) is thoughtful. The dataset is genuinely new and larger than FIMO for Olympiad problems. They ship code and data, which is a real plus.\n\nThe soft spot is load-bearing and the authors themselves supply the evidence. Appendix A.2 formalizes 'find f(240)' with an incorrect value; A.1's candy problem uses the wrong formula; B.3's magician-cards statement misses the distinct-pair condition and the counting goal. All of these passed both Lean typechecking and the DeepSeek-R1 consistency check. Table 4 gives that checker 74.1% accuracy and 69.8% precision, so about a quarter of its decisions are wrong. Since proofs are 'by sorry', Lean verification does nothing beyond typechecking. The quality ratings come from an LLM with no human validation or inter-annotator agreement, and the conclusion admits misjudgments occur. Geometry exclusion is a real bias but is disclosed.\n\nNone of this means the pipeline is worthless. As a challenge set for ATPs, FMC still has value — the benchmark results are informative. But the abstract's claim that it's a high-quality benchmark for theorem provers is stronger than the evidence supports.\n\nMy take: send it to review, but require a human-verified random sample (say 200–500 problems) with error rates reported, and temper the claims to match. The engineering is solid; the certification is not.","headline":"A useful autoformalization pipeline and a new Olympiad-scale Lean dataset, but the quality-certification claims don't survive the paper's own appendix.","tokens_in":18317,"tokens_out":2253,"would_cite":false,"duration_ms":24363,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"A fully automatic, training-free LLM pipeline with error feedback claims to formalize Olympiad-level problems into Lean at 81.74% semantic consistency, yielding a 3,922-problem benchmark that current theorem provers solve only 13–16% of…","keywords":["autoformalization","Lean 4","Olympiad mathematics","LLM pipeline","error feedback","benchmark dataset","automated theorem proving","semantic consistency"],"falsifier":"Take a random sample of roughly 100 entries from the released FMC dataset that passed both the syntax and consistency checks and have a mathematician with Lean experience judge whether each Lean statement expresses exactly the original problem's conditions and conclusion. If the human-verified rate falls well below 81.74%, or if the $f(240)$ and candy-distribution statements from Appendix A appear in the released data as passed entries, then the consistency filter demonstrably fails and the dataset-quality claim reduces to the raw translation pass rate.","tokens_in":17225,"feed_emoji":"🧮","tokens_out":10710,"duration_ms":109960,"temperature":0.7,"pith_summary":"The paper sets out to show that a fully automatic, training-free pipeline can convert natural-language mathematics competition problems into Lean formal statements at scale, producing a dataset that is both Olympiad-difficult and usable as a benchmark. The pipeline translates each problem with the DeepSeek-R1 model under few-shot prompting, checks the Lean statement with the Lean 4 REPL, translates it back to natural language, and asks the model whether the backtranslation matches the original; failed statements are retried with the error messages fed back into the prompt. On 4,798 preprocessed IMOmath problems it reports 93.39% syntactic validity and 81.74% semantic consistency, yielding FMC: 3,922 natural-language problems aligned with 9,787 Lean statements, of which 64.46% were rated at least above-average by an LLM quality judge. The payoff would be a cheap, repeatable route to competition-level formal data, replacing the expert hand-annotation that previously was required for hard problems. The paper also positions FMC as a theorem-prover benchmark: three automated provers solve only 13–16% of a random 1,000-statement sample, placing its difficulty between ProofNet and FormalMATH.","feed_headline":"3,922 Olympiad problems turned into a Lean benchmark","feed_subtitle":"An error-feedback pipeline hits 93% syntax and 82% semantic accuracy — and stumps today's theorem provers.","key_machinery":"The carrying mechanism is the four-stage autoformalization loop: formal translation of a natural-language problem into Lean by a few-shot LLM prompt; syntactic verification by the Lean 4 REPL (via the DeepSeek-Prover verifier); backtranslation of the Lean statement into natural language; and a consistency check in which an LLM compares the backtranslation against the original problem and must confirm identical conditions and goals. Any failure at the verification or consistency stage produces an error message that is inserted into a revised prompt, and the translation model retries once; this 'error feedback' loop is what the paper credits for the improvement over the Lean Workbook pipeline, along with a stronger base model. The named object is the FMC pipeline, and its load-bearing parts are the off-the-shelf DeepSeek-R1 model used for all three language roles and the REPL verifier that supplies structured, interpretable error text.","core_discovery":"On the paper's own terms, the discovery is that error feedback is what makes the translate–verify–backtranslate–check loop strong enough to formalize Olympiad-level problems without human annotation: feeding Lean's error messages and the consistency checker's rationale into a second translation attempt raised the overall pass rate, with the semantic-feedback retries contributing the larger gain (10.52% on the ablation subset, versus a negligible effect from syntax-error messages), and sampling each problem five times at temperature 1.0 raised formalization accuracy from 59.65% to 91.22% on the same subset. The authors therefore claim that the resulting dataset strikes a balance between scale and difficulty: the 3,922-problem FMC set with 9,787 Lean statements, of which 64.46% were judged to be at least above-average quality, derived from problems at IMO and national-Olympiad difficulty. They demonstrate the benchmark value by showing that three automated theorem provers reach intermediate pass rates on a 1,000-problem sample (16.4% for Kimina-Prover, 15.7% for Goedel-Prover, 13.0% for DeepSeek-Prover-V1.5-RL), between ProofNet and FormalMATH and well below their 50–63% on miniF2F.","pith_inferences":["The paper's own appendix evidence implies the real semantic error rate is higher than 81.74%: formally verified and consistency-checked statements include a wrong value for $f(240)$, a candy-distribution formula using $k(k+3)/2$ in place of the triangular numbers $\\frac{k(k+1)}{2}$, and a magician-card problem whose Lean text omits the distinct-pair condition. A human-annotated subsample, which th","Because the consistency judge is the same family of model that wrote the formalizations, the check may be biased toward agreement; downstream users should treat the 81.74% figure as a pipeline-internal estimate, not a certified accuracy.","A testable extension is per-domain consistency reporting: the authors' ablations and case studies suggest error modes cluster (recursion, 'find all' goals, combinatorics), so field-specific pass rates would make the benchmark far more informative than the aggregate number.","Since syntax-error feedback barely helped while semantic feedback helped a lot, a cheaper variant that skips the verifier-feedback step and retries only on semantic failures would likely match the full pipeline's accuracy at lower token cost; the paper's Table 6 numbers are consistent with that hypothesis."],"forward_implications":["Competition-level formal data can be produced cheaply and repeatedly: FMC required 161 million tokens and no fine-tuning, a cost profile that makes dataset reconstruction for new problem sources or languages feasible.","FMC gives theorem provers a difficulty plateau between ProofNet and FormalMATH (13–16% solve rates), one that separates provers that all succeed on miniF2F-class problems.","The cheap quality knobs are confirmed: few-shot examples, one error-feedback retry, and more samples per problem each measurably raise the pass rate, with per-problem sampling providing the largest gain.","Geometry is out of reach for this approach — the paper filters out all geometry problems because LLM formalizations omit implicit constraints and still pass both checks — so FMC covers algebra and number theory rather than the full Olympiad scope."],"supporting_citations":[{"why":"Supplies the base translate–verify–backtranslate–check pipeline that FMC improves with error feedback, and the direct baseline (62.5% syntactic, 17.5% semantic consistency) the paper claims to beat.","marker":"(Ying et al., 2024)"},{"why":"The off-the-shelf DeepSeek-R1 model used for translation, backtranslation, and consistency judging; the claim that no training is needed rests on this model's capabilities.","marker":"(DeepSeek-AI, 2025a)"},{"why":"Provides the Lean 4 REPL verifier whose structured error messages drive the error-feedback loop.","marker":"(Xin et al., 2024)"},{"why":"Source of the 6,980 official Olympiad problems that ground the dataset's difficulty and correctness claims.","marker":"(IMOmath, 2025)"},{"why":"FormalMATH is the comparison dataset that anchors FMC's difficulty placement in the theorem-prover benchmark (13.0–16.4% vs 10.2–16.5%).","marker":"(Yu et al., 2025)"},{"why":"miniF2F supplies the easier Olympiad-level reference point that highlights FMC's challenge (provers solve 50–63% there).","marker":"(Zheng et al., 2021)"},{"why":"The roughly 20% accuracy result for Euclidean-geometry autoformalization justifies the paper's decision to filter geometry problems out.","marker":"(Murphy et al., 2024)"}],"fun_headline_variants":["Error-feedback loop formalizes 3,922 Olympiad problems in Lean","Lean benchmark from 3,922 natural-language math problems","3,922-problem Lean benchmark stumps theorem provers","Feedback-driven pipeline builds 9,787-statement Lean dataset","Olympiad-level autoformalization: 3,922 problems via error feedback"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the LLM-based consistency check — backtranslating the Lean statement and judging whether it matches the original problem's conditions and goals — reliably rejects semantically wrong formalizations, yet the paper's own appendices show formally verified and consistency-checked statements that are mathematically wrong (a mistaken value for $f(240)$, a candy-distribution formula using $k(k+3)/2$ instead of triangular numbers, and a combinatorics statement missing a key condition).","fun_headline_variants_meta":{"raw":{"variants":["Error-feedback loop formalizes 3,922 Olympiad problems in Lean","Lean benchmark from 3,922 natural-language math problems","3,922-problem Lean benchmark stumps theorem provers","Feedback-driven pipeline builds 9,787-statement Lean dataset","Olympiad-level autoformalization: 3,922 problems via error feedback"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00092,"raw_usage":{"total_tokens":3969,"prompt_tokens":991,"completion_tokens":2978,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":607,"completion_tokens_details":{"reasoning_tokens":2887}},"tokens_in":607,"tokens_out":2978,"duration_ms":26799,"temperature":1.0,"reasoning_tokens":2887,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T17:11:01.748933+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a random sample of roughly 100 entries from the released FMC dataset that passed both the syntax and consistency checks and have a mathematician with Lean experience judge whether each Lean statement expresses exactly the original problem's conditions and conclusion. If the human-verified rate falls well below 81.74%, or if the $f(240)$ and candy-distribution statements from Appendix A appear in the released data as passed entries, then the consistency filter demonstrably fails and the dataset-quality claim reduces to the raw translation pass rate.","supporting_citations":[],"review_version":1}