paperbot · PL 论文追踪

全部论文 待读 收藏

P2 The Surprising Power of Constant Depth Algebraic Proofs

常数深度代数证明的惊人能力
LICS Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science2020匹配度 1/10 · 该论文属于证明复杂度与代数证明系统下界，研究 AC0[p]-Frege 等系统，与用户关注的静态分析、LLM/Agent 辅助验证、浮点程序分析及贝叶斯程序分析均无直接关联。虽然与形式化验证的理论基础有些许距离上的联系，但并非用户当前研究画像的核心方向。引用 9 inbox
Russell Impagliazzo, Sasank Mouli, Toniann Pitassi
逻辑与自动机
crossref: 2026-09-12

AI 速览

一句话：关注 AC0[p]-Frege 超多项式下界这一开放问题，讨论常数深度代数证明系统的能力与已有子系统下界。

本文属于证明复杂度研究，关注 AC0[p]-Frege 证明系统的超多项式下界这一重要开放问题。AC0[p]-Frege 是带素数模计数门的常数深度电路类 AC0[p] 对应的证明系统。尽管 AC0[p] 电路的下界已存在约三十年，AC0[p]-Frege 本身仍没有显著下界。对于该系统的若干子系统，包括 Nullstellensatz、Polynomial Calculus 和 SOS，已有大量次数下界，但如何将这些结果推广到 AC0[p]-Frege 仍无进展。论文围绕常数深度代数证明的意外能力展开，指出代数证明子系统与完整 AC0[p]-Frege 下界之间的差距。摘要未给出具体新证明方法或评估细节。

问题
证明 AC0[p]-Frege 的超多项式下界；该问题长期开放，而其代数子系统已有多项式次数下界。
方法
摘要未具体说明方法，主要是在证明复杂度框架下讨论常数深度代数证明系统及其与 AC0[p]-Frege 的关系。
评估
属于理论证明复杂度分析；摘要未报告实验评估或具体下界结果。
原文摘要（Abstract）

A major open problem in proof complexity is to prove superpolynomial lower bounds for AC0[p]-Frege proofs. This system is the analog of AC0 [p], the class of bounded depth circuits with prime modular counting gates. Despite strong lower bounds for this class dating back thirty years ([28, 30]), there are no significant lower bounds for AC0 [p]-Frege. Significant and extensive degree lower bounds have been obtained for a variety of subsystems of AC0[p]-Frege, including Nullstellensatz ([3]), Polynomial Calculus ([9]), and SOS ([14]). However to date there has been no progress on AC0 [p]-Frege lower bounds.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot5501,
  title = {The Surprising Power of Constant Depth Algebraic Proofs},
  author = {Russell Impagliazzo and Sasank Mouli and Toniann Pitassi},
  booktitle = {LICS},
  year = {2020},
  doi = {10.1145/3373718.3394754}
}