Research

Game Theory

My research interests focus on game theory. Very recently, I have been working on the topic of data economics. 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 Kenser graph, and multi-color discrepancy theory).

Programming Languages

Besides the theoretical direction, I have also been working on programming synthesis. 

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.