Collaborative Research: AF:Medium: Advancing the Lower Bound Frontier

计算复杂性理论的核心问题是为重要的计算问题开发最有效的算法。为了证明一种算法是最有效的，复杂性理论的圣杯是证明无条件的下界，表明任何算法，无论多么聪明或复杂，本质上都需要一定数量的资源（硬件或运行时）来解决。本研究的目标是解决显式问题的证明电路和运行时下界的最基本挑战，以及证明和通信复杂性下界的类似挑战。更详细地说，这个项目主要关注两种方法。第一种方法涉及利用电路下界和元算法之间的双向连接，元算法的输入或输出是电路或其他算法描述。元算法的重要例子有：电路可满足性，输入是电路，输出是电路是否可满足；证明搜索，其中输入是一个不满足的公式，输出是证明系统中对该公式的一个小反驳；和PAC学习，其中输入由未知目标函数的标记示例组成。通常，矛盾的是，诸如此类的元计算问题的高效算法会导致改进的下界，反之亦然。第二种方法被称为提升，即更复杂的计算模型中的下界被简化为更简单模型中的下界。通过提升和相关的思想，电路复杂性已经与证明复杂性和通信复杂性相关联，并且所有三种设置的下限都得到了改进。研究小组将研究各种各样的想法，以扩展和深化这些方法，以突破目前的下限障碍。该研究还有望为元算法问题开发改进的算法，这对于硬件和软件验证，算法学习以及广泛的其他应用至关重要。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

The central problem in computational complexity theory is to develop the most efficient algorithms for important computational problems. To prove that an algorithm is the most efficient, the holy grail of complexity theory is to prove unconditional lower bounds, showing that any algorithm, however clever or sophisticated, will inherently require a certain amount of resources (hardware, or runtime) to solve. The goal of this research is to tackle the most basic challenge of proving circuit and runtime lower bounds for explicit problems, as well as similar challenges in proof and communication complexity lower bounds.In more detail, this project is focused on two approaches. The first approach involves exploiting the two-way connection between circuit lower bounds and meta-algorithms, algorithms whose inputs or outputs are circuits or other algorithm descriptions. Important examples of meta-algorithms are: circuit satisfiability, where the input is a circuit and the output is whether it is satisfiable; proof search, where the input is an unsatisfiable formula and the output is a small refutation of it in a proof system; and PAC learning, where the input consists of labelled examples of an unknown target function to be output. Often, paradoxically, efficient algorithms for meta-computational problems such as these lead to improved lower bounds and vice versa. The second approach is known as lifting, whereby lower bounds in a more complex model of computation are reduced to lower bounds in a simpler model. Through lifting and related ideas, circuit complexity has been related to proof complexity and communication complexity, and lower bounds have been improved for all three settings. The team of researchers will investigate a variety of ideas to extend and deepen these approaches to push past the current barriers in lower bounds. The research is also expected to develop improved algorithms for meta-algorithmic problems, which are of central importance for hardware and software verification, algorithmic learning, and a broad range of other applications.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.