🎉 New SOTA for theorem proving model!
Our new open-source LLMs for Lean 4 theorem proving. See our post in X
☕️Suozhi Huang
Grad Student Researcher
Yao Class, Tsinghua University
About Me
Hi, I’m Suozhi, first year Ph.D. student in Princeton University studying in ECE department. My current interest is in LLM agents which can solve specific hard tasks that human can’t even handle.
I did my undergrad Computer Science(major in AI) at Yao Class in Tsinghua University. My past research interests included automated theorem proving, language model reasoning and AI for science(including math, physics and biochem). I am fortunate to work with Prof. Anima Anandkumar at Caltech. I am also a member of Internlm-Math team, developing llm formal math provers. I start my research journey from robotics.
Interests
- Artificial Intelligence
- Automated Theorem Proving
- Reasoning in LLMs
Education
B.E. Computer Science (Major in AI)
Yao Class, Tsinghua University
📚 My Research
My research interests include LLMs and agentic tasks. Additionally, I aim to incorporate reinforcement learning (RL) and real world high dimensional data to optimize the agent strategy, enabling systems to learn from expert strategies and improve their performance over time.
My goal is to create robust frameworks that leverage LLM capabilities for hard decision problems.
Please reach out to collaborate 😃
Publications
(2025).
LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction.
In ICLR 2025.
(2024).
InternLM2.5-StepProver: Advancing Automated Theorem Proving via Expert Iteration on Large-Scale LEAN Problems.
Tech Report.
(2024).
A Knowledge–Data Dual‐Driven Framework for Predicting the Molecular Properties of Rechargeable Battery Electrolytes.
In Angewandte Chemie.
(2024).
ActFormer: Scalable Collaborative Perception via Active Queries.
In ICRA 2024.
Recent News