Itsykson and Sokolov [IS14] identified resolution over parities, denoted by $\text{Res}(\oplus)$, as a natural and simple fragment of $\text{AC}^0[2]$-Frege for which no super-polynomial lower bounds on size of proofs are known. Building on a recent line of work ([EGI24], [BCD24], [AI25]), Efremenko and Itsykson [EI25] proved lower bounds of the form $\text{exp}(N^{Ω(1)})$, on the size of $\text{Res}(\oplus)$ proofs whose depth is upper bounded by $O(N\log N)$, where $N$ is the number of variables of the unsatisfiable CNF formula. The hard formula they used was Tseitin on an appropriately expanding graph, lifted by a $2$-stifling gadget. They posed the natural problem of proving super-polynomial lower bounds on the size of proofs that are $Ω(N^{1+ε})$ deep, for any constant $ε> 0$. We prove the first such lower bounds. In fact, we show that $\text{Res}(\oplus)$ refutations of Tseitin formulas on constant-degree expanders on $m$ vertices, lifted with Inner-Product gadget of size $O(\log m)$, must have size $\text{exp}(\tildeΩ(N^ε))$, as long as the depth of the $\text{Res}(\oplus)$ proofs are $O(N^{2-ε})$, for every $ε> 0$. Here $N=Θ(m\log m)$ is the number of variables of the lifted formula. An important ingredient in our work is to show that arbitrary distributions lifted with such gadgets fool safe affine spaces, an idea which originates in the earlier work of Bhattacharya, Chattopadhyay and Dvorak [BCD24].

翻译：Itsykson与Sokolov [IS14] 将奇偶解析（记为 $\\text{Res}(\\oplus)$）识别为 $\\text{AC}^0[2]$-Frege 系统中一个自然且简单的片段，目前尚未有关于其证明规模超多项式下界的已知结果。基于近期一系列研究工作（[EGI24]、[BCD24]、[AI25]），Efremenko与Itsykson [EI25] 证明了对于深度上界为 $O(N\\log N)$ 的 $\\text{Res}(\\oplus)$ 证明，其规模具有 $\\text{exp}(N^{\\Omega(1)})$ 形式的下界，其中 $N$ 为不可满足CNF公式的变量数。他们所采用的困难公式是定义在适当扩展图上的Tseitin公式，并通过一个2-抑制（2-stifling）装置进行提升。他们提出了一个自然问题：对于任意常数 $\\varepsilon>0$，证明深度为 $\\Omega(N^{1+\\varepsilon})$ 的证明具有超多项式规模下界。我们首次证明了此类下界。具体而言，我们证明：对于定义在 $m$ 个顶点的常数度扩展图上的Tseitin公式，通过规模为 $O(\\log m)$ 的内积（Inner-Product）装置提升后，只要 $\\text{Res}(\\oplus)$ 证明的深度为 $O(N^{2-\\varepsilon})$（对于任意 $\\varepsilon>0$），其反驳的规模必须达到 $\\text{exp}(\\tilde{\\Omega}(N^{\\varepsilon}))$。此处 $N=\\Theta(m\\log m)$ 为提升后公式的变量数。我们工作的一个重要组成部分是证明：通过此类装置提升的任意分布能够欺骗安全仿射空间，这一思想源于Bhattacharya、Chattopadhyay与Dvorak的早期工作 [BCD24]。