🧑‍🔬 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

1. A Comprehensive Overview of Large Language ModelsACM Transactions on Intelligent Systems and TechnologyHumza Naveed, Asad Ullah Khan, Shi Qiu, et al.2023 · 1,287 citations
2. The Rise and Potential of Large Language Model Based Agents: A SurveyScience China Information SciencesZhiheng Xi, Wenxiang Chen, Xin Guo, et al.2023 · 1,272 citations
3. Retrieval-Augmented Generation for AI-Generated Content: A SurveyarXiv:2402.19473Penghao Zhao, Hailin Zhang, Qinhan Yu, et al.2024 · 301 citations
4. Llemma: An Open Language Model For MathematicsarXiv:2310.10631Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, et al.2023 · 286 citations
5. AlphaEvolve: A coding agent for scientific and algorithmic discoveryarXiv:2506.13131Alexander Novikov, Ngân Vũ, Marvin Eisenberger, et al.2025 · 202 citations
6. Will we run out of data? Limits of LLM scaling based on human-generated dataarXiv:2211.04325Pablo Villalobos, Anson Ho, Jaime Sevilla, et al.2022 · 198 citations
7. MINT: Evaluating LLMs in Multi-turn Interaction with Tools and Language FeedbackarXiv:2309.10691Xingyao Wang, Zihan Wang, Jiateng Liu, et al.2023 · 141 citations
8. A Survey on Recent Advances in LLM-Based Multi-turn Dialogue SystemsACM Computing SurveysZihao Yi, Jiarui Ouyang, Zhe Xu, et al.2024 · 130 citations
9. Towards Large Reasoning Models: A Survey of Reinforced Reasoning with Large Language ModelsarXiv:2501.09686Fengli Xu, Qianyue Hao, Zefang Zong, et al.2025 · 120 citations
10. DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree SearcharXiv:2408.08152Huajian Xin, Z. Z. Ren, Junxiao Song, et al.2024 · 116 citations
11. DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic DataarXiv:2405.14333Huajian Xin, Daya Guo, Zhihong Shao, et al.2024 · 111 citations
12. PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical CompetitionConference on Neural Information Processing Systems (NeurIPS)George Tsoukalas, Jasper Lee, John Jennings, et al.2024 · 93 citations
13. InternLM-Math: Open Math Large Language Models Toward Verifiable ReasoningarXiv:2402.06332Huaiyuan Ying, Shuo Zhang, Linyang Li, et al.2024 · 90 citations
14. Goedel-Prover: A Frontier Model for Open-Source Automated Theorem ProvingarXiv:2502.07640Yong Lin, Shange Tang, Bohan Lyu, et al.2025 · 84 citations
15. Lean Workbook: A large-scale Lean problem set formalized from natural language math problemsConference on Neural Information Processing Systems (NeurIPS)Huaiyuan Ying, Zijian Wu, Yihan Geng, et al.2024 · 80 citations
16. LEGO-Prover: Neural Theorem Proving with Growing LibrariesarXiv:2310.00656Haiming Wang, Huajian Xin, Chuanyang Zheng, et al.2023 · 79 citations
17. BRIGHT: A Realistic and Challenging Benchmark for Reasoning-Intensive RetrievalarXiv:2407.12883Hongjin Su, Howard Yen, Mengzhou Xia, et al.2024 · 77 citations
18. Recursive Introspection: Teaching Language Model Agents How to Self-ImproveConference on Neural Information Processing Systems (NeurIPS)Yuxiao Qu, Tianjun Zhang, Naman Garg, et al.2024 · 75 citations
19. Cumulative Reasoning with Large Language ModelsarXiv:2308.04371Yifan Zhang, Jingqin Yang, Yang Yuan, et al.2023 · 74 citations
20. Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-CorrectionarXiv:2508.03613Yong Lin, Shange Tang, Bohan Lyu, et al.2025 · 67 citations
21. ArCHer: Training Language Model Agents via Hierarchical Multi-Turn RLarXiv:2402.19446Yifei Zhou, Andrea Zanette, Jiayi Pan, et al.2024 · 54 citations
22. From Decoding to Meta-Generation: Inference-time Algorithms for Large Language ModelsarXiv:2406.16838Sean Welleck, Amanda Bertsch, Matthew Finlayson, et al.2024 · 51 citations
23. Lean-STaR: Learning to Interleave Thinking and ProvingarXiv:2407.10040Haohan Lin, Zhiqing Sun, Sean Welleck, et al.2024 · 51 citations
24. TheoremLlama: Transforming General-Purpose LLMs into Lean4 ExpertsConference on Empirical Methods in Natural Language Processing (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 ProvingAnnual Meeting of the Association for Computational Linguistics (ACL)Ran Xin, Chenguang Xi, Jie Yang, et al.2025 · 49 citations
26. Formal Mathematical Reasoning: A New Frontier in AIarXiv:2412.16075Kaiyu Yang, Gabriel Poesia, Jingxuan He, et al.2024 · 49 citations
27. Chain of Ideas: Revolutionizing Research Via Novel Idea Development with LLM AgentsarXiv:2410.13185Long Li, Weiwen Xu, Jiayan Guo, et al.2024 · 47 citations
28. LLM-SR: Scientific Equation Discovery via Programming with Large Language ModelsarXiv:2404.18400Parshin Shojaee, Kazem Meidani, Shashank Gupta, et al.2024 · 47 citations
29. An In-Context Learning Agent for Formal Theorem-ProvingarXiv:2310.04353Amitayush Thakur, George Tsoukalas, Yeming Wen, et al.2023 · 47 citations
30. Seed-Prover: Deep and Broad Reasoning for Automated Theorem ProvingarXiv:2507.23726Luoxin Chen, Jinming Gu, Liankai Huang, et al.2025 · 46 citations
31. A Survey on Deep Learning for Theorem ProvingarXiv:2404.09939Zhaoyu Li, Jialiang Sun, Logan Murphy, et al.2024 · 46 citations
32. STP: Self-play LLM Theorem Provers with Iterative Conjecturing and ProvingarXiv:2502.00212Kefan Dong, Tengyu Ma2025 · 43 citations
33. Let's reward step by step: Step-Level reward model as the Navigators for ReasoningarXiv:2310.10080Qianli Ma, Haotian Zhou, Tingkai Liu, et al.2023 · 40 citations
34. A Survey of Frontiers in LLM Reasoning: Inference Scaling, Learning to Reason, and Agentic SystemsarXiv:2504.09037Zixuan Ke, Fangkai Jiao, Yifei Ming, et al.2025 · 39 citations
35. Lean Copilot: Large Language Models as Copilots for Theorem Proving in LeanarXiv:2404.12534Peiyang Song, Kaiyu Yang, Anima Anandkumar2024 · 39 citations
36. SciInstruct: a Self-Reflective Instruction Annotated Dataset for Training Scientific Language ModelsConference on Neural Information Processing Systems (NeurIPS)Dan Zhang, Ziniu Hu, Sining Zhoubian, et al.2024 · 37 citations
37. Multilingual Mathematical AutoformalizationarXiv:2311.03755Albert Q. Jiang, Wenda Li, Mateja Jamnik2023 · 37 citations
38. Magnushammer: A Transformer-Based Approach to Premise SelectionarXiv:2303.04488Maciej Mikuła, Szymon Tworkowski, Szymon Antoniak, et al.2023 · 35 citations
39. Process-Driven Autoformalization in Lean 4arXiv:2406.01940Jianqiao Lu, Yingjia Wan, Zhengying Liu, et al.2024 · 33 citations
40. FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language ModelsarXiv:2505.02735Zhouliang Yu, Ruotian Peng, Keyi Ding, et al.2025 · 31 citations
41. Aristotle: IMO-level Automated Theorem ProvingSuperIntelligence - Robotics - Safety & AlignmentTudor Achim, Alex Best, Alberto Bietti, et al.2025 · 29 citations
42. AutoVerus: Automated Proof Generation for Rust CodeProceedings of the ACM on Programming LanguagesChenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, et al.2024 · 28 citations
43. A Survey on Large Language Models for Mathematical ReasoningACM Computing SurveysPeng-Yuan Wang, Tian-Shuo Liu, Chenyang Wang, et al.2025 · 26 citations
44. Hilbert: Recursively Building Formal Proofs with Informal ReasoningarXiv:2509.22819Sumanth Varambally, Thomas Voice, Yanchao Sun, et al.2025 · 26 citations
45. Logical Reasoning in Large Language Models: A SurveyarXiv:2502.09100Hanmeng Liu, Zhizhang Fu, Mengru Ding, et al.2025 · 25 citations
46. HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem ProvingarXiv:2412.20735Yang Li, Dong Du, Linfeng Song, et al.2024 · 25 citations
47. StateFlow: Enhancing LLM Task-Solving through State-Driven WorkflowsarXiv:2403.11322Yiran Wu, Tianwei Yue, Shaokun Zhang, et al.2024 · 25 citations
48. Aligning LLMs with Individual Preferences via InteractionInternational Conference on Computational Linguistics (COLING)Shujin Wu, Yi R. Fung, Cheng Qian, et al.2025 · 24 citations
49. Lyra: Orchestrating Dual Correction in Automated Theorem ProvingarXiv:2309.15806Chuanyang Zheng, Haiming Wang, Enze Xie, et al.2023 · 24 citations
50. LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN proverarXiv:2407.17227Zijian Wu, Jiayu Wang, Dahua Lin, et al.2024 · 23 citations
51. Learning Formal Mathematics From Intrinsic MotivationConference on Neural Information Processing Systems (NeurIPS)Gabriel Poesia, David Broman, Nick Haber, et al.2024 · 23 citations
52. LLMSTEP: LLM proofstep suggestions in LeanarXiv:2310.18457Sean Welleck, Rahul Saha2023 · 22 citations
53. AI4Research: A Survey of Artificial Intelligence for Scientific ResearchScience China Information SciencesQiguang Chen, Mingda Yang, Libo Qin, et al.2025 · 21 citations
54. Leanabell-Prover: Posttraining Scaling in Formal ReasoningarXiv:2504.06122Jingyuan Zhang, Qi Wang, Xingguang Ji, et al.2025 · 21 citations
55. The Limits of Inference Scaling Through ResamplingarXiv:2411.17501Benedikt Stroebl, Sayash Kapoor, Arvind Narayanan2024 · 21 citations
56. TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language ModelsConference on Empirical Methods in Natural Language Processing (EMNLP)Jing Xiong, Jianhao Shen, Ye Yuan, et al.2023 · 21 citations
57. Graph2Tac: Online Representation Learning of Formal Math ConceptsarXiv:2401.02949Lasse Blaauwbroek, Miroslav Olšák, Jason Rute, et al.2024 · 19 citations
58. Proving Theorems RecursivelyConference on Neural Information Processing Systems (NeurIPS)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 ProvingarXiv:2503.03205Ruida Wang, Rui Pan, Yuxin Li, et al.2025 · 18 citations
60. FormalAlign: Automated Alignment Evaluation for AutoformalizationarXiv:2410.10135Jianqiao Lu, Yingjia Wan, Yinya Huang, et al.2024 · 18 citations
61. Machine learning and information theory concepts towards an AI MathematicianBulletin of the American Mathematical SocietyYoshua Bengio, Nikolay Malkin2024 · 18 citations
62. miniCTX: Neural Theorem Proving with (Long-)ContextsarXiv:2408.03350Jiewen Hu, Thomas Zhu, Sean Welleck2024 · 18 citations
63. APOLLO: Automated LLM and Lean Collaboration for Advanced Formal ReasoningConference on Neural Information Processing Systems (NeurIPS)Azim Ospanov, Farzan Farnia, Roozbeh Yousefzadeh2025 · 17 citations
64. Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal VerificationAnnual Meeting of the Association for Computational Linguistics (ACL)Chengwu Liu, Ye Yuan, Yichun Yin, et al.2025 · 17 citations
65. ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of DataConference on Neural Information Processing Systems (NeurIPS)Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, et al.2025 · 16 citations
66. Mathematical exploration and discovery at scalearXiv:2511.02864Bogdan Georgiev, Javier Gómez-Serrano, Terence Tao, et al.2025 · 16 citations
67. Solving Formal Math Problems by Decomposition and Iterative ReflectionarXiv:2507.15225Yichi Zhou, Jianqiu Zhao, Yongxin Zhang, et al.2025 · 16 citations
68. DafnyBench: A Benchmark for Formal Software VerificationarXiv:2406.08467Chloe Loughridge, Qinyi Sun, Seth Ahrenbach, et al.2024 · 15 citations
69. Kimina Lean Server: A High-Performance Lean Server for Large-Scale VerificationarXiv:2504.21230Marco Dos Santos, Hugues de Saxcé, Haiming Wang, et al.2025 · 14 citations
70. Prover Agent: An Agent-Based Framework for Formal Mathematical ProofsarXiv:2506.19923Kaito Baba, Chaoran Liu, Shuhei Kurita, et al.2025 · 14 citations
71. BioKGBench: A Knowledge Graph Checking Benchmark of AI Agent for Biomedical SciencearXiv:2407.00466Xinna Lin, Siqi Ma, Junjie Shan, et al.2024 · 12 citations
72. Proving Olympiad Algebraic Inequalities without Human DemonstrationsConference on Neural Information Processing Systems (NeurIPS)Chenrui Wei, Mengzhou Sun, Wei Wang2024 · 12 citations
73. Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical DefinitionsConference on Empirical Methods in Natural Language Processing (EMNLP)Lan Zhang, Marco Valentino, Andre Freitas2025 · 11 citations
74. IRIS: Interactive Research Ideation System for Accelerating Scientific DiscoveryAnnual Meeting of the Association for Computational Linguistics (ACL)Aniketh Garikaparthi, Manasi Patwardhan, Lovekesh Vig, et al.2025 · 11 citations
75. Proving Olympiad Inequalities by Synergizing LLMs and Symbolic ReasoningarXiv:2502.13834Zenan Li, Zhaoyu Li, Wen Tang, et al.2025 · 11 citations
76. ScienceBoard: Evaluating Multimodal Autonomous Agents in Realistic Scientific WorkflowsarXiv:2505.19897Qiushi Sun, Zhoumianze Liu, Chang Ma, et al.2025 · 11 citations
77. Consistent Autoformalization for Constructing Mathematical LibrariesConference on Empirical Methods in Natural Language Processing (EMNLP)Lan Zhang, Xin Quan, Andre Freitas2024 · 11 citations
78. REAL-Prover: Retrieval Augmented Lean Prover for Mathematical ReasoningarXiv:2505.20613Ziju Shen, Naohao Huang, Fanyi Yang, et al.2025 · 10 citations
79. Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum PhysicsarXiv:2510.12787Benjamin Breen, Marco Del Tredici, Jacob McCarran, et al.2025 · 9 citations
80. Rethinking Fine-Tuning when Scaling Test-Time Compute: Limiting Confidence Improves Mathematical ReasoningConference on Neural Information Processing Systems (NeurIPS)Feng Chen, Allan Raventos, Nan Cheng, et al.2025 · 9 citations
81. ReForm: Reflective Autoformalization with Prospective Bounded Sequence OptimizationarXiv:2510.24592Guoxin Chen, Jing Wu, Xinjie Chen, et al.2025 · 8 citations
82. Let's Reason Formally: Natural-Formal Hybrid Reasoning Enhances LLM's Math CapabilityConference on Empirical Methods in Natural Language Processing (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 PassesAnnual Meeting of the Association for Computational Linguistics (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 ModelsConference on Neural Information Processing Systems (NeurIPS)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-ProversarXiv:2509.06493Ran Xin, Zeyu Zheng, Yanchen Nie, et al.2025 · 7 citations
86. A Lean Dataset for International Math Olympiad: Small Steps towards Writing Math Proofs for Hard ProblemsarXiv:2411.18872Roozbeh Yousefzadeh, Xuenan Cao, Azim Ospanov2024 · 7 citations
87. A New Approach Towards AutoformalizationarXiv:2310.07957Nilay Patel, Rahul Saha, Jeffrey Flanigan2023 · 7 citations
88. EVOTOOL: Self-Evolving Tool-Use Policy Optimization in LLM Agents via Blame-Aware Mutation and Diversity-Aware SelectionAnnual Meeting of the Association for Computational Linguistics (ACL)Shuo Yang, Caren Han, Xueqi Ma, et al.2026 · 6 citations
89. Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem ProvingarXiv:2507.02726Matthieu Zimmer, Xiaotong Ji, Rasul Tutunov, et al.2025 · 5 citations
90. Premise Selection for a Lean HammerarXiv:2506.07477Thomas Zhu, Joshua Clune, Jeremy Avigad, et al.2025 · 5 citations
91. ImProver: Agent-Based Automated Proof OptimizationarXiv:2410.04753Riyaz Ahuja, Jeremy Avigad, Prasad Tetali, et al.2024 · 5 citations
92. Uncertainty Quantification in LLM Agents: Foundations, Emerging Challenges, and OpportunitiesAnnual Meeting of the Association for Computational Linguistics (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 CurationConference on Neural Information Processing Systems (NeurIPS)Zhenwen Liang, Linfeng Song, Yang Li, et al.2025 · 4 citations
94. EngiBench: A Benchmark for Evaluating Large Language Models on Engineering Problem SolvingFindings of the Association for Computational LinguisticsXiyuan 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 LeanAnnual Meeting of the Association for Computational Linguistics (ACL)Jordan Meadows, Lan Zhang, Andre Freitas2026
96. From Natural Language to Certified Geometry Proofs: A Survey of LLM-Augmented Verification and Neuro-Symbolic Theorem ProvingBig Picture v2: Crafting a Research NarrativeIoannis Tzachristas, Georgios Tzachristas2026
97. Reliable Use of Lemmas via Eligibility Reasoning and Section-Aware Reinforcement LearningAnnual Meeting of the Association for Computational Linguistics (ACL)Zhikun Xu, Xiaodong Yu, Ben Zhou, et al.2026

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

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/authors/peiyang-song/cited-by/