档案 01 / 06 · § 自述档案 NO. 001

许英特Yingte Xu

博士研究生 · MPI-SP / 鲁尔大学波鸿

Email · github · 中文(母语) / 英文 / 日文(N1)

§ 自述

我的研究将形式化方法应用于量子计算的程序理论 —— 语义、验证技术与证明自动化。目标是一个实用的工具链,能够自然地编码并验证量子算法与协议。

我也对 AI 研究充满兴趣,尤其是线性注意力与多模态模型。我相信运行于边缘设备的个性化 AI 智能体将逐渐成为主流,这需要新的体系结构、训练方法与评估指标。

我着迷于系统的设计与构建 —— 从形式化推理与智能体,到创造性表达。

1999-10-23 生于江苏苏州 · 中华人民共和国

§ 教育与就职

马克斯·普朗克安全与隐私研究所 (MPI-SP) 2024 — 至今

研究助理

鲁尔大学波鸿 2024 — 至今

博士研究生

新冠疫情与签证问题使我在北京滞留两年。

马克斯·普朗克安全与隐私研究所 (MPI-SP) 2023 — 2024

远程实习

中国科学院软件研究所计算机科学国家重点实验室 2022 — 2023

实习

兰州大学 2018 — 2022

理学学士(物理学)

苏州中学 2015 — 2018

§ 论文

[LICS '26 (Accepted)] Complete Relational Logic for Infinite-Dimensional Quantum Programs with Unbounded Assertions

Gilles Barthe, Minbo Gao, Jam Kabeer Ali Khan, Matthijs Muis, Ivan Renison, Keiya Sakabe, Michael Walter, Yingte Xu, Tianshi Yu, Li Zhou

[CAV '25] D-Hammer: Efficient Equational Reasoning for Labelled Dirac Notation

Yingte Xu, Li Zhou, and Gilles Barthe

[POPL '25] Automating Equational Proofs in Dirac Notation

Yingte Xu, Gilles Barthe, and Li Zhou

[TOSEM '25] Refinement Calculus of Quantum Programs with Projective Assertions

Yuan Feng, Li Zhou, Yingte Xu, and Xiaoquan Xu

[ASPLOS '23] Verification of Nondeterministic Quantum Programs

Yuan Feng and Yingte Xu

§ 获奖

CHES 2025 深度学习侧信道分析挑战赛冠军 2025

CHES 2025 / GE Wars 组织委员会

国家奖学金 2019

中华人民共和国教育部

§ 研究项目

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 + 强化学习解决困难的等式推理问题。