档案 01 / 05 · § 自述 档案 NO. 001
许英特Yingte Xu
博士研究生 · MPI-SP / 鲁尔大学波鸿
§ 自述
我目前的研究将形式化方法应用于量子计算的程序理论 —— 语义、验证技术、证明自动化。目标是建立一个实用的端到端工具链(从验证到编译),自然地表达多数量子算法与协议。
我同时对机器学习与人工智能很感兴趣,尤其是语言模型与多模态模型。我相信运行于边缘设备的个性化 AI 智能体将逐渐成为主流,这需要新的体系结构、训练方法与评估指标。我正在朝着这个方向努力。
我着迷于系统的设计 —— 从形式化推理与智能体,到创造性世界与人类想象。我对探索新想法、表达创造性的有形作品充满热情。人们说我也是个业余艺术家。
§ 教育与就职
马克斯·普朗克安全与隐私研究所 (MPI-SP) 2024 — 至今
研究助理
鲁尔大学波鸿 2024 — 至今
博士研究生
新冠疫情与签证问题使我在北京滞留两年。
马克斯·普朗克安全与隐私研究所 (MPI-SP) 2023 — 2024
远程实习
中国科学院软件研究所 计算机科学国家重点实验室 2022 — 2023
实习
兰州大学 2018 — 2022
理学学士(物理学)
苏州中学 2015 — 2018
§ 论文
§ 获奖
CHES 2025 深度学习侧信道分析挑战赛 冠军 2025
CHES 2025 / GE Wars 组织委员会
国家奖学金 2019
中华人民共和国教育部
§ 项目
Fanal 2025-2026
一个基于 Lean 的项目,构建用于编码与验证量子程序的实用工具。支持完整的具体语法与量子数组。实验了自动形式化流水线。我为项目网站配备了 AI chatbot 助手。
D-Hammer 2025
一个 C++ 工具,高效判定带标号的 Dirac 记号方程。
DiracDec 2024-2025
Dirac 记号方程证明自动化的原型,使用 Mathematica 实现,集成其实数计算代数系统。
EquationNN 2025
尝试用 LLM + 强化学习解决困难的等式推理问题。
QRefine 2024
支持程序精化的量子程序开发 IDE 原型,Python 实现。
NQPV 2023
非确定性量子程序验证的工具。