We study the relationship between the existence of optimal proof systems and recursive jump operators, two central open problems in proof complexity. For a set L, an optimal proof system is a strongest proof system in terms of proof length, whereas a recursive jump operator uniformly transforms any proof system for L into a stronger one with respect to proof length, thereby witnessing non-optimality. It is clear that the existence of a recursive jump operator for L rules out optimal proof systems for L. Khaniki (FOCS 2024) is interested in the converse of this implication and explicitly poses the following question, where TAUT denotes the set of propositional tautologies. Q: Does the non-existence of optimal proof systems for TAUT imply the existence of recursive jump operators for TAUT? We generalize and address this question from both a relativized and an unrelativized perspective. We show that proving a positive answer for Q is provably hard by constructing the following oracle. O: The polynomial-time hierarchy is infinite, TAUT has no optimal proof systems, and TAUT has no recursive jump operators. This shows that Khaniki's question can not be answered in the positive by relativizable means, even under the standard complexity-theoretic assumption that the polynomial-time hierarchy is infinite. In contrast, we obtain positive results when the question Q is posed for sets different from TAUT. We prove that the existence of recursive jump operators is upward closed under $\leq_{\text{m}}^{\text{p}}$-reducibility, a result that so far was only known for the non-existence of optimal proof systems. Furthermore, we show that the sets known to have no optimal proof systems by Messner (STACS 1999) in fact admit recursive jump operators. Thus, essentially all sets currently known to have no optimal proof systems have recursive jump operators.


翻译:我们研究了最优证明系统的存在性与递归跳跃算子之间的关系,这是证明复杂性中两个核心未解问题。对于集合L,最优证明系统是指在证明长度方面最强的证明系统,而递归跳跃算子则能将L的任何证明系统一致地转化为一个在证明长度上更强的系统,从而表明其非最优性。显然,L上递归跳跃算子的存在排除了L的最优证明系统。Khaniki(FOCS 2024)对该蕴涵的逆命题感兴趣,并明确提出了以下问题,其中TAUT表示命题重言式集合。问:TAUT不存在最优证明系统是否蕴涵TAUT存在递归跳跃算子?我们从相对化和非相对化两个角度对该问题进行了推广和研究。我们通过构造以下谕示证明了Q的肯定回答是难以证明的。O:多项式层次是无穷的,TAUT没有最优证明系统,且TAUT没有递归跳跃算子。这表明,即使在标准复杂性理论假设(多项式层次无穷)下,Khaniki的问题也无法通过相对化方法得到肯定回答。相比之下,当问题Q针对不同于TAUT的集合提出时,我们得到了肯定结果。我们证明了递归跳跃算子的存在性在$\leq_{\text{m}}^{\text{p}}$-可归约性下向上封闭,这一结果此前仅对最优证明系统的不存在性成立。此外,我们证明了Messner(STACS 1999)已知没有最优证明系统的集合实际上承认递归跳跃算子。因此,当前已知没有最优证明系统的所有集合本质上都具有递归跳跃算子。

0
下载
关闭预览

相关内容

【剑桥大学-算法手册】Advanced Algorithms, Artificial Intelligence
专知会员服务
36+阅读 · 2024年11月11日
南大《优化方法 (Optimization Methods》课程,推荐!
专知会员服务
80+阅读 · 2022年4月3日
专知会员服务
37+阅读 · 2021年9月12日
机器学习中的最优化算法总结
人工智能前沿讲习班
22+阅读 · 2019年3月22日
推荐系统算法合集,满满都是干货(建议收藏)
七月在线实验室
17+阅读 · 2018年7月23日
干货|掌握机器学习数学基础之优化[1](重点知识)
机器学习研究会
10+阅读 · 2017年11月19日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
Arxiv
0+阅读 · 5月31日
VIP会员
最新内容
ICML 2026 | CFPO:用反事实策略优化提升多模态推理
专知会员服务
1+阅读 · 今天14:45
综述 | 世界动作模型:少做梦,多行动
专知会员服务
1+阅读 · 今天14:43
美以伊冲突:无人机与人工智能的运用
专知会员服务
3+阅读 · 今天14:31
《特种部队在透明战场中的生存力》最新报告
专知会员服务
2+阅读 · 今天14:11
《人工智能生成的零日漏洞:对未来作战的影响》
综述 | 3D场景图:开放挑战与未来方向
专知会员服务
8+阅读 · 6月22日
21世纪的无人机战争
专知会员服务
4+阅读 · 6月22日
《量子技术的军事任务技术适配与利用》
专知会员服务
5+阅读 · 6月22日
相关资讯
机器学习中的最优化算法总结
人工智能前沿讲习班
22+阅读 · 2019年3月22日
推荐系统算法合集,满满都是干货(建议收藏)
七月在线实验室
17+阅读 · 2018年7月23日
干货|掌握机器学习数学基础之优化[1](重点知识)
机器学习研究会
10+阅读 · 2017年11月19日
相关基金
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
Top
微信扫码咨询专知VIP会员