Publications
Selected publications and research outputs.
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.
Activate Integrated Controllable Generation with Soft Prompt
Jingkun Ma, Runzhe Zhan, Derek F. Wong, Lidia S. Chao
A parameter-efficient soft-prompt method for controllable generation under complex multi-attribute settings.
