FILE 01 / 10 · § SELF ARCHIVE NO. 001

Yingte Xu许英特

PhD candidate · MPI-SP / Ruhr University Bochum

Email · github · Chinese (native) / English / Japanese (N1)

§ Self

Yingte's research applies formal methods to study the programming theory for quantum computing, including semantics, verification techniques, and proof automation. The aim is a practical toolchain that can naturally encode and verify quantum algorithms and protocols. Recent work also explores machine learning and LLM-based coding agents as a means toward this automation.

He is also drawn to AI research, especially in linear attention and multimodal models. He believes persona AI agents on edge devices will become prominent, demanding new architectures, training methods, and evaluation metrics.

He is fascinated by the design and building of systems, from formal reasoning and intelligent agents to creative expression.

Born 1999-10-23 · Suzhou, Jiangsu · P.R. China

§ Education & Employment

Max Planck Institute for Security and Privacy (MPI-SP) 2024 — now

Research Assistant

Ruhr University Bochum 2024 — now

PhD Student

The COVID pandemic and visa issues kept Yingte in Beijing for two years.

Max Planck Institute for Security and Privacy (MPI-SP) 2023 — 2024

Remote Internship

State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences 2022 — 2023

Internship

Lanzhou University 2018 — 2022

Bachelor of Science (Physics)

Suzhou High School 2015 — 2018

§ Publications

[LICS '26] 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

§ Workshop Papers

[PLanQC '26] A Unified Assertion-Based Framework for Classical-Quantum Program Verification

Yingte Xu

PLanQC 2026, co-located with POPL 2026

§ Awards

Winner of CHES 2025 Deep Learning SCA Battle 2025

CHES 2025, GE Wars Organization Committee

Winner of the First National "Challenger Cup" Quantum Computing Competition 2022

Quantum Computing Cloud Platform, Chinese Academy of Sciences

National Scholarship 2019

Ministry of Education of the People's Republic of China

§ Research Projects

Fanal 2025-2026

A Lean 4 project for the foundational formalization and verification of quantum programs.

D-Hammer 2025

A C++ tool that efficiently decides equations of labelled Dirac notations.

DiracDec 2024-2025

A prototype for proof automation of Dirac notation equations. Implemented in Mathematica, integrated with its computer algebra system for reals.

QRefine 2024

A prototype IDE for quantum program development with program refinement support, implemented in Python.

NQPV 2023

Artifact for verification of nondeterministic quantum programs.

§ Personal Experiments

AI4SMT 2026

Optimizing SMT-solver heuristics with a coding agent. An AI agent repeatedly edits and rebuilds the cvc5 solver, keeping every change that improves its SMT-COMP score without trading away soundness. The trained solver is registered for SMT-COMP 2026.

EquationNN 2025

An attempt to solve hard equational reasoning problems using LLM + Reinforcement Learning.

§ Teaching

Lecturer 2024

Quantum Computing Talent Development Summer School (USTC, online)

Teaching Assistant 2022-2023

Teaching Assistant 2019

Linear Algebra (Lanzhou University)

§ Academic Service

Subreviewer ICTAC 2026 (International Colloquium on Theoretical Aspects of Computing)

§ Technical Skills

Programming Languages: Python, C/C++, OCaml, JavaScript, Mathematica, MATLAB
Formal Methods & Proof Automation: Rocq (Coq), Lean 4, term-rewriting engines, SMT and first-order (Vampire) solvers
Machine Learning: PyTorch, Hugging Face (Transformers, Datasets, Accelerate), NumPy, Pandas, Numba
Systems & Tooling: Docker, OpenTelemetry, reactive pipelines (ReactiveX / RxPY), WebSockets, LLM coding-agent workflows