Hi! I’m Yihao Chen, though most people call me Arnie. I studied Software Engineering at East China Normal University in Shanghai, and these days I’m a research assistant working on formal verification.
What I work on
Model checking for quantum many-body systems. Quantum states of long spin chains are often written as matrix product states (MPS). Together with my collaborators, I helped design Linear Chain Logic, a way to specify properties that should hold no matter how long the chain gets, and built the model checker for it. That work appeared at CAV 2026, and the artifact I led picked up every Artifact Evaluation badge. Right now I’m extending the framework to chains with open boundaries, where the boundary changes the long-run behavior in interesting ways.
Automata for probabilistic verification. I also work on turning LTL specifications into automata that play well with Markov decision processes. My favorite part of that project was finding counterexamples to the original correctness argument: breaking a proof is a surprisingly good way to understand it.
Generative models (where I started). Before verification, I worked on diffusion models: image inpainting, fixing over-fitting when teaching DreamBooth a new art style, and adversarial watermarks that protect artwork from being copied by fine-tuned Stable Diffusion models.
A few other things
- I’ve been a TA for Theory of Computation and Digital Image Processing, and I still enjoy explaining automata to anyone who’ll listen.
- I write most things in Python, but I have a soft spot for OCaml and Coq.
Say hi
The best way to reach me is by email at arniechan595 [at] gmail [dot] com.