Conference Publication

In theoretical computer science, the authors are usually listed in alphabetical order.

Distinguishing, Predicting, and Certifying: On the Long Reach of Partial Notions of Pseudorandomness. FOCS 2024 (to apper). Jiatu Li, Edward Pyne, Roei Tell. View Paper. To appear. Summary. We proved the equivalence between general derandomization (e.g. or ) and partial notions of pseudorandomness such as DPT24 and PRZ23 that are initially studied for space-bounded computation. Utilizing the idea, we also proved new unconditional results regarding catalytic computation, derived from weaker assumptions, and provided insightful new proofs of many classical results in the theory of derandomization.

Reverse Mathematics of Complexity Lower Bounds. FOCS 2024 (to appear). Lijie Chen, Jiatu Li, Igor C. Oliveira. View Paper. Preliminary Version. Summary. We systematically studied the reverse mathematics of complexity lower bounds using Cook's bounded theory as the base theory. In particular, we proved the equivalence between complexity lower bounds and fundamental combinatorial principles such as the pigeonhole principle, and obtained some counter-intuitive corollaries.

Hardness of Range Avoidance and Remote Point for Restricted Circuits via Cryptography. STOC 2024. Yilei Chen and Jiatu Li. View Paper. Full Version. Conference Version. Summary. Under a strong but plausible LWE-like assumption, we proved that the range avoidance problem is extremely hard: there is no efficient algorithm even if the circuit is of constant depth and the algorithm is allowed to use nondeterministic guesses. The main technical contribution is a generic construction of witness encryption for certain (possibly not NP-complete) hard languages from public-key encryption that has certain structures, and a Regev-style PKE that is plausibly hard against nondeterministic adversaries.

Indistinguishability Obfuscation, Range Avoidance, and Bounded Arithmetic. STOC 2023. Rahul Ilango, Jiatu Li, R. Ryan Williams. View Paper. Full Version. Conference Version. Summary. We showed that the range avoidance problem has no deterministic polynomial-time algorithm assuming and indistinguishability obfuscation. Under similar assumptions, we proved that Cook's theory cannot prove the dual weak pigeonhole principle, i.e., Jerabek's is a strict extension of .

Range Avoidance, Remote Point, and Hard Partial Truth Table via Satisfying-Pairs Algorithms. STOC 2023. Yeyuan Chen, Yizhi Huang, Jiatu Li, Hanlin Ren. View Paper. Full Version. Conference Version. Summary. We proposed a framework that solves the range avoidance problem, remote point problem, and hard partial truth-table for restricted circuit classes by non-trivial algorithms that solve satisfying pairs for the circuit class. This generalizes Williams's algorithmic approach in circuit lower bounds. In particular, we construct unconditional algorithms of these problems for circuits that recover the best-known (almost-everywhere) lower bound against .

Unprovability of Strong Complexity Lower Bounds in Bounded Arithmetic. STOC 2023. Jiatu Li, Igor C. Oliveira. View Paper. Full Version. Conference Version.
Summary. We showed that strong average-case separation in the third level of polynomial-time hierarchy cannot be proved in . This is a corollary of a general result that applies to the -th level of polynomial-time hierarchy. We demonstrated a convenient game-theoretic witnessing theorem to develop unprovability results.

Extremely Efficient Constructions of Hash Functions, with Applications to Hardness Magnification and PRFs. CCC 2022. Lijie Chen, Jiatu Li, Tianqi Yang. View Paper. Full Version. Conference Version. Summary. We constructed an explicit, uniform, randomness efficient, and low-complexity hash function. It is used to prove the following hardness magnification result: if there is a sparse language in NP that is not computable by size probabilistic circuits, then NP is not contained in SIZE.

The Exact Complexity of Pseudorandom Functions and the Black-Box Natural Proof Barrier for Bootstrapping Results in Computational Complexity. STOC 2022. Zhiyuan Fan, Jiatu Li, Tianqi Yang.
View Paper. Full Version. Conference Version. Online Talk. Summary. We gave tight bounds to compute PRFs in general circuit (in size), circuits (in size and depth) and circuits (in wire). Inspired by the natural proof barrier and our results, we demonstrated a barrier for bootstrapping results (e.g. hardness magnification) in complexity theory.

Circuit Lower Bounds for Explicit Functions. STOC 2022. Jiatu Li, Tianqi Yang.
View Paper. Full Version. Conference Version. Online Talk. Summary. We improved the unconditional circuit lower bound (for explicit function in to with a more clever choice of complexity measure and a more careful case analysis (plus some combinatorial tricks).

Manuscripts

In theoretical computer science, the authors are usually listed in alphabetical order.

The Structure of Catalytic Space: Capturing Randomness and Time via Compression. James Cook, Jiatu Li, Ian Mertz, Edward Pyne. View Paper. Preliminary Version. Summary. We unconditionally resolved several fundamental structural question related to catalytic computation. In particular, we proved (full derandomization for catalytic logspace).

On the Unprovability of Circuit Size Bounds in Intuitionistic . Lijie Chen, Jiatu Li, Igor C. Oliveira. View Paper. Preliminary Version. Summary. We show that there is a constant such that Buss's intuitionistic theory does not prove that SAT requires co-nondeterministic circuits of size at least . To our knowledge, this is the first unconditional unprovability result in bounded arithmetic in the context of worst-case fixed-polynomial size circuit lower bounds. We complement this result by showing that the upper bound is unprovable in .

Other Projects

• Formalization of PAL·S5 in Proof Assistant.
  • Technical Report: https://arxiv.org/abs/2012.09388.
  • Talk in LIRa seminar: https://projects.illc.uva.nl/lgc/seminar/2021/03/lira-session-jiatu-li/
  • Summary. We formalize public announcement logic (a special kind of dynamic epistemic logic) in Lean theorem prover as an experiment to apply formal tools in logic research. We present formal proof of its soundness, completeness and reduction (i.e. elimination of dynamic modalities) theorem.
• Formalization of a theorem in a competitive programming problem.
  • Github: https://github.com/ljt12138/Proof-of-Surreal
• Cutepiler: A Compiler for a C-like Language.
  • Github: https://github.com/Cutepiler/Cutepiler-Sysy2020
  • In National Student Computer System Capability Challenge (Compiler track).
  • A joint work with Runda Liu, Zhidong Wang and Mengdi Wu.
• Hyper OS: An Operating System Simulator in C++.
  • Github: https://github.com/tqyaaaaang/Hyper-OS
  • A joint work with Tianqi Yang.
  • Summary. An operating system simulator for teaching and research use in C++. It contains basic virtual hardware (such as CPU, APIC, MMU, etc) and a tiny kernel (including process scheduling and paging).
• A Quick Introduction to Mathematical Logic.
  • Note: https://ljt12138.github.io/2020/05/05/logic-note/
  • Summary. A note on classical results about propositional logic, first-order logic, proof system and (basic) model theory. It covers completeness theorem of first-order logic, the compactness theorem and G¨odel’s incompleteness theorem.
• The Application of Non-Programming Problems in Competitive Programming Training (in Chinese).
  • Essay: https://ljt12138.github.io/2020/01/09/wc-final/