---
title: "Mathesis — paper by Xuejun et al. (2025) — summary and ideas"
description: "Current LLM theorem provers for Lean 4 assume their input is already a… 0.92 F1 on Gaokao-Formal. 44 references, cited by 9 papers here."
authors: ["Yu Xuejun", "Jianyuan Zhong", "Zijin Feng", "Pengyi Zhai", "Roozbeh Yousefzadeh", "Wei Chong Ng", "Haoxiong Liu", "Ziyi Shou", "Jing Xiong", "Yudong Zhou", "Claudia Beth Ong", "Austen Jeremy Sugiarto", "Yaoxi Zhang", "Wai Ming Tai", "Huan Cao", "Dongcai Lu", "Jiacheng Sun", "Qiang Xu", "Shen Xin", "Zhenguo Li"]
year: 2025
venue: "arXiv:2506.07047"
source: "https://arxiv.org/abs/2506.07047"
doi: "10.48550/arxiv.2506.07047"
arxiv: "2506.07047"
licence: "CC BY 4.0 (arXiv)"
licence_url: "http://creativecommons.org/licenses/by/4.0/"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/xuejun-2025-mathesis-towards-formal-theorem-proving/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/xuejun-2025-mathesis-towards-formal-theorem-proving/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2025](https://md.research.elamur.ai/free/en/papers/2025/page/11/) / Mathesis: Towards Formal Theorem Proving from Natural Languages

# Mathesis: Towards Formal Theorem Proving from Natural Languages

**Authors:** Yu Xuejun, [Jianyuan Zhong](https://md.research.elamur.ai/free/en/authors/jianyuan-zhong/), [Zijin Feng](https://md.research.elamur.ai/free/en/authors/zijin-feng/), Pengyi Zhai, [Roozbeh Yousefzadeh](https://md.research.elamur.ai/free/en/authors/roozbeh-yousefzadeh/), Wei Chong Ng, [Haoxiong Liu](https://md.research.elamur.ai/free/en/authors/haoxiong-liu/), Ziyi Shou, [Jing Xiong](https://md.research.elamur.ai/free/en/authors/jing-xiong/), Yudong Zhou, Claudia Beth Ong, Austen Jeremy Sugiarto, Yaoxi Zhang, Wai Ming Tai, Huan Cao, Dongcai Lu, Jiacheng Sun, Qiang Xu, Shen Xin and [Zhenguo Li](https://md.research.elamur.ai/free/en/authors/zhenguo-li/) · **Year:** 2025 · **Venue:** arXiv:2506.07047 · **Licence:** [CC BY 4.0 (arXiv)](http://creativecommons.org/licenses/by/4.0/)

**Links:** [Publisher's page](https://arxiv.org/abs/2506.07047) · [PDF](https://arxiv.org/pdf/2506.07047) · [DOI 10.48550/arxiv.2506.07047](https://doi.org/10.48550/arxiv.2506.07047) · [arXiv 2506.07047](https://arxiv.org/abs/2506.07047) · [OpenAlex](https://openalex.org/W4417126526)

**Citations:** 0 citations (OpenAlex, 2026-10-14) · [9](https://md.research.elamur.ai/free/en/papers/xuejun-2025-mathesis-towards-formal-theorem-proving/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
Current LLM theorem provers for Lean 4 assume their input is already a formal statement written by an expert. Real problems, however, are stated in natural language. Mathesis targets the full chain from informal problem to verified proof. Its pipeline has three stages:
- **Autoformalization:** Mathesis-Autoformalizer drafts several Lean 4 candidates.
- **Validation:** the Lean compiler filters the candidates, and LeanScorer ranks the survivors by semantic fidelity.
- **Proving:** Mathesis-Prover attempts a proof of the top-ranked statement.

The autoformalizer is trained with online reinforcement learning (GRPO). Its reward combines compilation success and semantic correctness, and a Hierarchical Preference Optimization (HPO) step adds signals about which statements provers favor. LeanScorer combines LLM-based error analysis with a Sugeno Fuzzy Integral to give graded quality judgments rather than a pass/fail verdict. The authors also built Gaokao-Formal, a benchmark drawn from China's college entrance exam that covers domains older benchmarks tend to skip. The complete system beats other autoformalizer–prover pairings on MiniF2F and Gaokao-Formal. This matters because it moves formal verification closer to everyday mathematical text and gives the field better tools for judging formalization quality.

## Key points
- **Gaokao-Formal:** 488 Gaokao proof problems, each paired with an English version and a human-checked Lean 4 statement.
- **Mathesis-Autoformalizer:** pass rate is 22% higher than Kimina-Autoformalizer on Gaokao-Formal and 5% higher on MiniF2F.
- **LeanScorer:** reaches 0.92 F1 on Gaokao-Formal, beating LLM-as-a-Judge by 7 points and re-informalization by 27 points.
- **End-to-end accuracy:** 64% on MiniF2F (pass@32) and a state-of-the-art 18% on Gaokao-Formal.
- **Huawei Celia deployment:** tested on 95 proof sub-questions from recent Gaokao exams.
  - The DeepSeek-R1 informal-reasoning baseline scores 65.3%.
  - Adding the Mathesis pipeline raises this to 69.4%.
  - The full Celia system, which adds an interactive formal–informal framework, reaches 84.2%.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

📚 Shelves (5): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🎭 Arts and Humanities](https://md.research.elamur.ai/free/en/shelves/arts-and-humanities/) · 17,959 works · [🗣️ Language and Linguistics](https://md.research.elamur.ai/free/en/shelves/arts-and-humanities/language-and-linguistics/) · 17,789 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,948 works

## Cite

Cite as: Yu Xuejun, Jianyuan Zhong, Zijin Feng, Pengyi Zhai, Roozbeh Yousefzadeh, Wei Chong Ng, Haoxiong Liu, Ziyi Shou, Jing Xiong, Yudong Zhou, Claudia Beth Ong, Austen Jeremy Sugiarto, Yaoxi Zhang, Wai Ming Tai, Huan Cao, Dongcai Lu, Jiacheng Sun, Qiang Xu, Shen Xin and Zhenguo Li. 2025. Mathesis: Towards Formal Theorem Proving from Natural Languages. arXiv:2506.07047.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@misc{xuejun2025mathesis,
  title = {{Mathesis: Towards Formal Theorem Proving from Natural Languages}},
  author = {Yu Xuejun, Jianyuan Zhong, Zijin Feng, Pengyi Zhai, Roozbeh Yousefzadeh, Wei Chong Ng, Haoxiong Liu, Ziyi Shou, Jing Xiong, Yudong Zhou, Claudia Beth Ong, Austen Jeremy Sugiarto, Yaoxi Zhang, Wai Ming Tai, Huan Cao, Dongcai Lu, Jiacheng Sun, Qiang Xu, Shen Xin and Zhenguo Li},
  year = {2025},
  doi = {10.48550/arxiv.2506.07047},
  eprint = {2506.07047},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2506.07047}
}
```

- [← previous Liger: Linearizing Large Language Models to Gated Recurrent Structures](https://md.research.elamur.ai/free/en/papers/lan-2025-liger-linearizing-large-language-models/)
- [next → Nemotron-Math: Efficient Long-Context Distillation of Mathematical Reasoning from Multi-Mode Supervision](https://md.research.elamur.ai/free/en/papers/du-2025-nemotron-math-efficient-long-context/)
- [↑ back to papers of 2025](https://md.research.elamur.ai/free/en/papers/2025/page/11/)

## References

44 references, 30 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. [Formal mathematical reasoning: A new frontier in AI](https://md.research.elamur.ai/free/en/papers/yang-2024-formal-mathematical-reasoning-new-frontier/). In Proceedings of the International Conference on Machine Learning, 2025.
2. The mathlib Community. [The lean mathematical library](https://md.research.elamur.ai/free/en/papers/community-2019-lean-mathematical-library/). In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, POPL ’20. ACM, January 2020.
3. Lawrence C Paulson. Isabelle: A generic theorem prover. Springer, 1994. [find](https://scholar.google.com/scholar?q=Lawrence+C+Paulson%2E+Isabelle%3A+A+generic+theorem+prover%2E+Springer%2C+1994%2E)
4. Gérard Huet, Gilles Kahn, and Christine Paulin-Mohring. The coq proof assistant a tutorial. Rapport Technique, 178:113, 1997. [find](https://scholar.google.com/scholar?q=G%C3%A9rard+Huet%2C+Gilles+Kahn%2C+and+Christine+Paulin%2DMohring%2E+The+coq+proof+assistant+a+tutorial%2E+Rapport+Technique%2C+178%3A113%2C+1997%2E)
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](https://md.research.elamur.ai/free/en/papers/ren-2025-deepseek-prover-v2-advancing-formal/). arXiv preprint arXiv:2504.21801, 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](https://md.research.elamur.ai/free/en/papers/wang-2025-kimina-prover-preview-large-formal/). arXiv preprint arXiv:2504.11354, 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](https://md.research.elamur.ai/free/en/papers/lin-2025-goedel-prover-frontier-model-open/). arXiv preprint arXiv:2502.07640, 2025.
8. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. [Minif2f: a cross-system benchmark for formal olympiad-level mathematics](https://md.research.elamur.ai/free/en/papers/zheng-2021-minif2f-cross-system-benchmark-formal/). arXiv preprint arXiv:2109.00110, 2021.
9. Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. [Proofnet: Autoformalizing and formally proving undergraduate-level mathematics](https://md.research.elamur.ai/free/en/papers/azerbayev-2023-proofnet-autoformalizing-formally-proving-undergraduate/). arXiv preprint arXiv:2302.12433, 2023.
10. 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](https://md.research.elamur.ai/free/en/papers/tsoukalas-2024-putnambench-evaluating-neural-theorem-provers/). arXiv preprint arXiv:2407.11214, 2024.
11. Guoxiong Gao, Yutong Wang, Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu, and Bin Dong. [Herald: A natural language annotated lean 4 dataset](https://md.research.elamur.ai/free/en/papers/gao-2024-herald-natural-language-annotated-lean/). arXiv preprint arXiv:2410.10878, 2024.
12. 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 repository, 13:9, 2024. [find](https://scholar.google.com/scholar?q=Jia+Li%2C+Edward+Beeching%2C+Lewis+Tunstall%2C+Ben+Lipkin%2C+Roman+Soletskyi%2C+Shengyi+Huang%2C+Kashif+Rasul%2C+Longhui+Yu%2C+Albert+Q+Jiang%2C+Ziju+Shen%2C+et+al%2E+Numinamath%3A+The+largest+public+dataset+in+ai4maths+with)
13. Albert Q Jiang, Wenda Li, and Mateja Jamnik. [Multilingual mathematical autoformalization](https://md.research.elamur.ai/free/en/papers/jiang-2023-multilingual-mathematical-autoformalization/). arXiv preprint arXiv:2311.03755, 2023.
14. 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](https://md.research.elamur.ai/free/en/papers/liu-2025-atlas-autoformalizing-theorems-through-lifting/). arXiv preprint arXiv:2502.05567, 2025.
15. 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](https://md.research.elamur.ai/free/en/papers/liang-2025-mps-prover-advancing-stepwise-theorem/). arXiv preprint arXiv:2505.10962, 2025.
16. 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](https://md.research.elamur.ai/free/en/papers/xin-2025-bfs-prover-scalable-best-first/). arXiv preprint arXiv:2502.03438, 2025.
17. Yang Li, Dong Du, Linfeng Song, Chen Li, Weikang Wang, Tao Yang, and Haitao Mi. [Hunyuanprover: A scalable data synthesis framework and guided tree search for automated theorem proving](https://md.research.elamur.ai/free/en/papers/li-2024-hunyuanprover-scalable-data-synthesis/). arXiv preprint arXiv:2412.20735, 2024.
18. 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](https://md.research.elamur.ai/free/en/papers/liu-2025-proofaug-efficient-neural-theorem-proving/).
19. 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. In The Thirteenth International Conference on Learning Representations, 2025. [find](https://scholar.google.com/scholar?q=Xiao%2DWen+Yang%2C+Zhi+Zhou%2C+Haiming+Wang%2C+Aoxue+Li%2C+Wen%2DDa+Wei%2C+Hui+Jin%2C+Zhenguo+Li%2C+and+Yu%2DFeng+Li%2E+Carts%3A+Advancing+neural+theorem+proving+with+diversified+tactic+calibration+and+bias%2Dresistant+tree+se)
20. Xueliang Zhao, Wenda Li, and Lingpeng Kong. [Decomposing the enigma: Subgoal-based demonstration learning for formal theorem proving](https://md.research.elamur.ai/free/en/papers/zhao-2023-decomposing-enigma-subgoal-based-demonstration/). arXiv preprint arXiv:2305.16366, 2023.
21. 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](https://md.research.elamur.ai/free/en/papers/wang-2023-lego-prover-neural-theorem-proving/). arXiv preprint arXiv:2310.00656, 2023.
22. 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](https://md.research.elamur.ai/free/en/papers/jiang-2022-draft-sketch-prove-guiding-formal/). arXiv preprint arXiv:2210.12283, 2022.
23. 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 feedback for reinforcement learning and monte-carlo tree search. arXiv preprint arXiv:2408.[08152, 2024](https://md.research.elamur.ai/free/en/papers/xin-2024-deepseek-prover-v1-5-harnessing/).
24. Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. [Autoformalization with large language models](https://md.research.elamur.ai/free/en/papers/wu-2022-autoformalization-large-language-models/). Advances in Neural Information Processing Systems, 35:32353–32368, 2022.
25. Anthropic. The Claude 3 model family: Opus, Sonnet, Haiku. Model Card, March 2024. [find](https://scholar.google.com/scholar?q=Anthropic%2E+The+Claude+3+model+family%3A+Opus%2C+Sonnet%2C+Haiku%2E+Model+Card%2C+March+2024%2E)
26. DeepSeek-AI and Anonymous Contributors. [DeepSeek-R1: Incentivizing reasoning capability in LLMs via reinforcement learning](https://md.research.elamur.ai/free/en/papers/deepseek-ai-2025-deepseek-r1-incentivizing-reasoning-capability/), 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](https://md.research.elamur.ai/free/en/papers/shao-2024-deepseekmath-pushing-limits-mathematical-reasoning/), 2024.
28. Maarten Grootendorst. [Bertopic: Neural topic modeling with a class-based tf-idf procedure](https://md.research.elamur.ai/free/en/papers/grootendorst-2022-bertopic-neural-topic-modeling-class/). arXiv preprint arXiv:2203.05794, 2022.
29. 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](https://md.research.elamur.ai/free/en/papers/ying-2024-lean-workbook-large-scale-lean/). arXiv preprint arXiv:2406.03847, 2024.
30. 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](https://md.research.elamur.ai/free/en/papers/rafailov-2023-direct-preference-optimization-language-model/). Advances in Neural Information Processing Systems, 36:53728–53741, 2023.
31. 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](https://md.research.elamur.ai/free/en/papers/ouyang-2022-training-language-models-follow-instructions/). Advances in neural information processing systems, 35:27730–27744, 2022.
32. 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. — [arXiv:2503.12854](https://arxiv.org/abs/2503.12854) [find](https://scholar.google.com/scholar?q=Songjun+Tu%2C+Jiahao+Lin%2C+Xiangyu+Tian%2C+Qichao+Zhang%2C+Linjing+Li%2C+Yuqian+Fu%2C+Nan+Xu%2C+Wei+He%2C+Xiangyuan+Lan%2C+Dongmei+Jiang%2C+et+al%2E+Enhancing+llm+reasoning+with+iterative+dpo%3A+A+comprehensive+empirical+in)
33. Tianduo Wang, Shichen Li, and Wei Lu. Self-training with direct preference optimization improves chain-of-thought reasoning. arXiv preprint arXiv:2407.18248, 2024. [find](https://scholar.google.com/scholar?q=Tianduo+Wang%2C+Shichen+Li%2C+and+Wei+Lu%2E+Self%2Dtraining+with+direct+preference+optimization+improves+chain%2Dof%2Dthought+reasoning%2E+arXiv+preprint+arXiv%3A2407%2E18248%2C+2024%2E)
34. 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. — [arXiv:2504.15843](https://arxiv.org/abs/2504.15843) [find](https://scholar.google.com/scholar?q=Junshu+Pan%2C+Wei+Shen%2C+Shulin+Huang%2C+Qiji+Zhou%2C+and+Yue+Zhang%2E+Pre%2Ddpo%3A+Improving+data+utilization+in+direct+preference+optimization+using+a+guiding+reference+model%2E+arXiv+preprint+arXiv%3A2504%2E15843%2C+20)
35. Michio Sugeno. Theory of fuzzy integrals and its applications. Doctoral Thesis, Tokyo Institute of Technology, 1974. [find](https://scholar.google.com/scholar?q=Michio+Sugeno%2E+Theory+of+fuzzy+integrals+and+its+applications%2E+Doctoral+Thesis%2C+Tokyo+Institute+of+Technology%2C+1974%2E)
36. 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. [find](https://scholar.google.com/scholar?q=Jonata+Wieczynski%2C+Giancarlo+Lucca%2C+Eduardo+Borges%2C+Asier+Urio%2DLarrea%2C+Carlos+L%C3%B3pez+Molina%2C+Humberto+Bustince%2C+and+Gra%C3%A7aliz+Dimuro%2E+Application+of+the+sugeno+integral+in+fuzzy+rule%2Dbased+classificatio)
37. 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 self-improvement](https://md.research.elamur.ai/free/en/papers/yang-2024-qwen2-5-math-technical-report/). arXiv p…
38. DeepSeek-AI. Deepseek-v3 technical report, 2024. [find](https://scholar.google.com/scholar?q=DeepSeek%2DAI%2E+Deepseek%2Dv3+technical+report%2C+2024%2E)
39. Kimi Authors. [Kimi k1.5: Scaling reinforcement learning with LLMs](https://md.research.elamur.ai/free/en/papers/kimi-team-2025-kimi-k1-5-scaling-reinforcement/), 2025.
40. 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](https://md.research.elamur.ai/free/en/papers/hu-2021-lora-low-rank-adaptation-large/). In International Conference on Learning Representations (ICLR), 2022.
41. Ilya Loshchilov and Frank Hutter. Decoupled weight decay regularization. In International Conference on Learning Representations (ICLR), 2019. [find](https://scholar.google.com/scholar?q=Ilya+Loshchilov+and+Frank+Hutter%2E+Decoupled+weight+decay+regularization%2E+In+International+Conference+on+Learning+Representations+%28ICLR%29%2C+2019%2E)
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, Mariama Drame, Quentin Lhoe… — [Transformers: State-of-the-Art Natural Language Processing](https://md.research.elamur.ai/free/en/papers/wolf-2020-transformers-state-art-natural-language/)
43. Leandro von Werra, Lewis Schmid, Thomas Wolf, and Lewis Tunstall. Trl: Transformer reinforcement learning. [https://github.com/huggingface/trl](https://github.com/huggingface/trl), 2020-2024. [↗](https://github.com/huggingface/trl)
44. Lukas Biewald. Experiment tracking with weights and biases. [https://wandb.ai](https://wandb.ai), 2020. Software available from wandb.com. [↗](https://wandb.ai)

*Updated 3 November 2026*