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<unk> O) (log\log\log\log\ n) 。 此外, 我们为证明电路下界的难度确定了放大效果 。</s>