---
title: "Who cites Peiyang Song — 205 papers of our library"
description: "205 papers of the Elamur Research library cite the works of Peiyang Song, found in their bibliographies; the most cited first."
canonical: "https://research.elamur.ai/free/en/authors/peiyang-song/cited-by/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/authors/peiyang-song/cited-by/)

[home](https://md.research.elamur.ai/free/en/) / [authors](https://md.research.elamur.ai/free/en/authors/) / [Peiyang Song](https://md.research.elamur.ai/free/en/authors/peiyang-song/) / cited by

# Who cites Peiyang Song

224 citations of their works from 205 papers of our library (of the 149,439 whose bibliographies we read) · 97 with a page here, the most cited first · [← Peiyang Song](https://md.research.elamur.ai/free/en/authors/peiyang-song/)

1. **[A Comprehensive Overview of Large Language Models](https://md.research.elamur.ai/free/en/papers/naveed-2023-comprehensive-overview-large-language-models/) [ACM Transactions on Intelligent Systems and Technology](https://md.research.elamur.ai/free/en/venues/acm-transactions-on-intelligent-systems-and-technology/)**Humza Naveed, Asad Ullah Khan, Shi Qiu, et al.*2023 · 1,287 citations*
2. **[The Rise and Potential of Large Language Model Based Agents: A Survey](https://md.research.elamur.ai/free/en/papers/xi-2023-rise-potential-large-language/) [Science China Information Sciences](https://md.research.elamur.ai/free/en/venues/science-china-information-sciences/)**Zhiheng Xi, Wenxiang Chen, Xin Guo, et al.*2023 · 1,272 citations*
3. [**Retrieval-Augmented Generation for AI-Generated Content: A Survey arXiv:2402.19473**Penghao Zhao, Hailin Zhang, Qinhan Yu, et al.*2024 · 301 citations*](https://md.research.elamur.ai/free/en/papers/zhao-2024-retrieval-augmented-generation-ai-generated/)
4. [**Llemma: An Open Language Model For Mathematics arXiv:2310.10631**Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, et al.*2023 · 286 citations*](https://md.research.elamur.ai/free/en/papers/azerbayev-2023-llemma-open-language-model-mathematics/)
5. [**AlphaEvolve: A coding agent for scientific and algorithmic discovery arXiv:2506.13131**Alexander Novikov, Ngân Vũ, Marvin Eisenberger, et al.*2025 · 202 citations*](https://md.research.elamur.ai/free/en/papers/novikov-2025-alphaevolve-coding-agent-scientific-algorithmic/)
6. [**Will we run out of data? Limits of LLM scaling based on human-generated data arXiv:2211.04325**Pablo Villalobos, Anson Ho, Jaime Sevilla, et al.*2022 · 198 citations*](https://md.research.elamur.ai/free/en/papers/villalobos-2022-will-run-out-data-limits/)
7. [**MINT: Evaluating LLMs in Multi-turn Interaction with Tools and Language Feedback arXiv:2309.10691**Xingyao Wang, Zihan Wang, Jiateng Liu, et al.*2023 · 141 citations*](https://md.research.elamur.ai/free/en/papers/wang-2023-mint-evaluating-llms-multi-turn/)
8. **[A Survey on Recent Advances in LLM-Based Multi-turn Dialogue Systems](https://md.research.elamur.ai/free/en/papers/yi-2024-survey-recent-advances-llm-based/) [ACM Computing Surveys](https://md.research.elamur.ai/free/en/venues/acm-computing-surveys/)**Zihao Yi, Jiarui Ouyang, Zhe Xu, et al.*2024 · 130 citations*
9. [**Towards Large Reasoning Models: A Survey of Reinforced Reasoning with Large Language Models arXiv:2501.09686**Fengli Xu, Qianyue Hao, Zefang Zong, et al.*2025 · 120 citations*](https://md.research.elamur.ai/free/en/papers/xu-2025-towards-large-reasoning-models-survey/)
10. [**DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search arXiv:2408.08152**Huajian Xin, Z. Z. Ren, Junxiao Song, et al.*2024 · 116 citations*](https://md.research.elamur.ai/free/en/papers/xin-2024-deepseek-prover-v1-5-harnessing/)
11. [**DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data arXiv:2405.14333**Huajian Xin, Daya Guo, Zhihong Shao, et al.*2024 · 111 citations*](https://md.research.elamur.ai/free/en/papers/xin-2024-deepseek-prover-advancing-theorem-proving/)
12. **[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/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**George Tsoukalas, Jasper Lee, John Jennings, et al.*2024 · 93 citations*
13. [**InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning arXiv:2402.06332**Huaiyuan Ying, Shuo Zhang, Linyang Li, et al.*2024 · 90 citations*](https://md.research.elamur.ai/free/en/papers/ying-2024-internlm-math-open-math-large/)
14. [**Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving arXiv:2502.07640**Yong Lin, Shange Tang, Bohan Lyu, et al.*2025 · 84 citations*](https://md.research.elamur.ai/free/en/papers/lin-2025-goedel-prover-frontier-model-open/)
15. **[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/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Huaiyuan Ying, Zijian Wu, Yihan Geng, et al.*2024 · 80 citations*
16. [**LEGO-Prover: Neural Theorem Proving with Growing Libraries arXiv:2310.00656**Haiming Wang, Huajian Xin, Chuanyang Zheng, et al.*2023 · 79 citations*](https://md.research.elamur.ai/free/en/papers/wang-2023-lego-prover-neural-theorem-proving/)
17. [**BRIGHT: A Realistic and Challenging Benchmark for Reasoning-Intensive Retrieval arXiv:2407.12883**Hongjin Su, Howard Yen, Mengzhou Xia, et al.*2024 · 77 citations*](https://md.research.elamur.ai/free/en/papers/su-2024-bright-realistic-challenging-benchmark-reasoning/)
18. **[Recursive Introspection: Teaching Language Model Agents How to Self-Improve](https://md.research.elamur.ai/free/en/papers/qu-2024-recursive-introspection-teaching-language-model/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Yuxiao Qu, Tianjun Zhang, Naman Garg, et al.*2024 · 75 citations*
19. [**Cumulative Reasoning with Large Language Models arXiv:2308.04371**Yifan Zhang, Jingqin Yang, Yang Yuan, et al.*2023 · 74 citations*](https://md.research.elamur.ai/free/en/papers/zhang-2023-cumulative-reasoning-large-language-models/)
20. [**Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction arXiv:2508.03613**Yong Lin, Shange Tang, Bohan Lyu, et al.*2025 · 67 citations*](https://md.research.elamur.ai/free/en/papers/lin-2025-goedel-prover-v2-scaling-formal/)
21. [**ArCHer: Training Language Model Agents via Hierarchical Multi-Turn RL arXiv:2402.19446**Yifei Zhou, Andrea Zanette, Jiayi Pan, et al.*2024 · 54 citations*](https://md.research.elamur.ai/free/en/papers/zhou-2024-archer-training-language-model-agents/)
22. [**From Decoding to Meta-Generation: Inference-time Algorithms for Large Language Models arXiv:2406.16838**Sean Welleck, Amanda Bertsch, Matthew Finlayson, et al.*2024 · 51 citations*](https://md.research.elamur.ai/free/en/papers/welleck-2024-decoding-meta-generation-inference-time/)
23. [**Lean-STaR: Learning to Interleave Thinking and Proving arXiv:2407.10040**Haohan Lin, Zhiqing Sun, Sean Welleck, et al.*2024 · 51 citations*](https://md.research.elamur.ai/free/en/papers/lin-2024-lean-star-learning-interleave-thinking/)
24. **[TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts](https://md.research.elamur.ai/free/en/papers/wang-2024-theoremllama-transforming-general-purpose-llms/) [Conference on Empirical Methods in Natural Language Processing (EMNLP)](https://md.research.elamur.ai/free/en/venues/emnlp/)**Ruida Wang, Jipeng Zhang, Yizhen Jia, et al.*2024 · 51 citations*
25. **[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/) [Annual Meeting of the Association for Computational Linguistics (ACL)](https://md.research.elamur.ai/free/en/venues/acl/)**Ran Xin, Chenguang Xi, Jie Yang, et al.*2025 · 49 citations*
26. [**Formal Mathematical Reasoning: A New Frontier in AI arXiv:2412.16075**Kaiyu Yang, Gabriel Poesia, Jingxuan He, et al.*2024 · 49 citations*](https://md.research.elamur.ai/free/en/papers/yang-2024-formal-mathematical-reasoning-new-frontier/)
27. [**Chain of Ideas: Revolutionizing Research Via Novel Idea Development with LLM Agents arXiv:2410.13185**Long Li, Weiwen Xu, Jiayan Guo, et al.*2024 · 47 citations*](https://md.research.elamur.ai/free/en/papers/li-2024-chain-ideas-revolutionizing-research/)
28. [**LLM-SR: Scientific Equation Discovery via Programming with Large Language Models arXiv:2404.18400**Parshin Shojaee, Kazem Meidani, Shashank Gupta, et al.*2024 · 47 citations*](https://md.research.elamur.ai/free/en/papers/shojaee-2024-llm-sr-scientific-equation/)
29. [**An In-Context Learning Agent for Formal Theorem-Proving arXiv:2310.04353**Amitayush Thakur, George Tsoukalas, Yeming Wen, et al.*2023 · 47 citations*](https://md.research.elamur.ai/free/en/papers/thakur-2023-context-learning-agent-formal-theorem/)
30. [**Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving arXiv:2507.23726**Luoxin Chen, Jinming Gu, Liankai Huang, et al.*2025 · 46 citations*](https://md.research.elamur.ai/free/en/papers/chen-2025-seed-prover-deep-broad-reasoning/)
31. [**A Survey on Deep Learning for Theorem Proving arXiv:2404.09939**Zhaoyu Li, Jialiang Sun, Logan Murphy, et al.*2024 · 46 citations*](https://md.research.elamur.ai/free/en/papers/li-2024-survey-deep-learning-theorem-proving/)
32. [**STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving arXiv:2502.00212**Kefan Dong, Tengyu Ma*2025 · 43 citations*](https://md.research.elamur.ai/free/en/papers/dong-2025-stp-self-play-llm-theorem/)
33. [**Let's reward step by step: Step-Level reward model as the Navigators for Reasoning arXiv:2310.10080**Qianli Ma, Haotian Zhou, Tingkai Liu, et al.*2023 · 40 citations*](https://md.research.elamur.ai/free/en/papers/ma-2023-let-s-reward-step-step/)
34. [**A Survey of Frontiers in LLM Reasoning: Inference Scaling, Learning to Reason, and Agentic Systems arXiv:2504.09037**Zixuan Ke, Fangkai Jiao, Yifei Ming, et al.*2025 · 39 citations*](https://md.research.elamur.ai/free/en/papers/ke-2025-survey-frontiers-llm-reasoning-inference/)
35. [**Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean arXiv:2404.12534**Peiyang Song, Kaiyu Yang, Anima Anandkumar*2024 · 39 citations*](https://md.research.elamur.ai/free/en/papers/song-2024-lean-copilot-large-language-models/)
36. **[SciInstruct: a Self-Reflective Instruction Annotated Dataset for Training Scientific Language Models](https://md.research.elamur.ai/free/en/papers/zhang-2024-sciinstruct-self-reflective-instruction-annotated/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Dan Zhang, Ziniu Hu, Sining Zhoubian, et al.*2024 · 37 citations*
37. [**Multilingual Mathematical Autoformalization arXiv:2311.03755**Albert Q. Jiang, Wenda Li, Mateja Jamnik*2023 · 37 citations*](https://md.research.elamur.ai/free/en/papers/jiang-2023-multilingual-mathematical-autoformalization/)
38. [**Magnushammer: A Transformer-Based Approach to Premise Selection arXiv:2303.04488**Maciej Mikuła, Szymon Tworkowski, Szymon Antoniak, et al.*2023 · 35 citations*](https://md.research.elamur.ai/free/en/papers/mikula-2023-magnushammer-transformer-based-approach-premise/)
39. [**Process-Driven Autoformalization in Lean 4 arXiv:2406.01940**Jianqiao Lu, Yingjia Wan, Zhengying Liu, et al.*2024 · 33 citations*](https://md.research.elamur.ai/free/en/papers/lu-2024-process-driven-autoformalization-lean-4/)
40. [**FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models arXiv:2505.02735**Zhouliang Yu, Ruotian Peng, Keyi Ding, et al.*2025 · 31 citations*](https://md.research.elamur.ai/free/en/papers/yu-2025-formalmath-benchmarking-formal-mathematical-reasoning/)
41. **[Aristotle: IMO-level Automated Theorem Proving](https://md.research.elamur.ai/free/en/papers/achim-2025-aristotle-imo-level-automated-theorem/) [SuperIntelligence - Robotics - Safety & Alignment](https://md.research.elamur.ai/free/en/venues/superintelligence-robotics-safety-alignment/)**Tudor Achim, Alex Best, Alberto Bietti, et al.*2025 · 29 citations*
42. **[AutoVerus: Automated Proof Generation for Rust Code](https://md.research.elamur.ai/free/en/papers/yang-2024-autoverus-automated-proof-generation-rust/) [Proceedings of the ACM on Programming Languages](https://md.research.elamur.ai/free/en/venues/proceedings-of-the-acm-on-programming-languages/)**Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, et al.*2024 · 28 citations*
43. **[A Survey on Large Language Models for Mathematical Reasoning](https://md.research.elamur.ai/free/en/papers/wang-2025-survey-large-language-models-mathematical/) [ACM Computing Surveys](https://md.research.elamur.ai/free/en/venues/acm-computing-surveys/)**Peng-Yuan Wang, Tian-Shuo Liu, Chenyang Wang, et al.*2025 · 26 citations*
44. [**Hilbert: Recursively Building Formal Proofs with Informal Reasoning arXiv:2509.22819**Sumanth Varambally, Thomas Voice, Yanchao Sun, et al.*2025 · 26 citations*](https://md.research.elamur.ai/free/en/papers/varambally-2025-hilbert-recursively-building-formal-proofs/)
45. [**Logical Reasoning in Large Language Models: A Survey arXiv:2502.09100**Hanmeng Liu, Zhizhang Fu, Mengru Ding, et al.*2025 · 25 citations*](https://md.research.elamur.ai/free/en/papers/liu-2025-logical-reasoning-large-language-models/)
46. [**HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving arXiv:2412.20735**Yang Li, Dong Du, Linfeng Song, et al.*2024 · 25 citations*](https://md.research.elamur.ai/free/en/papers/li-2024-hunyuanprover-scalable-data-synthesis/)
47. [**StateFlow: Enhancing LLM Task-Solving through State-Driven Workflows arXiv:2403.11322**Yiran Wu, Tianwei Yue, Shaokun Zhang, et al.*2024 · 25 citations*](https://md.research.elamur.ai/free/en/papers/wu-2024-stateflow-enhancing-llm-task-solving/)
48. **[Aligning LLMs with Individual Preferences via Interaction](https://md.research.elamur.ai/free/en/papers/wu-2025-aligning-llms-individual-preferences-interaction/) [International Conference on Computational Linguistics (COLING)](https://md.research.elamur.ai/free/en/venues/coling/)**Shujin Wu, Yi R. Fung, Cheng Qian, et al.*2025 · 24 citations*
49. [**Lyra: Orchestrating Dual Correction in Automated Theorem Proving arXiv:2309.15806**Chuanyang Zheng, Haiming Wang, Enze Xie, et al.*2023 · 24 citations*](https://md.research.elamur.ai/free/en/papers/zheng-2023-lyra-orchestrating-dual-correction-automated/)
50. [**LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover arXiv:2407.17227**Zijian Wu, Jiayu Wang, Dahua Lin, et al.*2024 · 23 citations*](https://md.research.elamur.ai/free/en/papers/wu-2024-lean-github-compiling-github-lean/)
51. **[Learning Formal Mathematics From Intrinsic Motivation](https://md.research.elamur.ai/free/en/papers/poesia-2024-learning-formal-mathematics-intrinsic-motivation/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Gabriel Poesia, David Broman, Nick Haber, et al.*2024 · 23 citations*
52. [**LLMSTEP: LLM proofstep suggestions in Lean arXiv:2310.18457**Sean Welleck, Rahul Saha*2023 · 22 citations*](https://md.research.elamur.ai/free/en/papers/welleck-2023-llmstep-llm-proofstep-suggestions-lean/)
53. **[AI4Research: A Survey of Artificial Intelligence for Scientific Research](https://md.research.elamur.ai/free/en/papers/chen-2025-ai4research-survey-artificial-intelligence/) [Science China Information Sciences](https://md.research.elamur.ai/free/en/venues/science-china-information-sciences/)**Qiguang Chen, Mingda Yang, Libo Qin, et al.*2025 · 21 citations*
54. [**Leanabell-Prover: Posttraining Scaling in Formal Reasoning arXiv:2504.06122**Jingyuan Zhang, Qi Wang, Xingguang Ji, et al.*2025 · 21 citations*](https://md.research.elamur.ai/free/en/papers/zhang-2025-leanabell-prover-posttraining-scaling-formal/)
55. [**The Limits of Inference Scaling Through Resampling arXiv:2411.17501**Benedikt Stroebl, Sayash Kapoor, Arvind Narayanan*2024 · 21 citations*](https://md.research.elamur.ai/free/en/papers/stroebl-2024-limits-inference-scaling-through-resampling/)
56. **[TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models](https://md.research.elamur.ai/free/en/papers/xiong-2023-trigo-benchmarking-formal-mathematical-proof/) [Conference on Empirical Methods in Natural Language Processing (EMNLP)](https://md.research.elamur.ai/free/en/venues/emnlp/)**Jing Xiong, Jianhao Shen, Ye Yuan, et al.*2023 · 21 citations*
57. [**Graph2Tac: Online Representation Learning of Formal Math Concepts arXiv:2401.02949**Lasse Blaauwbroek, Miroslav Olšák, Jason Rute, et al.*2024 · 19 citations*](https://md.research.elamur.ai/free/en/papers/blaauwbroek-2024-graph2tac-online-representation-learning-formal/)
58. **[Proving Theorems Recursively](https://md.research.elamur.ai/free/en/papers/wang-2024-proving-theorems-recursively/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Haiming Wang, Huajian Xin, Zhengying Liu, et al.*2024 · 19 citations*
59. [**MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving arXiv:2503.03205**Ruida Wang, Rui Pan, Yuxin Li, et al.*2025 · 18 citations*](https://md.research.elamur.ai/free/en/papers/wang-2025-ma-lot-model-collaboration-lean/)
60. [**FormalAlign: Automated Alignment Evaluation for Autoformalization arXiv:2410.10135**Jianqiao Lu, Yingjia Wan, Yinya Huang, et al.*2024 · 18 citations*](https://md.research.elamur.ai/free/en/papers/lu-2024-formalalign-automated-alignment-evaluation-autoformalization/)
61. **[Machine learning and information theory concepts towards an AI Mathematician](https://md.research.elamur.ai/free/en/papers/bengio-2024-machine-learning-information-theory-concepts/) [Bulletin of the American Mathematical Society](https://md.research.elamur.ai/free/en/venues/bulletin-of-the-american-mathematical-society/)**Yoshua Bengio, Nikolay Malkin*2024 · 18 citations*
62. [**miniCTX: Neural Theorem Proving with (Long-)Contexts arXiv:2408.03350**Jiewen Hu, Thomas Zhu, Sean Welleck*2024 · 18 citations*](https://md.research.elamur.ai/free/en/papers/hu-2024-minictx-neural-theorem-proving-long/)
63. **[APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning](https://md.research.elamur.ai/free/en/papers/ospanov-2025-apollo-automated-llm-lean-collaboration/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Azim Ospanov, Farzan Farnia, Roozbeh Yousefzadeh*2025 · 17 citations*
64. **[Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification](https://md.research.elamur.ai/free/en/papers/liu-2025-safe-enhancing-mathematical-reasoning-large/) [Annual Meeting of the Association for Computational Linguistics (ACL)](https://md.research.elamur.ai/free/en/venues/acl/)**Chengwu Liu, Ye Yuan, Yichun Yin, et al.*2025 · 17 citations*
65. **[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/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, et al.*2025 · 16 citations*
66. [**Mathematical exploration and discovery at scale arXiv:2511.02864**Bogdan Georgiev, Javier Gómez-Serrano, Terence Tao, et al.*2025 · 16 citations*](https://md.research.elamur.ai/free/en/papers/georgiev-2025-mathematical-exploration-discovery-scale/)
67. [**Solving Formal Math Problems by Decomposition and Iterative Reflection arXiv:2507.15225**Yichi Zhou, Jianqiu Zhao, Yongxin Zhang, et al.*2025 · 16 citations*](https://md.research.elamur.ai/free/en/papers/zhou-2025-solving-formal-math-problems-decomposition/)
68. [**DafnyBench: A Benchmark for Formal Software Verification arXiv:2406.08467**Chloe Loughridge, Qinyi Sun, Seth Ahrenbach, et al.*2024 · 15 citations*](https://md.research.elamur.ai/free/en/papers/loughridge-2024-dafnybench-benchmark-formal-software-verification/)
69. [**Kimina Lean Server: A High-Performance Lean Server for Large-Scale Verification arXiv:2504.21230**Marco Dos Santos, Hugues de Saxcé, Haiming Wang, et al.*2025 · 14 citations*](https://md.research.elamur.ai/free/en/papers/santos-2025-kimina-lean-server-high-performance/)
70. [**Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs arXiv:2506.19923**Kaito Baba, Chaoran Liu, Shuhei Kurita, et al.*2025 · 14 citations*](https://md.research.elamur.ai/free/en/papers/baba-2025-prover-agent-agent-based-framework/)
71. [**BioKGBench: A Knowledge Graph Checking Benchmark of AI Agent for Biomedical Science arXiv:2407.00466**Xinna Lin, Siqi Ma, Junjie Shan, et al.*2024 · 12 citations*](https://md.research.elamur.ai/free/en/papers/lin-2024-biokgbench-knowledge-graph-checking-benchmark/)
72. **[Proving Olympiad Algebraic Inequalities without Human Demonstrations](https://md.research.elamur.ai/free/en/papers/wei-2024-proving-olympiad-algebraic-inequalities-without/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Chenrui Wei, Mengzhou Sun, Wei Wang*2024 · 12 citations*
73. **[Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions](https://md.research.elamur.ai/free/en/papers/zhang-2025-autoformalization-wild-assessing-llms-real/) [Conference on Empirical Methods in Natural Language Processing (EMNLP)](https://md.research.elamur.ai/free/en/venues/emnlp/)**Lan Zhang, Marco Valentino, Andre Freitas*2025 · 11 citations*
74. **[IRIS: Interactive Research Ideation System for Accelerating Scientific Discovery](https://md.research.elamur.ai/free/en/papers/garikaparthi-2025-iris-interactive-research-ideation-system/) [Annual Meeting of the Association for Computational Linguistics (ACL)](https://md.research.elamur.ai/free/en/venues/acl/)**Aniketh Garikaparthi, Manasi Patwardhan, Lovekesh Vig, et al.*2025 · 11 citations*
75. [**Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning arXiv:2502.13834**Zenan Li, Zhaoyu Li, Wen Tang, et al.*2025 · 11 citations*](https://md.research.elamur.ai/free/en/papers/li-2025-proving-olympiad-inequalities-synergizing-llms/)
76. [**ScienceBoard: Evaluating Multimodal Autonomous Agents in Realistic Scientific Workflows arXiv:2505.19897**Qiushi Sun, Zhoumianze Liu, Chang Ma, et al.*2025 · 11 citations*](https://md.research.elamur.ai/free/en/papers/sun-2025-scienceboard-evaluating-multimodal-autonomous-agents/)
77. **[Consistent Autoformalization for Constructing Mathematical Libraries](https://md.research.elamur.ai/free/en/papers/zhang-2024-consistent-autoformalization-constructing-mathematical-libraries/) [Conference on Empirical Methods in Natural Language Processing (EMNLP)](https://md.research.elamur.ai/free/en/venues/emnlp/)**Lan Zhang, Xin Quan, Andre Freitas*2024 · 11 citations*
78. [**REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning arXiv:2505.20613**Ziju Shen, Naohao Huang, Fanyi Yang, et al.*2025 · 10 citations*](https://md.research.elamur.ai/free/en/papers/shen-2025-real-prover-retrieval-augmented-lean/)
79. [**Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics arXiv:2510.12787**Benjamin Breen, Marco Del Tredici, Jacob McCarran, et al.*2025 · 9 citations*](https://md.research.elamur.ai/free/en/papers/breen-2025-ax-prover-deep-reasoning-agentic/)
80. **[Rethinking Fine-Tuning when Scaling Test-Time Compute: Limiting Confidence Improves Mathematical Reasoning](https://md.research.elamur.ai/free/en/papers/chen-2025-rethinking-fine-tuning-scaling-test/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Feng Chen, Allan Raventos, Nan Cheng, et al.*2025 · 9 citations*
81. [**ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization arXiv:2510.24592**Guoxin Chen, Jing Wu, Xinjie Chen, et al.*2025 · 8 citations*](https://md.research.elamur.ai/free/en/papers/chen-2025-reform-reflective-autoformalization-prospective-bounded/)
82. **[Let's Reason Formally: Natural-Formal Hybrid Reasoning Enhances LLM's Math Capability](https://md.research.elamur.ai/free/en/papers/wang-2025-let-s-reason-formally-natural/) [Conference on Empirical Methods in Natural Language Processing (EMNLP)](https://md.research.elamur.ai/free/en/venues/emnlp/)**Ruida Wang, Yuxin Li, Yi R. Fung, et al.*2025 · 7 citations*
83. **[Math Neurosurgery: Isolating Language Models' Math Reasoning Abilities Using Only Forward Passes](https://md.research.elamur.ai/free/en/papers/christ-2025-math-neurosurgery-isolating-language-models/) [Annual Meeting of the Association for Computational Linguistics (ACL)](https://md.research.elamur.ai/free/en/venues/acl/)**Bryan R Christ, Zachary Gottesman, Jonathan Kropko, et al.*2025 · 7 citations*
84. **[Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models](https://md.research.elamur.ai/free/en/papers/cao-2025-reviving-dsp-advanced-theorem-proving/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Chenrui Cao, Liangcheng Song, Zenan Li, et al.*2025 · 7 citations*
85. [**Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers arXiv:2509.06493**Ran Xin, Zeyu Zheng, Yanchen Nie, et al.*2025 · 7 citations*](https://md.research.elamur.ai/free/en/papers/xin-2025-scaling-up-multi-turn-off/)
86. [**A Lean Dataset for International Math Olympiad: Small Steps towards Writing Math Proofs for Hard Problems arXiv:2411.18872**Roozbeh Yousefzadeh, Xuenan Cao, Azim Ospanov*2024 · 7 citations*](https://md.research.elamur.ai/free/en/papers/yousefzadeh-2024-lean-dataset-international-math-olympiad/)
87. [**A New Approach Towards Autoformalization arXiv:2310.07957**Nilay Patel, Rahul Saha, Jeffrey Flanigan*2023 · 7 citations*](https://md.research.elamur.ai/free/en/papers/patel-2023-new-approach-towards-autoformalization/)
88. **[EVOTOOL: Self-Evolving Tool-Use Policy Optimization in LLM Agents via Blame-Aware Mutation and Diversity-Aware Selection](https://md.research.elamur.ai/free/en/papers/yang-2026-evotool-self-evolving-tool-use/) [Annual Meeting of the Association for Computational Linguistics (ACL)](https://md.research.elamur.ai/free/en/venues/acl/)**Shuo Yang, Caren Han, Xueqi Ma, et al.*2026 · 6 citations*
89. [**Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving arXiv:2507.02726**Matthieu Zimmer, Xiaotong Ji, Rasul Tutunov, et al.*2025 · 5 citations*](https://md.research.elamur.ai/free/en/papers/zimmer-2025-bourbaki-self-generated-goal-conditioned/)
90. [**Premise Selection for a Lean Hammer arXiv:2506.07477**Thomas Zhu, Joshua Clune, Jeremy Avigad, et al.*2025 · 5 citations*](https://md.research.elamur.ai/free/en/papers/zhu-2025-premise-selection-lean-hammer/)
91. [**ImProver: Agent-Based Automated Proof Optimization arXiv:2410.04753**Riyaz Ahuja, Jeremy Avigad, Prasad Tetali, et al.*2024 · 5 citations*](https://md.research.elamur.ai/free/en/papers/ahuja-2024-improver-agent-based-automated-proof/)
92. **[Uncertainty Quantification in LLM Agents: Foundations, Emerging Challenges, and Opportunities](https://md.research.elamur.ai/free/en/papers/oh-2026-uncertainty-quantification-llm-agents-foundations/) [Annual Meeting of the Association for Computational Linguistics (ACL)](https://md.research.elamur.ai/free/en/venues/acl/)**Changdae Oh, Seongheon Park, To Eun Kim, et al.*2026 · 4 citations*
93. **[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/) [Conference on Neural Information Processing Systems (NeurIPS)](https://md.research.elamur.ai/free/en/venues/neural-information-processing-systems/)**Zhenwen Liang, Linfeng Song, Yang Li, et al.*2025 · 4 citations*
94. **[EngiBench: A Benchmark for Evaluating Large Language Models on Engineering Problem Solving](https://md.research.elamur.ai/free/en/papers/zhou-2026-engibench-benchmark-evaluating-large-language/) [Findings of the Association for Computational Linguistics](https://md.research.elamur.ai/free/en/venues/findings/)**Xiyuan Zhou, Xinlei Wang, Yirui He, et al.*2026 · 3 citations*
95. **[FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean](https://md.research.elamur.ai/free/en/papers/meadows-2026-formalscience-scalable-human-loop-autoformalisation/) [Annual Meeting of the Association for Computational Linguistics (ACL)](https://md.research.elamur.ai/free/en/venues/acl/)**Jordan Meadows, Lan Zhang, Andre Freitas*2026*
96. **[From Natural Language to Certified Geometry Proofs: A Survey of LLM-Augmented Verification and Neuro-Symbolic Theorem Proving](https://md.research.elamur.ai/free/en/papers/tzachristas-2026-natural-language-certified-geometry-proofs/) [Big Picture v2: Crafting a Research Narrative](https://md.research.elamur.ai/free/en/venues/bigpicture/)**Ioannis Tzachristas, Georgios Tzachristas*2026*
97. **[Reliable Use of Lemmas via Eligibility Reasoning and Section-Aware Reinforcement Learning](https://md.research.elamur.ai/free/en/papers/xu-2026-reliable-use-lemmas-eligibility-reasoning/) [Annual Meeting of the Association for Computational Linguistics (ACL)](https://md.research.elamur.ai/free/en/venues/acl/)**Zhikun Xu, Xiaodong Yu, Ben Zhou, et al.*2026*

108 more citing papers of our library have no page here yet.

- [← back to](https://md.research.elamur.ai/free/en/authors/peiyang-song/) — Peiyang Song