LLM & Coding Agents
Interactive agents, trajectory data, and rigorous evaluation for reliable tool use on real-world software tasks.
I am currently an AI researcher in Hong Kong, building LLM agents that reason, prove, and code. My work connects agent design, Lean-based verification, foundation-model post-training, and large-scale diffusion language models.
I received my Ph.D. from The Chinese University of Hong Kong, supervised by Prof. Hong Cheng, with a research focus on LLMs and data mining. I earned my B.Sc. with First Class Honors in Computer Science from Hong Kong Baptist University under Prof. Jianliang Xu. I also held research appointments at the University of Auckland and Aalborg University.
Research internships: I welcome enquiries from students with strong computer science and mathematics backgrounds who are interested in LLM agents for coding and mathematical reasoning, formal reasoning, or reinforcement learning. Please email your CV and research interests.
Interactive agents, trajectory data, and rigorous evaluation for reliable tool use on real-world software tasks.
Lean-integrated theorem proving, autoformalization, and reasoning agents with executable verification.
SFT, DPO, and GRPO for stronger reasoning and more reliable model behavior.
Large-scale pretraining and stable reinforcement learning for discrete diffusion LMs.
I led the development of a theorem-proving agent that achieved gold-medal-level performance on the 2026 IMO problems, state-of-the-art Pass@1 on MathOlympiad (86%) and Putnam (88%), and first prize in the ICML 2026 AI4Math Challenge.
Selected work in ICML, ICLR, NeurIPS, SIGMOD, EMNLP, and ICDE. See Google Scholar for the complete list.
† Corresponding author · Brief: challenge, method, evidence.
Challenge. GRPO-style reinforcement learning becomes unstable for diffusion language models because sequence likelihoods are intractable; noisy importance ratios can bypass clipping, trigger gradient spikes and policy drift, then collapse rewards.
Method. StableDRL adds unconditional clipping and self-normalization, constraining updates to the convex hull of per-sample gradients; staircase attention extends leakage-free estimation to block diffusion.
Evidence. It enables stable full-parameter training of full-attention and block models for more than 1,000 steps and leads all four evaluated LLaDA-8B reasoning benchmarks on average.
Challenge. Informal LLM math reasoning is flexible but accumulates logical gaps, while formal provers are rigorous but restrictive; existing agents struggle to combine exploration with verification efficiently.
Method. HERMES interleaves natural-language reasoning with Lean 4 verification of selected critical steps, using autoformalization, proof or counter-proof feedback, and retrieval memory to preserve cross-step consistency.
Evidence. Across four benchmarks, it consistently improves base-model accuracy; on the hardest datasets it delivers up to a 40% accuracy gain while using 80% fewer total inference FLOPs than reward-based approaches.
Challenge. Most LLM theorem provers require expert-written Lean statements, preventing direct use on real-world mathematics expressed in natural language; successful compilation alone cannot detect semantic mistranslations.
Method. Mathesis builds an end-to-end pipeline with a GRPO/DPO-trained autoformalizer, LeanScorer for syntactic and semantic selection, and a specialized prover that produces machine-checked Lean proofs.
Evidence. It scores 64% on MiniF2F and a state-of-the-art 18% on the new 488-problem Gaokao-Formal benchmark; its autoformalization achieves a 22% higher pass rate than the strongest baseline.
Challenge. Autoformalizers can produce Lean code that compiles yet changes the meaning or dependency structure of the original human proof, making it unreliable for mathematical verification.
Method. ProofFlow builds a directed acyclic graph of proof-step dependencies, formalizes each step as a Lean lemma, and completes tactics using only intended premises; ProofScore jointly measures syntax, semantics and structural fidelity.
Evidence. At pass@5 on the 184-problem ProofFlowBench, the best setup reaches a 0.545 ProofScore versus 0.123 for full-proof and 0.072 for stepwise baselines, plus 37.5% proof-level syntax accuracy.
Challenge. Masked diffusion LMs waste computation on MASK and PAD tokens, assume fixed-length sequences, and cannot reposition earlier decisions, limiting efficiency, variable-length generation and self-correction.
Method. DID replaces masking and unmasking with a continuous-time deletion-insertion diffusion process. It learns token-position insertion scores with a likelihood-bounded DISE objective and computes subsequence-count targets using parallel dynamic programming.
Evidence. On fixed- and variable-length benchmarks, DID improves modeling and sampling quality over masked-diffusion and insertion-based baselines while accelerating training by up to 3.42× and inference by up to 3.79×.
Challenge. Masked diffusion models predict multiple dimensions independently at each denoising step, missing cross-dimensional dependencies and degrading generation quality when only a few steps are used.
Method. VADD introduces a latent variable into the denoising distribution to capture correlations, then jointly trains the generator and an auxiliary recognition model through a variational lower bound. A specialized transformer preserves parallel inference.
Evidence. Across 2D synthetic data, pixel-level images and text, VADD consistently produces higher-quality samples than masked-diffusion baselines with few denoising steps while retaining efficient generation.
Challenge. Existing attributed-hypergraph clustering methods rely on costly matrix factorization and require the cluster count upfront, so estimation errors can sharply reduce clustering quality.
Method. AHRC fuses hypergraph topology and node attributes into a graph representation, optimizes multi-hop modularity without a preset cluster count, and uses hypergraph sparsification for scalability.
Evidence. On 10 real hypergraphs, AHRC averages 20% higher F-measure, 24% higher ARI, 26% higher Jaccard similarity and 10% higher purity, while running 5.5× faster than the state-of-the-art method.
Challenge. Few-step masked diffusion relies on hand-designed mask schedules, with little theory explaining which schedule minimizes generation cost.
Method. The paper casts masked diffusion as discrete optimal transport, proves several energy objectives equivalent, derives a closed-form optimality condition, and uses Beta-distribution CDFs to reduce schedule tuning to two parameters.
Evidence. This enables post-training, task-adaptive tuning without model changes; energy-inspired schedules outperform common handcrafted schedules, particularly for low-step sampling across synthetic, language, code and mathematical-reasoning benchmarks.
Challenge. Text clustering often misassigns ambiguous boundary points and outliers; earlier LLM-assisted methods can require many API calls, domain-specific tuning or generalize poorly.
Method. LLMEdgeRefine starts with K-means, groups distant points into super-points for iterative agglomerative reclustering, then asks an LLM to semantically assess and reassign only likely boundary errors.
Evidence. Across seven datasets, it consistently improves ACC and NMI; average ACC gains over six baselines range from 10.9% to 17.3%, while reducing LLM prompts and avoiding model fine-tuning.
Challenge. Existing hypergraph modularity either treats a hyperedge's cluster alignment as all-or-nothing, losing groupwise signal, or models partial alignment too expensively to scale.
Method. The Hyperedge Expansion Model provides an efficient random null model; Partial Innerclusteredge modularity captures partial alignment, and the PIC algorithm optimizes it with two search-space pruning techniques.
Evidence. Across real hypergraphs, PIC surpasses eight state-of-the-art methods in quality and scalability, running four orders of magnitude faster on average and up to five orders faster.
Challenge. Frequent interactions reactivate edges while inactivity makes them decay, so clustering a massive dynamic network must track temporal activeness, structural cohesion and multiple query granularities without costly global recomputation.
Method. A global decay factor avoids decay-triggered updates; a maintainable distance metric combines structure and activeness, while a hierarchical distance index supports global or local clustering and zoom-in or zoom-out queries.
Evidence. Query work depends on result size rather than graph size, index storage is near-linear, and activation updates are up to six orders of magnitude faster than rebuilding the index.
Challenge. Indoor routing must find diverse, keyword-relevant paths within a distance budget; complex room-and-door topology makes relevance scoring and exhaustive search expensive.
Method. IKRQ distinguishes identity and thematic keywords, uses bidirectional mappings, defines prime routes to remove redundant paths, and applies distance and top-k pruning through topology- and keyword-oriented search.
Evidence. On synthetic and real venues, both algorithms are efficient; real queries complete in under 500 milliseconds, while prime-route pruning makes the topology-oriented method three orders of magnitude faster in a tested setting.