SJTU AI4Math Team

上海交通大学 AI4Math 团队是上海交通大学数学科学学院罗涛教授领导的研究团队，致力于将人工智能与形式化应用于数学科学的研究和教学。

SJTU AI4Math Team is a research team at School of Mathematical Sciences, Shanghai Jiao Tong University under the leadership of Prof. Tao Luo, dedicated to applying artificial intelligence and formalization to research and teaching in mathematical sciences.

AI4Math Summer Schools

AI4Math 暑期学校 2025 (AI4Math Summer School 2025)

2025年上海交通大学数学科学学院“AI4Math：Lean 4 与数学形式化”暑期学校

2025 SJTU SMS "AI4Math: Lean 4 & Mathematics Formalization" Summer School

Publications

* Equal contribution. † Corresponding author.

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^†

ICML 2026 · AI4Math Workshop

Links: Official · arXiv · GitHub

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^†

ICML 2026

Links: Official · arXiv · GitHub

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^†

ICLR 2026

Links: Official · arXiv · GitHub

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^†

NeurIPS 2025

Links: Official · arXiv · GitHub

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^†

ICML 2025 · AI4Math Workshop

Links: Official · arXiv · GitHub