可微模糊逻辑中的算子选择

南京大学 KRistal 课题组 · 导师：赵一铮 副教授 · 2025 年 10 月 - 至今

• 项目：研究面向神经符号学习的可微逻辑算子选择问题
• 方法：结合在多种本体语料上的实证分析与训练动力学的理论研究
• 状态：第一作者论文已完成，投稿中

AI4Math：数学研究协作平台

微软亚洲研究院 (MSRA) · 导师：周子昱 · 2026 年 3 月 - 至今

• 项目：面向数学研究协作的 AI 辅助平台，融合自动定理证明、文献发现与证明助手集成
• 贡献：平台架构与知识基础设施的核心贡献者；开发面向数学推理与形式化验证工作流的 LLM 工具
• 状态：积极开发阶段，准备向数学社区演示

基于推理的细粒度强化学习 Web Agent

慕尼黑大学 (LMU Munich) · 导师：Dr. Yao Zhang · 2025 年 11 月 - 至今

• 问题：Web Agent 在需要感知、规划和有依据决策的多步推理任务上表现不佳
• 方法：设计细粒度 RL 框架，将复杂的 Web 任务分解为带结构化奖励信号的可学习子目标
• 技术：用于训练稳定性的新型奖励建模机制；面向多模态感知的图像锚定推理模块
• 产出：融合视觉语言模型与基于 RL 的任务分解的 agent 原型系统

面向偏好对齐的推理增强奖励模型

独立研究 · 导师：Dr. Zhen Han · 2025 年 7 月 - 至今

• 问题：RLHF 的标准奖励模型难以捕捉超越表层连贯性的推理质量
• 方法：通过结合拒绝采样、SFT 和 RL 的可扩展偏好数据流水线，将推理特定信号引入奖励建模
• 状态：实验进行中；论文撰写中

基于 LLM 与 Lean4 的交互式定理证明

UIUC ScaleML Lab · 导师：Prof. Tong Zhang · 2025 年 4 - 6 月

• 问题：LLM 能给出看似合理的证明步骤但缺乏形式化验证，限制了其在数学推理上的可靠性
• 方法：构建了一个集成 Lean4 与 LLM 的原型，在 MiniF2F 上进行交互式定理证明；带证明状态序列化与闭环精化的双向 (LLM ↔ Lean4) 流水线
• 成果：可运行原型 + 对常见失败模式（上下文违规、无效步骤建议）的分析，反馈到接口设计

HarmonyOS 智能体基准评测系统

华为 2012 实验室 · 主管：桂剑锋 · 2025 年 7 - 9 月

• 问题：需要对移动 OS 智能体在多样任务下的推理与适应性进行系统性评测
• 贡献：共同搭建 IntelliOS-agent 流水线的基准评测基础设施；将 HDC 调试工具与基于 LLM 的推理模块集成，并将 Python 依赖移植到 HarmonyOS
• 成果：已在华为内部 IntelliOS 项目中部署用于智能体评测

面向机器学习的量子内存架构

北卡罗来纳州立大学 QUEST Lab · 导师：Prof. Yuan Liu · 2024 年 7 - 11 月

• 问题：用于 ML 工作负载的量子计算硬件缺乏针对量子-经典混合执行优化的内存架构
• 方法：探索专门面向量子机器学习算法的量子内存设计
• 贡献：提出了面向量子系统上 ML 工作负载的优化计算架构；合作撰写了一篇论文（后由其他合作者继续推进）

机器学习模型中的对抗性后门

南京大学 COSEC 课题组 · 导师：张源 教授、仲盛 教授 · 2023 年 7 月 - 2024 年 12 月

• 问题：理解并防御神经网络训练流水线中的后门攻击
• 贡献：提出了新颖的后门注入利用机制；设计了恶意训练场景下的攻击实验
• 影响：该工作贡献于课题组在 ML 鲁棒性与可信性方向上的更广泛研究