Proof Complexity and Meta-Mathematics 2023
2023-03-20..2023-03-24
Berkeley, United States
who it's for
proof complexity researchers, computational complexity theorists, bounded arithmetic researchers, algebraic complexity researchers, cryptographers working on obfuscation, sat and solver researchers, learning theory and ml theorists
topics
polynomial calculus over F_p lower bounds; cutting planes lower bounds for log-cnf; hitting proof system and verification; k-DNF resolution on random CNF; lifting to parity decision trees; consistency of NEXP not in P/poly; indistinguishability obfuscation constructions; extended Frege lower bounds implications; algebraic natural proofs and IPS; variety membership and tensor slice rank; certifying cutting planes with strengthenings; connections between QBF and circuit complexity
| title | author | length |
|---|---|---|
| Lower Bounds Against PC With Extension Variables | Russell Impagliazzo | 55m |
Proves a concrete size lower bound for Polynomial Calculus over F_p (PCR): for every prime p, n and κ = O(log n) there is an explicit unsatisfiable polynomial… | ||
| Random log(n)-CNF are Hard for Cutting Planes (Again) | Dmitry Sokolov | 59m |
Claim: random Δ=Θ(log n)-CNF formulas require hugely large Cutting Planes proofs. The proof builds a reduction from any Cutting Planes proof to a dag-like… | ||
| The Hitting Proof System | Yuval Filmus | 30m |
A hitting refutation is a partition of 0/1^n into subcubes where each subcube’s assignments all falsify a single clause; disjointness is certified by variable… | ||
| A Lower Bound for k-DNF Resolution on Random CNF Formulas via Expansion | Anastasia Sofronova | 27m |
Proves that random m-clause CNFs whose clause-variable bipartite graph is a good boundary expander require Res(k) proofs of exponential size by converting… | ||
| Lifting to Parity Decision Trees via Stifling (with applications to proof complexity) | Suhail Sherif | 01h 05m |
Proves a lifting theorem that turns any deterministic decision tree lower bound for a relation R into a parity decision tree size lower bound for R composed… | ||
| Consistency of NEXP Not in P/poly in a Strong Theory | Albert Atserias | 01h 02m |
Shows a concrete consistency result: there is a model of V^0_2 in which the canonical NEXP complete bounded halting problem has no polynomial size circuits, so… | ||
| Indistinguishability Obfuscation, Range Avoidance, and Bounded Arithmetic | Rahul Ilango | 31m |
Main claim: under two assumptions—NP not in coAM infinitely often and existence of subexponentially secure indistinguishability obfuscation—the theory PV1… | ||
| Unprovability of Strong Complexity Lower Bounds in Bounded Arithmetic | Igor Oliveira | 48m |
Unconditional result: APC_1 cannot prove LB3 — a single sentence asserting a mild average‑case separation between ∃∀∃ and ∀∃∀ circuits (poly‑size π3 versus… | ||
| Towards P≠NP from Extended Frege Lower Bounds | Ján Pich | 57m |
If (a) S^1_2 proves a concrete E-function is hard to approximate by subexponential circuits and (b) S^1_2 proves a p-time reduction turns circuits breaking… | ||
| Indistinguishability Obfuscation via Mathematical Proofs of Equivalence | Zhengzhong Jin | 52m |
Claims an indistinguishability obfuscator whose security loss is independent of input length when the two programs have short formal proofs of equivalence… | ||
| Frontiers of Proof Complexity Lower Bounds via Algebraic Complexity & Open Problems | Iddo Tzameret | 01h 04m |
Survey of state-of-the-art reductions showing that lower bounds for algebraic circuits yield proof complexity lower bounds via the Ideal Proof System (IPS)… | ||
| Variety Membership Testing, Algebraic Natural Proofs, and Geometric Complexity Theory | Markus Bläser | 52m |
Proves that testing membership for 3-tensor slice rank and minrank varieties is NP-hard, and hence orbit closure containment for 3-tensors is NP-hard; extends… | ||
| Natural Proofs in Algebraic Circuit Complexity | Anamay Tengse | 47m |
Shows two concrete results: bounded-coefficient polynomials in VP-prime admit nontrivial algebraic equations computable by small circuits, constructed by… | ||
| On the Problems Related to Waring Rank and Border Waring Rank | Pranjal Dutta | 33m |
Shows that if a homogeneous polynomial has border Waring rank k (k < degree d) then its actual Waring rank is at most 4^k · d, improving the trivial d^k bound… | ||
| Certifying Combinatorial Solving Using Cutting Planes with Strengthening Rules | Jakob Nordström | 01h 05m |
Claims that cutting planes with redundance-based strengthening plus explicit witnesses lets off‑the‑shelf solvers emit compact, machine‑checkable proofs for… | ||
| On the Dominance-Based Strengthening Rule | Neil Thapen | 33m |
Introduces a formalization of the dominance-based strengthening rule and proves it simulates polynomial local search (PLS) by encoding neighbors, initial… | ||
| Connections Between QBF Proof Complexity and Circuit Complexity | Olaf Beyersdorff | 33m |
Proves a tight correspondence: QBF refutations in Frege-like systems exactly mirror circuit lower bounds via strategy extraction that yields programs in… | ||
| Weak Versions of Extended Resolution | Emre Yolcu | 34m |
Shows that a family of explicitly defined weakenings of extended resolution (BC-, SBC-, RAT-, SPR- etc.) are pairwise incomparable by giving a uniform… | ||
| CDCL vs Resolution: The Picture in QBF | Benjamin Böhm | 29m |
The paper proves classical QCDCL and Q-Resolution are incomparable and then pins down which algorithmic changes give exact matches: allowing arbitrary decision… | ||
| Read-Once Branching Programs as Proof Lines | Dmitry Itsykson | 37m |
Defines semantic refutations whose proof lines are read-once branching programs (deterministic, nondeterministic, ordered OBDDs) and shows concrete simulations… | ||
| Lower Bounds Against Non-Commutative Models of Algebraic Computation | Prerona Chatterjee | 34m |
Proves a concrete improvement: any homogeneous non-commutative circuits computing the ordered elementary symmetric polynomial of degree n/2 requires size… | ||
| Unprovability and Other Impossibility Results in Machine Learning | Shai Ben-David | 47m |
Shows that expectation-maximization learning of set families hinges on set-theory: existence of a finite compression scheme for finite-subset classes is… | ||
| Implicit Proof Systems | Pavel Pudlák | 36m |
Defines circuit that outputs proof bits as a way to present exponentially long proofs succinctly and insists on a separate short certificate that the circuit… | ||
| Lower Bounds for NW-generators in AC0-Frege | Erfan Khaniki | 33m |
Proves a concrete conditional lower bound: for any symmetric f in NP ∩ CoNP that is exponentially hard for depth‑two AC0 circuits, the Nisan–Wigderson map… | ||
| TFNP | Noah Fleming | 48m |
Claims that relate TFNP subclasses to concrete models: resolution = PLS via an explicit reduction from search(F) to the sink-of-DAG problem (one DAG vertex per… | ||
| nothing matches | ||