HEИндивидуална стипендия2024–2026

NoShortProof · Nonexistence of Short Proofs

„Хоризонт Европа“ — Действия „Мария Склодовска-Кюри“

Период: 2024-04-01 → 2026-03-31
Финансиране от ЕС: 230 774 €
Участници: 2
Схема: HORIZON-TMA-MSCA-PF-EF

Линиите свързват координатора с партньорите.

Накратко на български

Математическите системи за доказване определят колко дълги и сложни са изчисленията при решаване на комбинаторни задачи. Това помага да се разбере защо някои алгоритми работят бавно и кои методи за търсене на отговори са безполезни.

Този кратък обзор е генериран от изкуствен интелект

Кратко обяснение, генерирано от езиков модел по текста на CORDIS. Оригиналът е по-долу.

Резултати накратко

Nonexistence of Short Proofs

This project investigates the fundamental limits of efficient algorithms for solving combinatorial problems through formal mathematical reasoning frameworks known as proof systems. These systems form the theoretical basis of widely used algorithmic methods such as SAT solvers, algebraic techniques, integer programming, and semidefinite programming hierarchies. Despite their practical success, a theoretical understanding of why these algorithms perform well, or fail, on real-world instances remains larely incomplete. The main objectives are to establish strong impossibility results, specifically average-case lower bounds and supercritical trade-offs, on the size or depth of proofs in three key proof systems: Resolution, Cutting Planes, and Sum-of-Squares. The mathematical methods developed have broader implications, including advances in pseudo-random matrix analysis and circuit complexity. Practically, these results clarify the inherent hardness of fundamental computational and learning problems beyond worst-case scenarios, offering guidance for future algorithm design by ruling out futile heuristics.

Текст от CORDIS, на английски · Данни: CORDIS, © Европейски съюз

Цел на проекта

Efficient algorithms are vital for dealing with the ever growing amounts of data in our modern world. A particularly tricky task is posed by so-called combinatorial problems, where objects need to be combined together to form a solution satisfying some specified constraints. Increasing data size quickly causes an exponential growth in the search space for such problems, and despite decades of effort no algorithms have been designed that are guaranteed to tame this combinatorial explosion. In practice, however, it is often possible to find algorithmic shortcuts that work reasonably well, although there is very limited scientific understanding of when and why this is the case. This points to a fundamental challenge: We need a better understanding of the power and limitations of modern algorithm design.An important tool for algorithm analysis is to describe its method of reasoning in a formal proof system. When the algorithm terminates, the execution trace can be viewed as a proof of correctness of the result computed. If we can prove mathematically that no short proofs exist for certain types of statements, then this shows that the algorithm cannot possibly solve the corresponding problems efficiently.The goal of this project is to shed light on proof systems corresponding to some of the most powerful algorithmic paradigms in wide use and to delineate their potential. One concrete objective is to study combinatorial and algebraic methods for solving well-known graph problems such as Clique. Another goal is to compare semidefinite programming to traditional algorithms for solving non-Gaussian component analysis (NGCA), a fundamental problem in statistical learning. I will do so by strengthening existing techniques for analyzing these proof systems and combining them in novel ways. In particular, one important challenge will be to study the setting where the power of a proof system needs to be understood for a distribution of problems from which the input is drawn.

Оригинален текст от CORDIS (на английски).

Участници

KOBENHAVNS UNIVERSITET · KOBENHAVNКоординаторДания
UNIVERSITAT POLITECNICA DE CATALUNYA · BARCELONAИспания