cv

M.S. in Computer Science

University of Illinois Urbana-Champaign

B.Eng. in Computer Science and Technology

ShanghaiTech University

Research Assistant

University of Illinois Urbana-Champaign

Scaling αβ-CROWN toward parallel, high-performance, distributed, and scalable formal verification; applying HPC techniques in Python/PyTorch.

• Parallelization and performance engineering of αβ-CROWN
• Leveraged HPC strategies for PyTorch-based verifier workloads

ML System Engineer

Research Startup

Built end-to-end LLM pretraining stack: data production, distributed training, and evaluation.

• Designed a data production cluster capable of ~10M tokens/sec
• Set up NVIDIA Megatron-based distributed training
• Produced ~1T tokens and trained an 890M model on 16×H100 in ~14 days

Quant Systems Engineer

Sixie Capital

Supported quant research with GPU/CUDA/PyTorch; built distributed ML and HPC storage infra.

• Implemented multinode multi-GPU training with one-click orchestration
• Automated BeeGFS over RDMA InfiniBand deployment for HPC storage
• Shipped a meta-rule-based market data check system preventing multiple incidents

Research Assistant

National University of Singapore (NUS)

Developed CUDA implementations of algorithms with large speedups.

• Delivered CUDA kernels/implementations achieving ~1000× speedups over CPU

ISC'23 Student Cluster Competition — Third Place

International Supercomputing Conference (ISC)

Compiled, optimized, and analyzed fluid simulation workloads on FAU & Bridges-2 supercomputers.

SC'23 Student Cluster Competition — Seventh Place & Outstanding Reproducibility Report

Supercomputing Conference (SC)

48-hour continuous run analyzing large-scale matrix decompositions; reproduced key results.

ICPC Asia Regional — 3× Silver Medals

ICPC

Team captain and core member; solved 7 problems within 5-hour contests.

Verification of Bit-Flip Attacks against Quantized Neural Networks

OOPSLA 2025 (CCF-A)

verification of bit-flip attacks on QNNs.

BFAVerifier — CUDA-Accelerated Formal Verifier for Bit-Flip Attacks

• C++, CUDA, Gurobi
• Implemented SymPoly verification algorithm on GPU

LBM — Fluid Simulation Optimized for Microarchitectural Features

• C, OpenMP, SSE2, AVX2
• Microarchitecture-aware and low-level performance engineering