Mining Tactics for Automated Theorem Proving
ASE'26: 41th IEEE/ACM International Conference on Automated Software Engineering · October 2026
Yingfei Xiong
Full Professor with Tenure
- Programming Languages Lab · Vice Director
- Institute of Software · Vice Director
- School of Computer Science
- Peking University
Distinguished Member of ACM, Member of IFIP WG 2.4, IEEE, CCF
Office: Room 1431, Science Building # 1, Yanyuan Campus / 447 Wende Building, Changping New Campus
Email: xiongyf@pku.edu.cn
Phone: +86-10-62757008-12
My Free/Busy Information: HTML · ICS
Pronunciation of my name: [i:ŋfei] (yingfei) [ʃiɔŋ] (xiong)
News
More news →I was prompted to a full professor with tenure at Peking University. Thank everyone who helped during the process.
Mining Tactics for Automated Theorem Proving was accepted at ASE 2026. This paper is the first peer-reviewed publication of our new project aiming to optimizing symbolic provers with the intelligence of LLMs. We believe symbolic methods are more suitable to cope with symbolic problems compared to LLMs, but the human intelligence devoted so far is not enough to discover the most suitable symbolic methods, and we use LLMs to continue the devleopment. Through data-driven LLM-based strategy generation, our approach improves CoqHammer by more than 20% with only a small training set.
SemOpt: LLM-Driven Code Optimization via Rule-Based Analysis was accepted at TOSEM 2026. In this paper, we use an LLM to mine optimization strategies from history commits and formalize them as semgrep rules, and use these rules to find optimization opportunities in software projects and guide an LLM to perform optimization. We successfully optimized popular software projects that have been optimized by human experts for years, and some patches we generated have been accepted by developers.
HoarePrompt: Structural Reasoning About Program Correctness in Natural Language was awarded ACM SIGSOFT Distinguished Paper Award.
Reducing Cost of LLM Agents with Trajectory Reduction was accepted at FSE 2026. In this paper, we propose the first general trajectory reduction approach for reducing the cost of LLM agents by removing unnecessary contents in trajectories while retaining the reasoning capability of agents.
Recent Selected Publications
SemOpt: LLM-Driven Code Optimization via Rule-Based Analysis
TOSEM: ACM Transactions on Software Engineering and Methodology · July 2026
Reducing Cost of LLM Agents with Trajectory Reduction
FSE'26: The ACM International Conference on the Foundations of Software Engineering · July 2026
HoarePrompt: Structural Reasoning About Program Correctness in Natural Language
ICSE'26: 48th IEEE/ACM International Conference on Software Engineering · May 2026
✦ ACM SIGSOFT Distinguished Paper Award
PredicateFix: Repairing Static Analysis Alerts with Bridging Predicates
ICSE'26: 48th IEEE/ACM International Conference on Software Engineering · May 2026
Education & Employment
- 2026.08–NowPeking University · Full Professor with Tenure
- 2018.08–2026.07Peking University · Associate Professor with Tenure / Co-Appointed Research Professor
- 2012.04–2018.07Peking University · Research Professor in Young Talents Plan (Tenure-Track Assistant Professor Equivalence)
- 2009.12–2011.11University of Waterloo · PostDocAdvisors: Krzysztof Czarnecki
- 2006.10–2009.09The University of Tokyo · Ph.D.Advisors: Zhenjiang Hu, Masato Takeichi
- 2004.09–2006.09Peking University · Pre-Ph.D. CourseAdvisors: Fuqing Yang, Hong Mei
- 2000.09–2004.06University of Electronic Science and Technology of China · Bachelor Diploma of Computer Science
Academic and University Service
More →2027
Area Chair · ICSE 2028
2027
Area Chair · ISSTA 2027
2026-2028
Associate Editor-in-Chief · IEEE Transactions on Software Engineering
2026
Program Chair · CCF-PL 2026
2026
Associate Chair · PLDI 2027
2026
PC Member · POPL 2027
2026
PC Member · ICSE 2027
2026
Associate Chair · OOPSLA 2026