Motivated by practical applications in the design of optimization compilers for neural networks, we initiated the study of identity testing problems for arithmetic circuits augmented with exponentiation gates that compute the real function x↦ e^x. These circuits compute real functions of form P(→x)/P'(→x), where both P(→x) and P'(→x) are exponential polynomials ∑_{i = 1}^k f_i(→x)⋅ exp((g_i(→x))/(h_i(→x))), for polynomials f_i(→x),g_i(→x), and h_i(→x). We formalize a black-box query model over finite fields for this class of circuits, which is mathematical simple and reflects constraints faced by real-world neural network compilers. We proved that a simple and efficient randomized identity testing algorithm achieves perfect completeness and non-trivial soundness. Concurrent with our work, the algorithm has been implemented in the optimization compiler Mirage by Wu et al. (OSDI 2025), demonstrating promising empirical performance in both efficiency and soundness error. Finally, we propose a number-theoretic conjecture under which our algorithm is sound with high probability.

In this work, we propose a new bounded arithmetic theory, denoted APX1, designed to formalize a broad class of probabilistic arguments commonly used in theoretical computer science. Under plausible assumptions, APX1 is strictly weaker than previously proposed frameworks, such as the theory APC1 introduced in the seminal work of Jeřábek (2007). From a computational standpoint, APX1 is closely tied to approximate counting and to the central question in derandomization, the prBPP versus prP problem, whereas APC1 is linked to the dual weak pigeonhole principle and to the existence of Boolean functions with exponential circuit complexity.

Modern cryptography relies on the intractability of computational problems. We present an approach to build cryptography from a new source of hardness: proving mathematical theorems. Unprovability results are abundant in mathematics and theoretical computer science, yet to our knowledge, they have not been used as a resource for cryptography.

STOC ’25, Prague, Czechia

STOC ’25, Prague, Czechia

We show that there is a constant $k$ such that Buss's intuitionistic theory $\mathsf{IS}^1_2$ does not prove that SAT requires co-nondeterministic circuits of size at least $n^k$. 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 $\mathsf{NP} \subseteq \mathsf{coNSIZE}[n^k]$ is unprovable in $\mathsf{IS}^1_2$. In order to establish our main result, we obtain new unconditional lower bounds against refuters that might be of independent interest. In particular, we show that there is no efficient refuter for the lower bound $\mathsf{NP} \nsubseteq \mathsf{i.o.}\text{-}\mathsf{coNP}/\mathsf{poly}$, addressing in part a question raised by Atserias (2006).

Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are necessary to prove a given theorem. In this work, we systematically explore the reverse mathematics of complexity lower bounds. We explore reversals in the setting of bounded arithmetic, with Cook's theory PV1 as the base theory, and show that several natural lower bound statements about communication complexity, error correcting codes, and Turing machines are equivalent to widely investigated combinatorial principles such as the weak pigeonhole principle for polynomial-time functions and its variants. As a consequence, complexity lower bounds can be formally seen as fundamental mathematical axioms with far-reaching implications. The proof-theoretic equivalence between complexity lower bound statements and combinatorial principles yields several new implications for the (un)provability of lower bounds. Among other results, we derive the following consequences: • Under a plausible cryptographic assumption, the classical single-tape Turing machine (n2)-time lower bound for Palindrome is unprovable in Jerabek's theory APC1. The conditional unprovability of this simple lower bound goes against the intuition shared by some researchers that most complexity lower bounds could be established in APC1. • While APC1 proves one-way communication lower bounds for Set Disjointness, it does not prove one-way communication lower bounds for Equality, under a plausible cryptographic assumption. • An amplification phenomenon connected to the (un)provability of some lower bounds, under which a quantitatively weak lower bound is provable if and only if a stronger (and often tight) nclower bound is provable. • Feasibly definable randomized algorithms can be feasibly defined deterministically (APC1 is over PV1) if and only if one-way communication complexity lower bound for Set Disjointness are provable in PV1.

This paper revisits the study of two classical technical tools in theoretical computer science: Yao's trans-formation of distinguishers to next-bit predictors (FOCS 1982), and the “reconstruction paradigm” in pseudorandomness (e.g., as in Nisan and Wigderson, JCSS 1994). Recent works of Pyne, Raz, and Zhan (FOCS 2023) and Doron, Pyne, and Tell (STOC 2024) showed that both of these tools can be derandomized in the specific context of read-once branching programs (ROBPs), but left open the question of de randomizing them in more general settings. Our main contributions give appealing evidence that derandomization of the two tools is possible in general settings, show surprisingly strong consequences of such derandomization, and reveal several new settings where such derandomization is unconditionally possible for algorithms stronger than ROBPs (with useful consequences). Specifically: •We show that derandomizing these tools is equivalent to general derandomization. Specifically, we show that derandomizing distinguish - to- predict transformations is equivalent to prBPP=prP, and that derandomized reconstruction procedures (in a more general sense that we introduce) is equivalent to prBPP=prZPP. These statements hold even when scaled down to weak circuit classes and to algorithms that run in super-polynomial time. •Our main technical contributions are unconditional constructions of derandomized versions of Yao's transformation (or reductions of this task to other problems) for classes and for algorithms beyond ROBPs. Consequently, we deduce new results: A significant relaxation of the hypotheses required to derandomize the isolation lemma for logspace algorithms and deduce that NL=UL; and proofs that de-randomization necessitates targeted PRGs in catalytic logspace (unconditionally) and in logspace (conditionally). In addition, we introduce a natural subclass of prZPP that has been implicitly studied in recent works (Korten FOCS 2021, CCC 2022): The class of problems reducible to a problem called “Lossy Code”. We provide a structural characterization for this class in terms of derandomized reconstruction procedures, and show that this characterization is robust to several natural variations. Lastly, we present alternative proofs for classical results in the theory of pseudorandomness (such as two-sided derandomization reducing to one-sided), relying on the notion of deterministically transforming distinguishers to predictors as the main technical tool.

A recent line of research has introduced a systematic approach to exploring the complexity of explicit construction problems through the use of meta-problems, namely, the range avoidance problem (abbrev. Avoid) and the remote point problem (abbrev. ). The upper and lower bounds for these meta problems provide a unified perspective on the complexity of specific explicit construction problems that were previously studied independently. An interesting question largely unaddressed by previous works is whether we can show hardness of Avoid and RPP for simple circuits, such as low-depth circuits. In this paper, we demonstrate, under plausible cryptographic assumptions, that both the range avoidance problem and the remote point problem cannot be efficiently solved by nondeterministic search algorithms, even when the input circuits are as simple as constant-depth circuits. This extends a hardness result established by Ilango, Li, and Williams (STOC’23) against deterministic algorithms employing witness encryption for NP, where the inputs to Avoid are general Boolean circuits. Our primary technical contribution is a novel construction of witness encryption inspired by public-key encryption for certain promise language in NP that is unlikely to be NP-complete. We introduce a generic approach to transform a public-key encryption scheme with particular properties into a witness encryption scheme for a promise language related to the initial public-key encryption scheme. Based on this translation and variants of standard lattice-based or coding-based PKE schemes, we obtain, under plausible assumption, a provably secure witness encryption scheme for some promise language in NP-coNP/poly. Additionally, we show that our constructions of witness encryption are plausibly secure against nondeterministic adversaries under a generalized notion of security in the spirit of Rudich’s super-bits (RANDOM’97), which is crucial for demonstrating the hardness of Avoid and RPP against nondeterministic algorithms.

The range avoidance problem, denoted as C-Avoid, asks to find a non-output of a given C-circuit C:0,1^n -> 0,1^l with stretch l>n. This problem has recently received much attention in complexity theory for its connections with circuit lower bounds and other explicit construction problems. Inspired by the Algorithmic Method for circuit lower bounds, Ren, Santhanam, and Wang (FOCS’22) established a framework to design FP^NP algorithms for C-Avoid via slightly non-trivial data structures related to C. However, a major drawback of their approach is the lack of unconditional results even for C=AC^0.

The range avoidance problem (denoted by Avoid) asks to find a string outside of the range of a given circuit C:{0,1}n→{0,1}m, where m>n. Although at least half of the strings of length m are correct answers, it is not clear how to deterministically find one. Recent results of Korten (FOCS’21) and Ren, Wang, and Santhanam (FOCS’ 22) show that efficient deterministic algorithms for Avoid would have far-reaching consequences, including strong circuit lower bounds and explicit constructions of combinatorial objects (e.g., Ramsey graphs, extractors, rigid matrices). This strongly motivates the question: does an efficient deterministic algorithm for Avoid actually exist?

While there has been progress in establishing the unprovability of complexity statements in lower fragments of bounded arithmetic, understanding the limits of Jerabek’s theory APC1 (2007) and of higher levels of Buss’s hierarchy S2i (1986) has been a more elusive task. Even in the more restricted setting of Cook’s theory PV (1975), known results often rely on a less natural formalization that encodes a complexity statement using a collection of sentences instead of a single sentence. This is done to reduce the quantifier complexity of the resulting sentences so that standard witnessing results can be invoked.

Investigating the computational resources we need for cryptography is an essential task of both theoretical and practical interests. This paper provides answers to this problem on pseudorandom functions (PRFs). We resolve the exact complexity of PRFs by proving tight upper and lower bounds for various circuit models.

Proving circuit lower bounds has been an important but extremely hard problem for decades. Although it can be shown that almost every function f:F2n→F2 requires circuit of size Ω(2n/n) by a simple counting argument, it remains unknown whether there is an explicit function (for example, a function in NP) not computable by circuits of size 10n. In fact, a 3n−o(n) explicit lower bound by Blum (TCS, 1984) was unbeaten for over 30 years until a recent breakthrough by Find, Golovnev, Hirsch, and Kulikov (FOCS, 2016), which proved a (3+1/86)n−o(n) lower bound for affine dispersers, a class of functions known to be constructible in P. To obtain this improvement, Find, Golovnev, Hirsch, and Kulikov (FOCS, 2016) generalized the classical gate elimination method by keeping track of a bottleneck structure called troubled gates.