Symbolic Computation × ML Mechanics

KRistal Group, Nanjing University · Advisor: Prof. YiZheng Zhao · Oct 2025 - Present · manuscript under submission

AI4Math: Mathematical Research Collaboration Platform

Microsoft Research Asia (MSRA) · Advisor: Ziyu Zhou · Mar 2026 - Present

Reasoning-Based WebAgents with Reinforcement Learning

Ludwig Maximilian University of Munich · Advisor: Dr. Yao Zhang · Nov 2025 - Present

Formal Methods × World Models for Agents

Independent research · with Dr. Yao Zhang (LMU Munich) · 2026 - Present

Mechanistic Analysis of Agent Harnesses

Ludwig Maximilian University of Munich · Advisor: Dr. Yao Zhang · 2026 - Present

Quantum Bosonic Encoding × Attention Mechanisms

Independent research · with Prof. Yuan Liu (NC State) · 2026 - Present

Reasoning-Enhanced Reward Models for Preference Alignment

Independent Research · Advisor: Dr. Zhen Han · Jul 2025 - Present · manuscript in preparation

Interactive Theorem Proving with LLMs and Lean4

ScaleML Lab, UIUC · Advisor: Prof. Tong Zhang · Apr - Jun 2025

• Problem: LLMs can propose plausible proof steps but lack formal verification, limiting their reliability for mathematical reasoning
• Approach: Built a prototype integrating Lean4 with LLMs for interactive theorem proving on MiniF2F; bidirectional pipeline (LLM ↔ Lean4) with proof-state serialization and closed-loop refinement
• Outcome: Working prototype + analysis of common failure modes (context violations, invalid step proposals) informing interface design

Benchmarking System for HarmonyOS Intelligent Agents

Huawei 2012 Labs · Supervisor: JianFeng Gui · Jul - Sept 2025

• Problem: Need for systematic evaluation of reasoning and adaptability in mobile OS agents across diverse tasks
• Contributions: Co-developed benchmarking infrastructure for the IntelliOS-agent pipeline; integrated HDC debugging tools with LLM-based reasoning modules and ported Python dependencies to HarmonyOS
• Outcome: Deployed in Huawei's internal IntelliOS project for agent evaluation

Quantum Memory Architectures for Machine Learning

QUEST Lab, NC State University · Advisor: Prof. Yuan Liu · Jul - Nov 2024

• Problem: Quantum computing hardware for ML workloads lacks optimized memory architectures tailored to quantum-classical hybrid execution
• Approach: Explored quantum memory designs specifically for quantum machine learning algorithms
• Contributions: Proposed optimized computational architecture for ML workloads on quantum systems; co-authored a manuscript later continued by collaborators

Adversarial Backdoors in Machine Learning Models

COSEC Research Group, Nanjing University · Advisors: Prof. Yuan Zhang, Prof. Sheng Zhong · Jul 2023 - Dec 2024

• Problem: Understanding and defending against backdoor attacks in neural network training pipelines
• Contributions: Proposed novel exploit mechanism for backdoor injection; designed attack experiments on malicious training scenarios
• Impact: Work contributed to group's broader research on ML robustness and trustworthiness