档案 01 / 10 · § 自述 档案 NO. 001
许英特Yingte Xu
博士研究生 · MPI-SP / 鲁尔大学波鸿
§ 自述
我的研究将形式化方法应用于量子计算的程序理论 —— 语义、验证技术与证明自动化。目标是一个实用的工具链,能够自然地编码并验证量子算法与协议。近期工作也探索以机器学习与基于大语言模型的编程智能体作为迈向这一自动化的途径。
我也对 AI 研究充满兴趣,尤其是线性注意力与多模态模型。我相信运行于边缘设备的个性化 AI 智能体将逐渐成为主流,这需要新的体系结构、训练方法与评估指标。
我着迷于系统的设计与构建 —— 从形式化推理与智能体,到创造性表达。
§ 教育与就职
马克斯·普朗克安全与隐私研究所 (MPI-SP) 2024 — 至今
研究助理
鲁尔大学波鸿 2024 — 至今
博士研究生
新冠疫情与签证问题使我在北京滞留两年。
马克斯·普朗克安全与隐私研究所 (MPI-SP) 2023 — 2024
远程实习
中国科学院软件研究所 计算机科学国家重点实验室 2022 — 2023
实习
兰州大学 2018 — 2022
理学学士(物理学)
苏州中学 2015 — 2018
§ 论文
§ 研讨会论文
PLanQC 2026,与 POPL 2026 同期举办
§ 获奖
CHES 2025 深度学习侧信道分析挑战赛 冠军 2025
CHES 2025 / GE Wars 组织委员会
首届全国"挑战杯"量子计算竞赛 冠军 2022
中国科学院 量子计算云平台
国家奖学金 2019
中华人民共和国教育部
§ 研究项目
Fanal 2025-2026
用 Lean 4 进行量子程序基础形式化与验证的项目。
D-Hammer 2025
一个 C++ 工具,高效判定带标号的 Dirac 记号方程。
DiracDec 2024-2025
Dirac 记号方程证明自动化的原型,使用 Mathematica 实现,集成其实数计算代数系统。
QRefine 2024
支持程序精化的量子程序开发 IDE 原型,Python 实现。
NQPV 2023
非确定性量子程序验证的工具。
§ 个人实验项目
AI4SMT 2026
用编程智能体优化 SMT 求解器的启发式策略。AI 智能体反复修改并重新编译 cvc5 求解器,保留每一次能提升 SMT-COMP 分数且不牺牲可靠性的改动。训练得到的求解器已报名 SMT-COMP 2026。
EquationNN 2025
尝试用 LLM + 强化学习解决困难的等式推理问题。
§ 教学
讲师 2024
量子计算人才培养暑期学校(中国科学技术大学,线上)
助教 2022-2023
助教 2019
线性代数(兰州大学)
§ 学术服务
副审稿人 ICTAC 2026(理论计算方面国际学术研讨会)
§ 技术技能
- 编程语言
- Python, C/C++, OCaml, JavaScript, Mathematica, MATLAB
- 形式化方法与证明自动化
- Rocq (Coq), Lean 4, term-rewriting engines, SMT and first-order (Vampire) solvers
- 机器学习
- PyTorch, Hugging Face (Transformers, Datasets, Accelerate), NumPy, Pandas, Numba
- 系统与工具
- Docker, OpenTelemetry, reactive pipelines (ReactiveX / RxPY), WebSockets, LLM coding-agent workflows