Home
I am Andrew, Jingkun Ma, a second-year Ph.D. student in Computer Science at the University of Macau and a member of the NLP2CT Lab, supervised by Prof. Derek F. Wong. I am deeply grateful to Prof. Derek F. Wong for his invaluable supervision, support, and academic guidance throughout my doctoral journey. I would also like to express my sincere gratitude to Runzhe Zhan for his generous mentorship, insightful discussions, and continuous encouragement, all of which have played an important role in shaping my research interests and development. In addition, I have greatly benefited from the valuable insights and guidance of Dr. Hou Pong Chan from Alibaba DAMO Academy. My research focuses on building trustworthy and reasoning-driven AI systems. I am particularly interested in formal theorem proving, agentic systems, and culturally aligned AI, with applications in healthcare, education, and personalized decision support. Beyond research, I am the founder of the Artificial Intelligence and Data Science Society (AIDSS) at the University of Macau, where I serve as Chief Academic Mentor.
Research Group Overview
I currently mentor a growing group of undergraduate and master's students working on formal theorem proving, compositional reasoning, agents, medical AI, multi-modal LLMs, Math + AI, and cultural alignment.
Recent mentee outcomes include 2026 master's admissions to Johns Hopkins University, HKUST, CUHK, and the University of Macau.
Highlighted students:
- Yuchao Wang: Formal theorem proving; co-authored FIPO-Prover, accepted to ICML 2026 Workshop AI4Math with a Spotlight
- Yang Li: Multi-modal LLM and Math + AI; co-authored VisAidMath, which received the Best Paper Award at NeurIPS 2025 Workshop VLM4RWD
- Rongsheng Zhang: Math + AI, admitted to Johns Hopkins University M.S. (2026)
- Lingyi Ou: Medical AI, admitted to HKUST M.S. (2026)
- Xingchen Chen: Medical AI, admitted to University of Macau M.S. (2026)
- Zhexuan Zhang: Cultural Alignment, admitted to CUHK M.S. (2026)
More details can be found on the Research Group page.
Selected Publications
View All ->
VisAidMath: Benchmarking Visual-Aided Mathematical Reasoning
Jingkun Ma, Runzhe Zhan, Yang Li, Di Sun, Hou Pong Chan, Lidia S. Chao, Derek F. Wong
A benchmark for visual-aided mathematical reasoning, accepted by ACL 2026 and also recognized with the Best Paper Award at the 1st VLM4RWD Workshop at NeurIPS 2025.
FIPO-Prover: Formalization-Oriented Informal Proof Optimization for Efficient Formal Theorem Proving
Jingkun Ma*, Yuchao Wang*, Yujia Huo, Derek F. Wong
FIPO-Prover bridges the gap between informal reasoning and formal verification by optimizing an intermediate proof representation that is diagnosable, repairable, and guided by verifier feedback.
Idioms Understood, Yet Translated Literally: Diagnosing Literal Translation Bias in Multilingual LLMs
Yanming Sun, Runzhe Zhan, Shuo Wang, Jingkun Ma, Yu Chao, Lidia S. Chao, Derek F. Wong
LLMs can recognize and interpret idioms yet still translate them literally, and we diagnose this literal translation bias through a cascaded framework and representation-level intervention.
Lean2Isabelle: Factorized Cross-Assistant Proof Translation
Guanyu Liu*, Jingkun Ma*, Derek F. Wong
Lean2Isabelle factorizes Lean-to-Isabelle proof translation into statement prediction and proof generation, showing that verifier-guided RL and Lean proof inputs improve semantically accepted cross-assistant proof migration.
From Local Success to Composite Failure: Diagnosing Local-to-Composite Transfer in Mathematical Reasoning
Jingkun Ma*, Haoran Wang*, Yang Li‡, Rongsheng Zhang‡, Derek F. Wong
We introduce a paired diagnostic framework showing that mathematical reasoning models can solve local components yet fail when those components are bound into composed dependency structures.
News
Two of our papers, FIPO-Prover and Lean2Isabelle, have been accepted to the ICML 2026 Workshop AI4Math, with FIPO-Prover selected as a Spotlight. We will present them on site. See you in Seoul, Korea 
!
Our paper VisAidMath: Benchmarking Visual-Aided Mathematical Reasoning has been accepted to ACL 2026. We will also present it on site in San Diego, California, United States 
.
Yang Li and Chao Tang are conducting Summer Research 2026 at Westlake University 
.
Ziyan Hong and Yangshen Pan are conducting Summer Research 2026 at the University of Macau 
.
Rongsheng Zhang has been admitted to the M.S. program at Johns Hopkins University 
.
Lingyi Ou has been admitted to the M.S. program at HKUST 
.
Xingchen Chen has been admitted to the M.S. program at the University of Macau .
Zhexuan Zhang has been admitted to the M.S. program at CUHK 
.
VisAidMath received the Best Paper Award at the first VLM4RWD Workshop at NeurIPS 2025.
Wenxi Ao and Lingyi Ou conducted Summer Research 2025 at the University of Macau .
Started my Ph.D. in Computer Science at the University of Macau.
Released Yu Sheng, a human-in-the-loop Classical Chinese poetry generation system, at EACL 2023 Demo.