Haocheng Wang (王浩丞)

PhD @ HKUST(GZ) | Visiting Researcher @ ETH Zürich

I am a PhD student at HKUST(GZ) and a Visiting Researcher at ETH Zürich, focusing on formal mathematical reasoning and verifiable code generation.

日拱一卒 · Keep pounding the rock

Email GitHub Google Scholar CV
Haocheng Wang

About Me

I am a direct doctoral student at DSA Thrust, HKUST(GZ) supervised by Prof. Zhijiang Guo. Currently, I am a Visiting Researcher at ETH Zürich (D-INFK), working with Prof. Rasmus Kyng and Dr. Sorrachai Yingchareonthawornchai on verifiable autoformalization and formal reasoning in Theoretical Computer Science. Previously, I was a Student Researcher at ByteDance Seed and DeepSeek AI.

I graduated with a Bachelor's degree (Honours) in Mathematics and Applied Mathematics from Xiamen University in 2025. My undergraduate thesis focused on formalizing Auction Theory, supervised by Prof. Ma Jiajun.

Research Interests

My research focuses on:

News

Apr. 2026One paper accepted at ICML 2026.
Mar. 2026Co-organizing the 3rd AI4Math Workshop at ICML 2026 as Program Chair.
Jan. 2026Started my Ph.D. at DSA Thrust, HKUST(GZ), supervised by Prof. Zhijiang Guo.
Aug. 2025Joined ETH Zürich (D-INFK) as a Visiting Researcher.
Apr. 2025DeepSeek-Prover-V2 and ProverBench are released.
Jan. 2025Joined ByteDance Seed as a Student Researcher.
Jun. 2024Joined DeepSeek AI as a Student Researcher.

Featured Projects

FormalRx

FormalRx: Rectify and eXamine Semantic Failures in Autoformalization

Haocheng Wang, Baiyu Huang, Yingjia Wan, Xiao Zhu, Xiaoyang Liu, Yinya Huang, Zhijiang Guo

A diagnostic evaluation framework for autoformalization with a 28-class SCI Error Taxonomy. FormalRx-8B jointly performs verdict, error categorization, localization, and correction in one forward pass.

Page Dataset Challenge
ICML 2026
DeepSeek-Prover-V2

DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition

Z.Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z.F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao, Daya Guo, Chong Ruan

671B-sized model achieving SOTA on miniF2F (88.9%) and PutnamBench (47/658) via RL with subgoal decomposition.

Paper Model Dataset
ArXiv Preprint, 2025
DeepSeek-Prover-V1.5

DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search

Huajian Xin, Z.Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang, Zhibin Gou, Z.F. Wu, Fuli Luo, Chong Ruan

Hybrid approach combining LLMs and Monte-Carlo tree search. SOTA on miniF2F (63.5%) and ProofNet (25.3%).

Paper OpenReview Code
ICLR 2025
Formal Math

Solving Formal Math Problems by Decomposition and Iterative Reflection

ByteDance Seed Team

Training-free agent framework enabling general-purpose LLMs to solve complex formal proofs in Lean 4.

Paper
ArXiv Preprint, 2025

Professional Experience

Scientific Assistant I
ETH Zürich
Aug 2025 - Present · Zürich, Switzerland
Student Researcher
ByteDance Co., Ltd.
Jan 2025 - Jul 2025 · Shanghai, China
  • Built Scoring & Self-refinement agent pipeline for Natural Language Proof
  • Proposed sketch-incorporated long horizon CoT formal reasoning method
  • Led data initiatives for DeltaProver
Student Researcher
DeepSeek AI Co., Ltd.
June 2024 - Sep 2024 · Beijing, China
  • Contributed to DeepSeek-Prover-V1.5 and V2 model development
  • Developed ProverBench, a domain-categorized benchmark with 325 problems for evaluating LLM theorem proving

Education

Xiamen University

Sep 2020 - Jun 2025

Bachelor of Science in Mathematics and Applied Mathematics (Honours)

Final Thesis: Formalization of Auction Theory [GitHub]

I'm grateful that my alma mater shared moments from my non-linear journey through "Not Good at Math", Yet Pursuing a PhD [EN / 中文].

Beyond academics, I care deeply about volunteering. My story on the frontline of the Zhengzhou 7·20 flood relief efforts was also shared [中文].

Academic Service

Program Chair

Area Chair

Conference Reviewer

Teaching Assistant

Engagements

Invited Talks

Workshops

Contact

Feel free to reach out to me:

haocheng [dot] wang [at] inf [dot] ethz [dot] ch

hcwang942 [at] gmail [dot] com

OAT Z29, Andreasstrasse 5, Zürich

Visitor Map