We prove the first unconditional consistency result for superpolynomial circuit lower bounds with a relatively strong theory of bounded arithmetic. Namely, we show that the theory V$^0_2$ is consistent with the conjecture that NEXP $\not\subseteq$ P/poly, i.e., some problem that is solvable in non-deterministic exponential time does not have polynomial size circuits. We suggest this is the best currently available evidence for the truth of the conjecture. The same techniques establish the same results with NEXP replaced by the class of problems that are decidable in non-deterministic barely superpolynomial time such as NTIME$(n^{O(\log\log\log n)})$. Additionally, we establish a magnification result on the hardness of proving circuit lower bounds.

翻译：我们证明了首个非条件性一致性结果，即超多项式电路下界与有界算术的相对强理论相一致。具体而言，我们表明理论V$^0_2$与猜想NEXP $\not\subseteq$ P/poly一致，即某些可在非确定型指数时间内求解的问题不具有多项式大小的电路。我们提出这是目前支持该猜想真实性的最佳可用证据。相同的技术也建立了将NEXP替换为可在非确定型接近超多项式时间内判定的问题类时的一致结果，例如NTIME$(n^{O(\log\log\log n)})$。此外，我们建立了关于证明电路下界困难性的放大结果。