I’m a CS PhD student in UCSB. My current research topic is AI for math.

Previously, I graduated from Shanghai Jiao Tong University ACM class, doing research about embodied AI and Foundation Models.

Publication

Angelic Proving: Optimistic Proof Checking and Human-Oracle Refinement for Scalable Auto-Formalization

• Authors: Yanju Chen, Ruizhe Qian, Jiaming Shan, Xu Yang, Yufei Ding, Osbert Bastani, Yu Feng

• Conference/Journal: ICSE, 2026 (submission)

• We introduce MathEye, a framework to scale the auto-formalization of complex mathematical theorems where current methods fail. MathEye combines two key techniques: “angelic proving” to optimistically check incomplete proof sketches, and human-oracle intervention to refine difficult steps. This approach efficiently prunes invalid proofs and simplifies problems for either automatic resolution or expert input. On the PutnamBench suite, MathEye achieved over 98% accuracy with minimal human input, significantly outperforming strong baselines.

Sentinel: Adaptive Counter-Attack Synthesis for Mitigating Onchain Exploits

• Authors: Yanju Chen, Jiaming Shan, Hanzhi Liu, Jiaxin Song, Hongbo Wen, Yu Feng

• We introduce Sentinel, the first fully automated run-time defense against DeFi exploits. When an attack is detected, Sentinel analyzes it on the fly, understands the attacker’s goal, and synthesizes an optimal counter-attack contract to front-run the exploit and rescue the assets. Evaluated on 24 real-world exploits, Sentinel successfully generated mitigations in all cases, saving a potential $10M and outperforming state-of-the-art defenses by over 1,000x. Already deployed in pilot programs, it has neutralized five novel attacks, proving its practicality as a last line of defense for smart contracts.

Building Cooperative Embodied Agents Modularly with Large Language Model

• Authors: Weihua Du, Qiushi Lyu, Jiaming Shan, Zhenting Qi, Hongxin Zhang, Sunli Chen, Andi Peng, Tianmin Shu, Kwonjoon Lee, Behzad Dariush, Chuang Gan

• NeurIPS 2024 Track Datasets and Benchmarks Poster

• We introduce Constrained Human-AI Cooperation (CHAIC), an embodied AI challenge centered on social intelligence. Agents must infer human intent and constraints and cooperatively assist with everyday tasks. Our benchmark features new constrained human agents and diverse, long-horizon indoor/outdoor scenarios. We evaluate baselines and propose a new LLM-based method, demonstrating CHAIC’s effectiveness in assessing machine social intelligence.