Xiaoyang Liu 刘晓洋

I am a second-year PhD candidate advised by Prof. Tao Luo at School of Mathematical Sciences, Shanghai Jiao Tong University (SJTU).

I have been interning at the Wizard Intelligence Learning Lab (WILL) as a post-training researcher since July 2026.

Research

LLMs · Lean · AI4Math · Verifiable Code Generation

I develop verifiable AI systems that bridge informal reasoning and formal verification. My research addresses the core challenges of trustworthy reasoning through scalable autoformalization, faithful evaluation and diagnosis, and rigorous adversarial testing.

Autoformalization

Bootstrapping autoformalization through scalable data synthesis in ATLAS and structural operator-tree refinement in DSR.

Evaluation & Diagnosis

Building faithful structural-semantic metrics with ASSESS and white-box diagnostic models with FormalRx.

Specification Testing

Scaling adversarial test suites with VeriScale to rigorously assess the soundness and completeness of formal specifications.

Publications

* Equal contribution. † Corresponding author.

ICML 2026 · AI4Math Workshop

VeriScale: Adversarial Test-Suite Scaling for Verifiable Code Generation

Yifan Bai^*, Xiaoyang Liu^*, Zihao Mou, Guihong Wang, Jian Yu, Shuhan Xie, Yantao Li, Yangyu Zhang, Jingwei Liang^†, Tao Luo^†

An adversarial framework that expands and reduces test suites to expose unsound or incomplete formal specifications in verifiable code generation.

PDF arXiv GitHub

ICML 2026

Decompose, Structure, and Repair: A Neuro-Symbolic Framework for Autoformalization via Operator Trees

Xiaoyang Liu, Zineng Dong, Yifan Bai, Yantao Li, Yuntian Liu, Tao Luo^†

A neuro-symbolic framework that structures autoformalization with operator trees and repairs failed Lean outputs.

PDF arXiv GitHub

ICML 2026

FormalRx: Rectify and eXamine Semantic Failures in Autoformalization

Haocheng Wang^*, Baiyu Huang^*, Yingjia Wan^*, Xiao Zhu, Xiaoyang Liu, Yinya Huang^†, Zhijiang Guo^†

A framework for detecting, examining, and rectifying semantic failures in autoformalized statements.

PDF arXiv HuggingFace

ICLR 2026

ASSESS: A Semantic and Structural Evaluation Framework for Statement Similarity

Xiaoyang Liu^*, Tao Zhu^*, Zineng Dong, Yuntian Liu, Qingfeng Guo, Zhaoxuan Liu, Yu Chen, Tao Luo^†

An evaluation framework that combines semantic and structural signals to compare formal statements.

PDF arXiv GitHub

NeurIPS 2025

ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data

Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, Yunqi Liu, Yu Chen, Yuntian Liu, Yang Jiao^†, Tao Luo^†

A data-centric approach to theorem autoformalization through lifting, augmentation, and synthesis.

PDF arXiv GitHub

ICML 2025 · AI4Math Workshop

Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization

Yuntian Liu^*, Tao Zhu^*, Xiaoyang Liu^*, Yu Chen, Zhaoxuan Liu, Qingfeng Guo, Jiashuo Zhang, Kangjie Bao, Tao Luo^†

A tree-edit-distance metric designed to evaluate the structure and meaning of autoformalized statements.

PDF arXiv GitHub

Invited Talks

Aug 2026
CSML, Shanghai Jiao Tong University
Shanghai, China
Jul 2026
AI4Math Workshop, Zhejiang University
Hangzhou, China
Jul 2025
AI4Math Workshop, Shanghai Jiao Tong University
Shanghai, China

Education

2024–2028
PhD, Applied Mathematics
Shanghai Jiao Tong University
2023–2024
MS, Data-Driven Modeling
Hong Kong University of Science and Technology
2019–2023
BS, Information and Computing Science
Jinan University