REVIEW 4 major objections 6 minor 5 cited by
Mathesis: Towards Formal Theorem Proving from Natural Languages
T0 review · 4 major / 6 minor · reviewed 2026-08-07 · deepseek-v4-flash
Pith's one-line read This paper claims that end-to-end theorem proving from natural language becomes practical when the formalization step is trained with both syntactic and semantic feedback, and it reports 64.3% accuracy on a standard competition-level…
desk verdict Valuable benchmark and a serious end-to-end pipeline, but the headline accuracy numbers need better-defined evaluation before they'll stand up in peer review. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The load-bearing component is Mathesis-Autoformalizer, a translator trained with Group Relative Policy Optimization under a composite reward $R_{sem} + R_{ver}$, where $R_{sem}$ is a binary semantic-equivalence reward from an LLM judge and $R_{ver}$ is a binary Lean-verification reward. A second stage, Hierarchical Preference Optimization, applies Direct Preference Optimization to pairs of formalizations ranked by downstream proof success. The validation stage uses LeanScorer, which decomposes the informal problem into subtasks, rates each formalized subtask as Perfectly Match, Minor Inconsistency, or Major Inconsistency, and aggregates the ratings with a Sugeno fuzzy integral whose measure vetoes any Major Inconsistency and progressively penalizes multiple Minor Inconsistencies. The prover, Mathesis-Prover, is trained by expert iteration on verified proofs from open datasets, using a prior 7B prover as its starting point. The paper also introduces Gaokao-Formal, 488 exam problems with parallel English and human-verified Lean statements, which serves as both a training signal and an evaluation set.
What would settle it
Take the autoformalizer's generated Lean statements for a random sample of the 488 Gaokao-Formal problems, have human experts classify each statement as faithful or unfaithful to the informal text, then recompute the semantically correct formalization rate and the end-to-end pass@32 using only the human-verified faithful statements; if the corrected rates fall well below 71% and 18%, the semantic judge is passing unfaithful statements and the reported results overstate the system's real ability to solve the informal problems.
Extended reading notes
Core claim
On the paper's own terms, the central discovery is that end-to-end theorem proving from natural language becomes practical when the autoformalizer is trained with a reinforcement learning signal combining two rewards: a Lean compiler check that the generated statement is syntactically valid, and an LLM-judge check that the statement preserves the informal problem's semantics. Adding a second training stage, called Hierarchical Preference Optimization, uses whether downstream proofs succeed to preference-rank formalizations, teaching the autoformalizer to produce statements that provers can actually prove rather than statements that merely compile. With the trained autoformalizer filtering candidates through the new LeanScorer evaluation and a prover trained by expert iteration, the system attains 64.3% on the standard competition-level test set at pass@32 and 18.0% on the new Gaokao-Formal benchmark, and its autoformalizer alone raises the rate of semantically faithful formalizations on that benchmark from 49% to 71% at six samples. The authors also note that model-created formalizations sometimes outperform human-written ones on the new benchmark, which they attribute to differences in formalization style and to residual false positives in the semantic filter.
Load-bearing premise
The whole incentive system assumes that the LLM judge used in the semantic reward and in LeanScorer correctly decides whether a formal statement says what the natural-language problem says; if that judgment is biased, the training rewards could reinforce unfaithful formalizations and the reported accuracy would be inflated even though every proof is Lean-checked.
Editorial extensions
If this is right
- If the central claim is correct, the formalization bottleneck relaxes: a user can submit a prose problem and receive a machine-checked Lean proof without writing the formal statement by hand.
- The ablation numbers imply that autoformalization quality, not proof search, is the dominant lever on the harder benchmark: improving the autoformalizer nearly doubles end-to-end accuracy on Gaokao-Formal, whereas improving the prover adds about 6 percentage points.
- The same pipeline can be pointed at problem types such as geometry, combinatorics, and word problems that existing formalization benchmarks downplay, potentially expanding the formal library with newly formalized exam problems.
- The Hierarchical Preference Optimization stage offers a general recipe for aligning a generator with a downstream verifier: first reward local correctness, then prefer outputs that make the downstream proof search succeed.
Reading between the lines
- A testable extension would be to run the same reinforcement-learning-with-semantic-reward recipe with a different semantic judge or with human-labelled preferences in the loop; if the end-to-end scores drop sharply when the judge is replaced, that would confirm the gains come from the reward signal rather than from the underlying model.
- Because the semantic judge is itself an LLM, the 18.0% end-to-end number is best read as a ceiling conditional on the judge's fidelity; auditing the judge on a standard formal-competition benchmark where human formalizations already exist would quantify that ceiling.
- The method suggests a path for other formalization-heavy tasks, such as turning natural-language algorithm descriptions into executable verified code, where the same composite reward of compiler check plus semantic fidelity and the downstream-preference stage could apply.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper presents Mathesis, an end-to-end theorem-proving pipeline that takes natural language problem statements, formalizes them into Lean 4 via a new autoformalizer (Mathesis-Autoformalizer) trained with GRPO and a hierarchical preference optimization (HPO) stage, scores candidate formalizations with a new LeanScorer based on LLM subtask evaluation and Sugeno fuzzy integral, and then proves the selected statement with a new Mathesis-Prover. The paper also introduces Gaokao-Formal, a benchmark of 488 problems from the Chinese Gaokao exams with parallel English statements and human-verified Lean formalizations. The headline claims are 64.3% accuracy on MiniF2F-test at pass@32 and 18.0% on Gaokao-Formal, surpassing all compared combinations of existing autoformalizers and provers, and a 22% absolute improvement in autoformalization pass rate over the Kimina baseline.
Significance. If the reported results are robust, the paper makes a useful and timely contribution: Gaokao-Formal is a challenging benchmark that includes geometry and combinatorics, the autoformalization RL training is a new direction, and LeanScorer is a more nuanced evaluation method than binary compilation. The pipeline's use of Lean verification for proofs is a methodological strength, and the paper honestly discusses problematic edge cases. However, the headline empirical claims rest on a semantic-evaluation loop that is not yet convincingly validated, and the current evidence does not fully exclude co-adaptation between the autoformalizer and prover.
major comments (4)
- [§5.4 (End-to-End Performance)] The end-to-end accuracy metric is not well-defined because the paper excludes proofs ending in `apply?` and statements concluding with `: True := by sorry` from the success metrics, but it provides no counts, no automated detection criteria, and no sensitivity analysis. Since these artifacts are trivially provable for a subset of problems, even a few dozen exclusions can shift the reported 64.3%/18.0% numbers by several points. Please report exact exclusion counts per model and benchmark, define objective rules (e.g., any proof whose last tactic is `apply?` or any theorem whose statement is syntactically `True`), and present accuracy both with and without these exclusions.
- [§3.1.2, §3.2, §5.4] The end-to-end gains may partly reflect co-adaptation between the autoformalizer and the prover rather than an improvement in semantic fidelity. The HPO stage derives preferences from the downstream prover's success, and both the GRPO reward in Eq. (1) and the LeanScorer evaluation in Eq. (3) rely on the same LLM judge (DeepSeek-V3). The observation in §5.4 that autoformalized statements are proved more often than human-written ones is consistent with the autoformalizer learning to produce statements that are easy for the prover rather than faithful to the informal problem. Please add a human evaluation on a sample of successful end-to-end cases to verify that the formal statements actually capture the informal problems, and report the results separately for human-written and autoformalized statements.
- [§5.4, Table 5] The headline results are reported without error bars or statistical significance. The improvement of the best system (64.3%) over the second-best (63.9%) is 0.4 percentage points at pass@32, which is within the expected sampling noise for stochastic proof search. Please run multiple independent evaluations (or at least bootstrap confidence intervals) for all configurations in Table 5 and adjust the claims of superiority accordingly.
- [§B.1, Eq. (4)] The formula for success rate@k is mathematically incorrect as written: for C ~ Binomial(k,p), E[1 − (1 − C/k)^k] is not equal to 1 − (1−p)^k, and the expression mixes the actual success indicator with a plug-in estimator. Please correct the derivation and clarify how the numbers in Table 4 were computed (i.e., whether they are the empirical pass@k or the plug-in estimator).
minor comments (6)
- [Table 3] The row for LLM-as-a-Judge prints '731000.85', which appears to be a formatting error; the intended values are presumably 73, 100, 0.85.
- [§5.4] The text '11.2% improvement (7.2% to 18.4%)' does not match Table 5, where the corresponding values are 7.2% to 18.0%; please reconcile the numbers.
- [Abstract and §1] The claims 'first end-to-end theorem proving pipeline' and 'first autoformalizer using RL' are too strong without a more exhaustive related-work discussion; please qualify them with a precise scope (e.g., 'to our knowledge, first for Lean with GRPO').
- [§1 and §5.1] The paper states 'We release Mathesis-Autoformalizer' but no URL or artifact is provided; for reproducibility, please include release links or describe how to obtain the models and data.
- [§3.2] The Sugeno fuzzy measure constants (0.2 and 0.1 penalties) and the threshold α=0.6 are free parameters; a sensitivity analysis would strengthen the claim that LeanScorer is robust.
- [Appendix B.2] The example proof for `apply?` is displayed with a 'This is a placeholder' comment and seems incomplete; please provide the complete Lean code that actually compiles, to support the assertion that it passes the verifier.
Circularity Check
The end-to-end success metric is gated by the same LLM semantic judge used as the GRPO training reward and by the same prover-success signal used in HPO training, so the headline 64.3%/18.0% figures partly measure the training objectives; post-hoc 'apply?' and ': True' exclusions leave the metric under-specified.
-
fitted input called prediction
[§3.1.1 Eq. (1); §3.2 LeanScorer; §5.1–5.2 (DeepSeek-V3 judge)]
"Semantic Equivalence Reward (Rsem) This binary reward assesses whether oi preserves the semantic meaning of x, determined by an auxiliary LLM judge (J sem). Rsem(x, oi) = 1 if J sem(x, oi) judges "Appropriate", 0 otherwise. (1) ... All the LLM roles utilize Deepseek-V3 with prompts in Appendix B.5."
The GRPO reward that trains Mathesis-Autoformalizer is an LLM judge's approval of formalization semantics (Eq. 1). The reported success criteria are defined by the same class of LLM judgment: LC+LSC (Table 4) requires passing LeanScorer, an LLM-based semantic evaluator, and the end-to-end pipeline forwards the statement with 'the highest semantic assessment score' to the prover (§3). Section 5.2 states that all LLM roles use DeepSeek-V3, and no evidence is given that the evaluation judge differs from the training judge. The reported quality numbers therefore measure, in part, the very objective the model was fitted to: an LLM's 'Appropriate' verdict on NL-FL meaning preservation.
-
fitted input called prediction
[§3.1.2 DPO Training Data Generation; §5.4 End-to-End Methodology (Table 5)]
"Preferences are assigned based on the successful completion of the proof verified by Lean, yielding data tuple {x, yi w, zi w} for successful cases, and {x, yi l, zi l} for failed attempts. ... We measured the proving success rate (Accuracy) with a fixed search budget of 32."
The HPO stage trains Mathesis-Autoformalizer with DPO preferences assigned by whether the downstream prover completes a Lean-verified proof. The end-to-end results in Table 5 then measure the same quantity: the prover's success rate on formal statements generated by the autoformalizer. The reported HPO gains (e.g., 15.6% to 18.0% on Gaokao-Formal with Mathesis-Prover) thus partly quantify how well the formalizer was fitted to that very prover, rather than how faithful its statements are. The paper's own concession — 'residual false positives in the verification pipeline could partially account for this performance discrepancy' (§5.4) — describes exactly this confound.
1 more flagged steps
-
other
[§5.4 final paragraph; Appendix B.2–B.3]
"Additionally, we identified edge cases where autoformalizers and provers circumvented Lean syntactic checks. For instance, both Deepseek-prover-v2 and Mathesis-Prover occasionally produced proofs ending with 'apply?', which were technically verifiable but lacked substantive reasoning; these were excluded from success metrics. Similarly, Kimina-Autoformalizer and Mathesis-Autoformalizer generated statements concluding with ': True := by sorry' ... such formulations failed to capture the original problem's logical structure and were thus excluded from end-to-end evaluation."
The headline 64.3% (MiniF2F) and 18.0% (Gaokao-Formal) accuracies are well-defined only if the success criterion is fixed in advance. Instead, §5.4 states that proofs ending in 'apply?' and statements concluding ': True := by sorry' were excluded from success metrics after the fact, without exclusion counts, explicit detection criteria, or sensitivity analysis. Because the numerator and denominator of the reported accuracy are defined only over the residual set, the metric's definition is retrofitted to the outputs it excludes; even a few such cases can move pass@32 by several points.
full rationale
The strongest claims — 64.3% end-to-end accuracy on MiniF2F, 18.0% on Gaokao-Formal, and autoformalizers that 'occasionally surpassed human-written formalizations' — acquire their numbers through a closed loop. GRPO fits the autoformalizer to an LLM semantic judge (Eq. 1); LeanScorer, the gate that defines reported success, is the same class of LLM judgment (all LLM roles use DeepSeek-V3, §5.2); HPO fits the formalizer to prover success (§3.1.2); and end-to-end accuracy is measured as prover success on the judge-approved statement (§5.4). The measured success conditions are thus the training objectives, with the Lean kernel providing the only fully external verification. This warrants 6 rather than 0–2 per pattern 2 (fitted input called prediction) on both the semantic-judge loop and the HPO/prover loop. Several factors prevent a higher score: proofs are Lean-checked relative to the formal statements; LeanScorer was anchored to human labels at 0.92 F1 (Table 3); Mathesis-HPO statements also improve three other provers (Table 5), so the HPO gain is not purely self-fit; and the F2F rows on human-written statements (up to 69.2% on MiniF2F) independently validate the prover. No load-bearing self-citation chain appears: references [18] and [19] overlap with co-authors but are not load-bearing for the central claims. The post-hoc 'apply?' and ': True' exclusions (§5.4, App. B.2–B.3) are a separate, acknowledged weakness that makes the headline metric under-specified; combined with the judge gate, this inflates the exact numbers but does not by itself constitute a deductive circle. A related non-circularity risk: training data curation uses 'our in-house Gaokao dataset' (§3.1.1), whose overlap with the 488-problem Gaokao-Formal test set is not quantified. Net: partial circularity of the central end-to-end claim; the reader's 6.0 is sustained by the paper's own equations and concessions.
Assumptions & free parameters
free parameters (3)
- LeanScorer decision threshold alpha =
0.6
- Sugeno fuzzy measure constants =
0.1 per Minor Inconsistency, 0.2 for two or more; f(A)=1, f(B)=0.5, f(C)=0
- Semantic reward weighting =
R_sem + R_ver with both binary
assumptions (5)
- domain assumption The auxiliary LLM judge J_sem in equation (1) correctly distinguishes appropriate from inappropriate formalizations.
- domain assumption LeanScorer's LLM subtask ratings and Sugeno fuzzy aggregation approximate human judgment of formalization fidelity.
- domain assumption The human-verified Lean statements in Gaokao-Formal are correct translations of the original Gaokao problems.
- domain assumption A fixed pass@32 search budget is a fair comparison protocol across all provers and autoformalizers.
- domain assumption Prover success on a generated formal statement is a meaningful proxy for solving the original natural-language problem.
Cite this review
Pith. "Pith review of Mathesis: Towards Formal Theorem Proving from Natural Languages." pith.science (2026). https://pith.science/paper/HRUDOF67
@misc{pith2026250607047,
author = {Pith},
title = {Pith review of: Mathesis: Towards Formal Theorem Proving from Natural Languages},
year = {2026},
howpublished = {\url{https://pith.science/paper/HRUDOF67}},
note = {Machine review of arXiv:2506.07047}
}
read the original abstract
Recent advances in large language models show strong promise for formal reasoning. However, most LLM-based theorem provers have long been constrained by the need for expert-written formal statements as inputs, limiting their applicability to real-world problems expressed in natural language. We tackle this gap with Mathesis, the first end-to-end theorem proving pipeline processing informal problem statements. It contributes Mathesis-Autoformalizer, the first autoformalizer using reinforcement learning to enhance the formalization ability of natural language problems, aided by our novel LeanScorer framework for nuanced formalization quality assessment. It also proposes a Mathesis-Prover, which generates formal proofs from the formalized statements. To evaluate the real-world applicability of end-to-end formal theorem proving, we introduce Gaokao-Formal, a benchmark of 488 complex problems from China's national college entrance exam. Our approach is carefully designed, with a thorough study of each component. Experiments demonstrate Mathesis's effectiveness, with the autoformalizer outperforming the best baseline by 22% in pass-rate on Gaokao-Formal. The full system surpasses other model combinations, achieving 64% accuracy on MiniF2F with pass@32 and a state-of-the-art 18% on Gaokao-Formal.
Figures
Figures from the paper (3 more)
Forward citations
Cited by 5 Pith papers
-
FormalRx: Rectify and eXamine Semantic Failures in Autoformalization
FormalRx diagnoses Lean autoformalization failures with a 28-category SCI taxonomy and an 8B model that jointly predicts alignment, error type, location, and correction.
-
Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph
A graph-of-thought agent with retrieval and a term-grounded semantic checker auto-formalizes research-level math statements in Lean, hitting 68.5% on ProofNet and 6/14 homological conjectures where baselines score 0.
-
Integrating Rules and Semantics for LLM-Based C-to-Rust Translation
IRENE combines rule-based retrieval, structured summarization, and compiler feedback to improve LLM-based C-to-Rust translation accuracy and safety.
-
Advocate for Complete Benchmarks for Formal Reasoning with Formal/Informal Statements and Formal/Informal Proofs
The paper advocates complete four-part benchmarks (formal/informal statements and proofs) for formal reasoning and reports that a published 97% autoformalization accuracy is actually 67% on expert review.
-
HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs
Interleaving LLM reasoning with Lean4 verification of individual steps improves math-problem accuracy and cuts token budgets versus reward-model methods.
Reference graph
Works this paper leans on
-
[1]
Formal mathematical reasoning: A new frontier in AI
Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. Formal mathematical reasoning: A new frontier in AI. InProceedings of the International Conference on Machine Learning, 2025
work page 2025
-
[2]
The mathlib Community. The lean mathematical library. InProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, POPL ’20. ACM, January 2020
work page 2020
-
[3]
Springer, 1994
Lawrence C Paulson.Isabelle: A generic theorem prover. Springer, 1994
1994
-
[4]
The coq proof assistant a tutorial
Gérard Huet, Gilles Kahn, and Christine Paulin-Mohring. The coq proof assistant a tutorial. Rapport Technique, 178:113, 1997
1997
-
[5]
ZZ Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, et al. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition.arXiv preprint arXiv:2504.21801, 2025
arXiv 2025
-
[6]
Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, et al. Kimina-prover preview: Towards large formal reasoning models with reinforcement learning.arXiv preprint arXiv:2504.11354, 2025
arXiv 2025
-
[7]
Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, et al. Goedel-prover: A frontier model for open-source automated theorem proving.arXiv preprint arXiv:2502.07640, 2025
arXiv 2025
-
[8]
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: a cross-system benchmark for formal olympiad-level mathematics.arXiv preprint arXiv:2109.00110, 2021
arXiv 2021
Show all 61 references
-
[9]
Proofnet: Autoformalizing and formally proving undergraduate-level mathematics.arXiv preprint arXiv:2302.12433, 2023
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics.arXiv preprint arXiv:2302.12433, 2023
2023 arXiv
-
[10]
Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition.arXiv preprint arXiv:2407.11214, 2024
George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri. Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition.arXiv preprint arXiv:2407.11214, 2024
2024 arXiv
-
[11]
Herald: A natural language annotated lean 4 dataset.arXiv preprint arXiv:2410.10878, 2024
Guoxiong Gao, Yutong Wang, Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu, and Bin Dong. Herald: A natural language annotated lean 4 dataset.arXiv preprint arXiv:2410.10878, 2024
2024 arXiv
-
[12]
Numinamath: The largest public dataset in ai4maths with 860k pairs of competition math problems and solutions.Hugging Face repository, 13:9, 2024
Jia Li, Edward Beeching, Lewis Tunstall, Ben Lipkin, Roman Soletskyi, Shengyi Huang, Kashif Rasul, Longhui Yu, Albert Q Jiang, Ziju Shen, et al. Numinamath: The largest public dataset in ai4maths with 860k pairs of competition math problems and solutions.Hugging Face repositor...
2024
-
[13]
Multilingual mathematical autoformalization
Albert Q Jiang, Wenda Li, and Mateja Jamnik. Multilingual mathematical autoformalization. arXiv preprint arXiv:2311.03755, 2023
2023 arXiv
-
[14]
Atlas: Autoformalizing theorems through lifting, augmentation, and synthesis of data
Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, Yunqi Liu, Yu Chen, Yuntian Liu, Yang Jiao, and Tao Luo. Atlas: Autoformalizing theorems through lifting, augmentation, and synthesis of data. arXiv preprint arXiv:2502.05567, 2025
2025
-
[15]
Mps-prover: Advancing stepwise theorem proving by multi-perspective search and data curation
Zhenwen Liang, Linfeng Song, Yang Li, Tao Yang, Feng Zhang, Haitao Mi, and Dong Yu. Mps-prover: Advancing stepwise theorem proving by multi-perspective search and data curation. arXiv preprint arXiv:2505.10962, 2025
2025 arXiv
-
[16]
Bfs-prover: Scalable best-first tree search for llm-based automatic theorem proving
Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Kai Shen. Bfs-prover: Scalable best-first tree search for llm-based automatic theorem proving. arXiv preprint arXiv:2502.03438, 2025
2025
-
[17]
Hun- yuanprover: A scalable data synthesis framework and guided tree search for automated theorem proving.arXiv preprint arXiv:2412.20735, 2024
Yang Li, Dong Du, Linfeng Song, Chen Li, Weikang Wang, Tao Yang, and Haitao Mi. Hun- yuanprover: A scalable data synthesis framework and guided tree search for automated theorem proving.arXiv preprint arXiv:2412.20735, 2024. 13
2024 arXiv
-
[18]
Efficient neural theorem proving via fine-grained proof structure analysis.arXiv preprint arXiv:2501.18310, 2025
Haoxiong Liu, Jiacheng Sun, Zhenguo Li, and Andrew C Yao. Efficient neural theorem proving via fine-grained proof structure analysis.arXiv preprint arXiv:2501.18310, 2025
2025 arXiv
-
[19]
Carts: Advancing neural theorem proving with diversified tactic calibration and bias- resistant tree search
Xiao-Wen Yang, Zhi Zhou, Haiming Wang, Aoxue Li, Wen-Da Wei, Hui Jin, Zhenguo Li, and Yu-Feng Li. Carts: Advancing neural theorem proving with diversified tactic calibration and bias- resistant tree search. InThe Thirteenth International Conference on Learning Representations, 2025
2025
-
[20]
Decomposing the enigma: Subgoal-based demonstration learning for formal theorem proving.arXiv preprint arXiv:2305.16366, 2023
Xueliang Zhao, Wenda Li, and Lingpeng Kong. Decomposing the enigma: Subgoal-based demonstration learning for formal theorem proving.arXiv preprint arXiv:2305.16366, 2023
2023 arXiv
-
[21]
Lego-prover: Neural theorem proving with growing libraries.arXiv preprint arXiv:2310.00656, 2023
Haiming Wang, Huajian Xin, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, et al. Lego-prover: Neural theorem proving with growing libraries.arXiv preprint arXiv:2310.00656, 2023
-
[22]
Draft, sketch, and prove: Guiding formal theorem provers with informal proofs.arXiv preprint arXiv:2210.12283, 2022
Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs.arXiv preprint arXiv:2210.12283, 2022
-
[23]
Deepseek-prover-v1
Huajian Xin, ZZ Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, et al. Deepseek-prover-v1. 5: Harnessing proof assistant feed- back for reinforcement learning and monte-carlo tree search.arXiv preprint arXiv:2408.08152, 2024
2024 arXiv
-
[24]
Autoformalization with large language models.Advances in Neural Information Processing Systems, 35:32353–32368, 2022
Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models.Advances in Neural Information Processing Systems, 35:32353–32368, 2022
2022
-
[25]
The Claude 3 model family: Opus, Sonnet, Haiku
Anthropic. The Claude 3 model family: Opus, Sonnet, Haiku. Model Card, March 2024
2024
-
[26]
DeepSeek-R1: Incentivizing reasoning capability in LLMs via reinforcement learning, 2025
DeepSeek-AI and Anonymous Contributors. DeepSeek-R1: Incentivizing reasoning capability in LLMs via reinforcement learning, 2025
2025
-
[27]
Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Xiao Bi, Haowei Zhang, Mingchuan Zhang, Y .K. Li, Y . Wu, and Daya Guo. Deepseekmath: Pushing the limits of mathematical reasoning in open language models, 2024
2024
-
[28]
Bertopic: Neural topic modeling with a class-based tf-idf procedure
Maarten Grootendorst. Bertopic: Neural topic modeling with a class-based tf-idf procedure. arXiv preprint arXiv:2203.05794, 2022
2022 arXiv
-
[29]
Lean workbook: A large-scale lean problem set formalized from natural language math problems.arXiv preprint arXiv:2406.03847, 2024
Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. Lean workbook: A large-scale lean problem set formalized from natural language math problems.arXiv preprint arXiv:2406.03847, 2024
2024 arXiv
-
[30]
Direct preference optimization: Your language model is secretly a reward model
Rafael Rafailov, Archit Sharma, Eric Mitchell, Christopher D Manning, Stefano Ermon, and Chelsea Finn. Direct preference optimization: Your language model is secretly a reward model. Advances in Neural Information Processing Systems, 36:53728–53741, 2023
2023
-
[31]
Training language models to follow instructions with human feedback.Advances in neural information processing systems, 35:27730–27744, 2022
Long Ouyang, Jeffrey Wu, Xu Jiang, Diogo Almeida, Carroll Wainwright, Pamela Mishkin, Chong Zhang, Sandhini Agarwal, Katarina Slama, Alex Ray, et al. Training language models to follow instructions with human feedback.Advances in neural information processing systems, 35:27730...
2022
-
[32]
Enhancing llm reasoning with iterative dpo: A comprehensive empirical investigation.arXiv preprint arXiv:2503.12854, 2025
Songjun Tu, Jiahao Lin, Xiangyu Tian, Qichao Zhang, Linjing Li, Yuqian Fu, Nan Xu, Wei He, Xiangyuan Lan, Dongmei Jiang, et al. Enhancing llm reasoning with iterative dpo: A comprehensive empirical investigation.arXiv preprint arXiv:2503.12854, 2025
2025 arXiv
-
[33]
Self-training with direct preference optimization improves chain-of-thought reasoning.arXiv preprint arXiv:2407.18248, 2024
Tianduo Wang, Shichen Li, and Wei Lu. Self-training with direct preference optimization improves chain-of-thought reasoning.arXiv preprint arXiv:2407.18248, 2024
2024 arXiv
-
[34]
Pre-dpo: Improving data utilization in direct preference optimization using a guiding reference model.arXiv preprint arXiv:2504.15843, 2025
Junshu Pan, Wei Shen, Shulin Huang, Qiji Zhou, and Yue Zhang. Pre-dpo: Improving data utilization in direct preference optimization using a guiding reference model.arXiv preprint arXiv:2504.15843, 2025. 14
2025
-
[35]
Theory of fuzzy integrals and its applications.Doctoral Thesis, Tokyo Institute of Technology, 1974
Michio Sugeno. Theory of fuzzy integrals and its applications.Doctoral Thesis, Tokyo Institute of Technology, 1974
1974
-
[36]
Application of the sugeno integral in fuzzy rule-based classification.Applied Soft Computing, 167:112265, 2024
Jonata Wieczynski, Giancarlo Lucca, Eduardo Borges, Asier Urio-Larrea, Carlos López Molina, Humberto Bustince, and Graçaliz Dimuro. Application of the sugeno integral in fuzzy rule-based classification.Applied Soft Computing, 167:112265, 2024
2024
-
[37]
Qwen2.5-math technical report: Toward mathematical expert model via self-improvement.arXiv preprint arXiv:2409.12122, 2024
An Yang, Beichen Zhang, Binyuan Hui, Bofei Gao, Bowen Yu, Chengpeng Li, Dayiheng Liu, Jianhong Tu, Jingren Zhou, Junyang Lin, Keming Lu, Mingfeng Xue, Runji Lin, Tianyu Liu, Xingzhang Ren, and Zhenru Zhang. Qwen2.5-math technical report: Toward mathematical expert model via se...
2024 arXiv
-
[38]
Deepseek-v3 technical report, 2024
DeepSeek-AI. Deepseek-v3 technical report, 2024
2024
-
[39]
Kimi k1.5: Scaling reinforcement learning with LLMs, 2025
Kimi Authors. Kimi k1.5: Scaling reinforcement learning with LLMs, 2025
2025
-
[40]
Hu, Yelong Shen, Phillip Wallis, Zeyuan Allen-Zhu, Yuanzhi Li, Shean Wang, Lu Wang, and Weizhu Chen
Edward J. Hu, Yelong Shen, Phillip Wallis, Zeyuan Allen-Zhu, Yuanzhi Li, Shean Wang, Lu Wang, and Weizhu Chen. LoRA: Low-rank adaptation of large language models. In International Conference on Learning Representations (ICLR), 2022
2022
-
[41]
Decoupled weight decay regularization
Ilya Loshchilov and Frank Hutter. Decoupled weight decay regularization. InInternational Conference on Learning Representations (ICLR), 2019
2019
-
[42]
Thomas Wolf, Lysandre Debut, Victor Sanh, Julien Chaumond, Clement Delangue, Anthony Moi, Pierric Cistac, Tim Rault, Remi Louf, Morgan Funtowicz, Joe Davison, Sam Shleifer, Patrick von Platen, Clara Ma, Yacine Jernite, Julien Plu, Canwen Xu, Teven Le Scao, Sylvain Gugger, Mari...
2020
-
[43]
Trl: Transformer reinforcement learning.https://github.com/huggingface/trl, 2020-2024
Leandro von Werra, Lewis Schmid, Thomas Wolf, and Lewis Tunstall. Trl: Transformer reinforcement learning.https://github.com/huggingface/trl, 2020-2024
2020
-
[44]
Experiment tracking with weights and biases
Lukas Biewald. Experiment tracking with weights and biases. https://wandb.ai, 2020. Software available from wandb.com. 15 A Model Training Details A.1 Training Details forMathesis-Autoformalizer The training of ourMathesis-Autoformalizermodel, which employs Group Relative Poli...
2020
-
[45]
* 2 ^ (3 * k) := by 11 12intro h 13have h := h 14rw [Nat.dvd_iff_mod_eq_zero] at h 15have h : ( P k in Finset.range (n + 1), Nat.choose (2 * n + 1) (2 * k + 1) * 2 ^ (3 * k)) % 5̸=0 := by 16-- We will show that the sum modulo 5 is never 0 by examining the terms and their contr...
-
[46]
Start with "theorem" followed by a unique name or the provided ID if avail- able
-
[47]
Define the types of all variables (e.g., a :Rfor real numbers)
-
[48]
Use appropriate mathematical symbols and notation
-
[49]
:= by sorry
End with ":= by sorry" to indicate the proof will be completed later
-
[50]
Please evaluate whether the formal LEAN statement appropriately translates the natural language statement based on the following criteria
Your formalization must exactly capture the mathematical meaning of the statement Formal Lean 4 theorem: Prompt for Mathesis-Prover Complete the following Lean 4 code: ```lean4 {formal statement} Prompt for LLM Semantic Check You will receive a natural language math problem st...
-
[51]
Key Elements: The fundamental mathematical components, including variables, constants, operations, domain, and codomain are correctly represented in LEAN code
-
[52]
Mathematical Accuracy: The mathematical relationships and expressions should be interpreted consistently during translation
-
[53]
Structural Fidelity: The translation aligns closely with the original problem, maintaining its structure and purpose
-
[54]
opposite angles/sides
Comprehensiveness: All conditions, constraints, and objectives stated in the natural language statement are mathematically included in the LEAN translation. When doing evaluation, break down each problem statement into components, match the components, and evaluate their equiv...
-
[55]
- Lean: ‘(hq : 1 < q)’
**qis a natural number greater than 1**: - Math:q∈N, q >1. - Lean: ‘(hq : 1 < q)’. - Match:\box{Perfectly match}
-
[56]
- Lean: ‘(hn : 1 < n)’
**nis a natural number greater than 1**: - Math:n∈N, n >1. - Lean: ‘(hn : 1 < n)’. - Match:\box{Perfectly match}
-
[57]
- Lean: ‘(M : FinsetN:= Finset.range q)’
**SetM={0,1,2,· · ·, q−1}**: - Math:Mis explicitly defined as this set. - Lean: ‘(M : FinsetN:= Finset.range q)’. - Detailed interpretation: ‘Finset.range q‘ is ‘0, 1, ..., q - 1’. - Match:\box{Perfectly match}
-
[58]
- Lean: ‘A : Set N := {x | ∃ (x_vec : N→N ), (∀ i, x_vec i ∈ M) ∧ x = P i in Finset.range n, x_vec(i + 1) * q ^i}’
**SetAdefinition**: - Math:A={x|x= Pn i=1 xiqi−1, xi inM}. - Lean: ‘A : Set N := {x | ∃ (x_vec : N→N ), (∀ i, x_vec i ∈ M) ∧ x = P i in Finset.range n, x_vec(i + 1) * q ^i}’. - Detailed interpretation: In Lean, ‘x_vec’ is indexed from ‘1’ to ‘n’ (since ‘i + 1’ ranges from ‘1’ ...
-
[59]
- Lean: ‘s = P i in Finset.range n, a (i + 1) * q ^i’, ‘t = P i in Finset.range n, b (i + 1) * q ^i’, with ‘∀i, a i∈M’ and ‘∀i, b i∈M’
**s, t∈Awith specific expansions**: - Math:s= Pn i=1 aiqi−1,t= Pn i=1 biqi−1, witha i, bi ∈M. - Lean: ‘s = P i in Finset.range n, a (i + 1) * q ^i’, ‘t = P i in Finset.range n, b (i + 1) * q ^i’, with ‘∀i, a i∈M’ and ‘∀i, b i∈M’. - Detailed interpretation: The Lean version use...
-
[60]
- Lean: ‘(hab : a n < b n)’
**an < bn**: - Math:a n < bn. - Lean: ‘(hab : a n < b n)’. - Match:\box{Perfectly match}
-
[61]
- Lean: ‘s <= t’
**Conclusions < t**: - Math:s < t. - Lean: ‘s <= t’. - Match:\box{Major inconsistency}. ###Check for missing conditions / implicit conditions: - No missing conditions / implicit conditions - Match:\box{Perfectly match}. 21
Reviewed August 7, 2026 · model on record in the stance chip above.
Discussion (0). Sign in to comment.