De la complexité des preuves à la complexité des circuits via des protocoles interactifs

Le folklore dans la théorie de la complexité soupçonne que les bornes inférieures des circuits contre NC¹ ou P/poly, actuellement hors de portée, sont une étape nécessaire pour prouver des bornes inférieures fortes de complexité des preuves pour des systèmes comme Frege ou Frege étendu. Établir formellement une telle connexion est cependant déjà intimidant, car cela impliquerait la séparation révolutionnaire NEXP P/poly, comme l'ont récemment observé Pich et Santhanam (2023). Nous montrons une telle connexion conditionnelle pour le système de preuve Frege étendu implicite (iEF) introduit par Kraj\'icek (The Journal of Symbolic Logic, 2004), capable de formaliser la plupart de la théorie de la complexité contemporaine. En particulier, nous montrons que si iEF prouve efficacement l'hypothèse de dérandomisation standard selon laquelle une fonction booléenne concrète est difficile en moyenne pour des circuits de taille subexponentielle, alors toute bornes inférieure suprapolynomiale sur la longueur des preuves iEF implique \#P FP/poly (ce qui impliquerait à son tour, par exemple, PSPACE P/poly). Notre preuve exploite la formalisation à l'intérieur de iEF de la validité du protocole de sum-check de Lund, Fortnow, Karloff et Nisan (Journal of the ACM, 1992). Cela a des conséquences pour l'auto-validité des bornes supérieures des circuits dans iEF. Fait intéressant, améliorer davantage notre résultat semble nécessiter des progrès dans la construction de systèmes de preuve interactifs avec des prouveurs plus efficaces.