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)})$）时的相同结果。此外，我们建立了关于证明电路下界难度的一个放大结果。