Research
Research
Experience
University of Illinois, Urbana-Champaign (From Aug 2024 - )
Data Economics Graduate student, Guided by Prof. Bhaskar Ray Chaudhury
Human-AI collaboration Graduate student, Guided by Prof. Bhaskar Ray Chaudhury and Prof. Kate Donahue
University of California, Santa Barbara, Nubit (From June 2023 - )
Invariant Generation via Data-Driven Symbolic Reasoning Research Intern, Guided by Prof.Yu Feng and Hongbo Wen
Security of Smart Contracts Research Intern, Guided by Prof.Yu Feng, Dr. Yanju Chen, and Hongbo Wen
Zero-Knowledge Compiler Research Intern, Guided by Prof.Yu Feng, Dr. Yanju Chen, and Junrui Liu
Shanghai Jiao Tong University (from May 2020 - June 2023)
Fair Division Undergraduate Student, Guided by Prof. Biaoshuai Tao
Static Program Analysis Undergraduate student, Guided by Prof. Hongfei Fu
Verification of Correctness of C Compiler Undergraduate student, Guided by Prof. Qinxiang Cao
Interest
Game Theory
My research interests focus on algorithmic game theory. Very recently, I have been working on the topic of data economics and human-AI collaboration. With the rise of data markets, data-related economics have drawn attention. Due to the replicability of data, its analysis differs from traditional goods. In one of my recent works, we studied the existence of core-stable data exchange and showed it is PPAD-hard to find one -- which is the first PPAD-hardness result on this topic (the paper should be released very soon). Besides, I am also interested in the design of data markets (like fair and efficient data markets).
I also hold great interest in the problem of fair division, which studies how to fairly allocate fairly among a set of agents. I am highly engaged in exploring new models and intriguing notions.
In [BLLST'24], we propose the comparison-based query model -- where the allocator does not know the agents' valuation in advance and can only learn about it through comparison-based queries. We proved that a PROP1+1/2MMS allocation can be found in O(log m) queries.
In [BLLST'23], we study fair division with the allocator's preference -- you need to find an allocation that is fair to both agents and the allocator. We proved that a doubly-EF1 allocation always exists for two agents using some techniques related to graph chromatic numbers. The model still has many fascinating problems worth exploring (like applying techniques of Knser graph, and multi-color discrepancy theory).
Programming Languages
Besides the theoretical direction, I have also been working on the direction of programming languages and security.
Very recently, I have been interested in the security of smart contracts and optimizations of zero-knowledge circuits. In [WLS+'24], we propose FORAY -- a solver-aided approach that automatically detects logical vulnerabilities of DeFi smart contracts. In our very recent work, we have proposed new methods that achieve 5X~10X optimization in terms of proving time and circuit size compared to NOIR+halo2 (our papers will be released soon).
Before that, I was working in some "classical" directions of programming languages. I enjoy writing Coq proofs — a small try of using Coq to formalize the proof of envy-cycle elimination.