{"id":"421b437a-3827-44fe-9977-1b69b7d1b2e1","arxiv_id":"2412.09984","paper_version":2,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"A new framework defines TFNP subclasses by adversarial oracles for complexity classes, and shows PSPACE and the polynomial hierarchy yield classes characterized by Frege and constant-depth Frege.","lead":"Total search problems (always find a solution) are organized into classes like PPA and PLS. This paper shows that many such classes can be built by asking an untrustworthy oracle about harder complexity classes, and connects the resulting classes to standard proof systems.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Section 9's type-2/decision-tree translation is not depth-preserving; Proposition 8.7 relies on an unproven TFNPdt equivalence.","rationale":"The reader's weakest assumption identifies the same border between type-2 TFNP and TFNPdt, but my concern is more specific: the natural translation asserted in Section 9.1 does not preserve the depth parameter. A polynomial-time type-2 reduction can make a^{O(1)} queries to an oracle string of length quasipoly(a), whereas a TFNPdt reduction may only make poly(log a) queries to its input. The paper does not define the decision-tree versions of Local-Γk_TQBF or Local-ΓTQBF, nor does it prove that the particular reductions from Proposition 9.2 and Proposition 9.6 are shallow. This matters because Proposition 8.7 is the broadest-interest claim, and it is stated about TFNPdt classes and proof-system characterizations. The proof-complexity core in Section 8 is careful and largely self-contained, and I have no objection to Theorem 8.17 or Theorem 8.20 as statements about GIk and FCon. The gap is in the bridge: Corollaries 9.3 and 9.8 need either a precise construction of the decision-tree version of Local-ΓTQBF with a bound on QBF query length, or an explicit depth-tracking translation of the type-2 equivalences. If such a construction is impossible for the current definition, the Frege characterization is not a well-formed TFNPdt theorem; if it is possible but omitted, the paper is still incomplete at a load-bearing point. I would therefore ask for a conditional acceptance: the likely mathematical claims should be accepted only after Section 9.1 is expanded to make the decision-tree versions precise and to verify the poly(log a) depth bounds, or the claims should be restated in type-2 terms.","tokens_in":46708,"tokens_out":17053,"duration_ms":211032,"concrete_test":"Write down the induced TFNPdt problem for type-2 Local-ΓTQBF with explicit bounds: protocol tree depth log a, each query a QBF of length L(a), and δ a string of length quasipoly(a). Determine the minimal decision-tree depth required to check a branch against ΓTQBF. (i) If L(a) is allowed to be a^{O(1)}, construct a one-query protocol A(F) where F is a quantifier-free circuit of size a^2 with D-gates querying a^2 distinct positions of δ; the 'good branch' predicate then needs a^2 queries to δ, so the problem is not TFNPdt. (ii) If L(a) is meant to be polylog a, prove that checking a branch has depth poly(log a) and then re-derive Corollary 9.3 and Corollary 9.8 by explicitly composing the type-2 reductions of Propositions 9.2 and 9.6 with this check, tracking the depth bound at every step.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The central characterizations are TFNPdt statements, but the equivalences that feed them (Corollary 9.3 and Corollary 9.8) are proved for type-2 problems, and the passage from type-2 to decision-tree problems in Section 9.1 is only asserted. A polynomial-time oracle machine over a quasipolynomial-length input does not automatically become a decision tree of depth poly(log a): it may query a^{O(1)} bits of the input, which is not a polylogarithmic number of queries. Thus the statement that Local-Γk_TQBF and GIk are equivalent in TFNPdt requires a separate argument that the reductions from Proposition 9.2 are shallow and that the solution predicates are decidable by depth-poly(log a) decision trees. For Local-ΓTQBF this is especially delicate: whether a branch is good depends on evaluating quantifier-free circuits with D-gates (axiom 3 of ΓTQBF), and nothing in Section 9.1 bounds the size of the QBFs appearing in a protocol tree or the number of δ-queries needed to evaluate them. If a protocol of depth log a may contain a long QBF query, the induced relation need not lie in TFNPdt, and Corollary 9.8 would not be a statement about TFNPdt at all. The equivalence Local-ΓTQBF ≡ FCon in the decision-tree setting is therefore not established by the text as written.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper develops two abstract mechanisms for producing TFNP subclasses from objects outside TFNP. The first is an Inspector-Adversary game over a list Γ of universal axioms, yielding the class of problems reducible to the canonical problem Local-Γ (Section 3). The second is counterexample reducibility to TFΣ_2^p problems, whose projection to TFNP gives Checkable R (Section 6). The main results are: parity axioms Γ⊕ give exactly PPA (Theorem 4.1) with some robustness to the choice of axioms (Theorem 4.7); natural NP axioms give PLS (Proposition 6.10); PSPACE axioms, whether via QBF evaluation or via iterated circuits, give equivalent classes (Theorem 5.3) that contain the standard TFNP classes; and the stratified QBF axioms Γ_k^TQBF correspond to the previously studied GI_k problems and, in the decision-tree setting, to constant-depth Frege and Frege proof systems (Proposition 8.7). The paper also gives a simplified definition of the approximate-counting class APPROX, proves Ramsey, Weak long choice, and Weak short choice are in or reduce to APPROX, and compares these with Long choice and Short choice.","tokens_in":47008,"tokens_out":10989,"duration_ms":129257,"significance":"If the headline characterizations are established, the paper makes a substantial contribution: it supplies natural TFNP classes sitting above the standard ones, connects PSPACE and the polynomial hierarchy to Frege and constant-depth Frege in the TFNPdt framework of [GHJ+22], and gives a clean computational route to APPROX and its applications to Ramsey. The framework of Inspector-Adversary games is a genuinely useful organizing idea, and the paper contains several explicit, carefully written reductions, such as the proof that Weak long choice is in APPROX (Proposition 7.14) and the independence result for parity axioms (Theorem 4.7). The paper is open about what is new versus translated from bounded arithmetic, and it does not engage in parameter-fitting: the dependence on [ST11] and [BB17] is explicit and appropriate. However, the central Frege and constant-depth Frege characterizations currently rest on an asserted and non-obvious passage from type-2 problems to decision-tree TFNP problems in Section 9.1, which needs to be made rigorous before the paper's main claim is fully supported.","major_comments":[{"comment":"The transfer from type-2 TFNP to TFNPdt is asserted rather than proved, and the assertion is not automatic. In TFNPdt (Definition 8.1) the input length is quasipolynomial in a and every solution predicate must be decidable by a decision tree of depth poly(log a). A type-2 problem, by contrast, is solved by a polynomial-time oracle machine whose input includes a quasipolynomial-length string β; converting that machine into decision trees in the natural way gives depth polynomial in a, not poly(log a), because the machine may query polynomially many positions of β. This matters concretely for Local-ΓTQBF: checking that a branch α is good requires evaluating QBFs with D-gates under axiom 3 of ΓTQBF as modified in Definition 9.1, and nothing in Section 9.1 bounds the size of the QBFs appearing on a depth-log a branch or the number of δ-queries needed to evaluate them. Therefore Corollary 9.3 does not follow from Proposition 9.2, and Corollary 9.8 does not follow from Corollary 9.7. Since Proposition 8.7 is the paper's headline, this is a load-bearing gap: the claimed Frege and constant-depth Frege characterizations of Local-ΓTQBF and Local-Γ_k^TQBF require a separate uniform argument showing that the relevant reductions and solution predicates can be made shallow.","section":"Section 9.1 and Corollaries 9.3, 9.8"},{"comment":"The equivalence Local-ΓPSPACE ≡ Local-ΓTQBF is stated as a theorem but is only sketched. Lemma 5.5 in particular relies on formalizing the assertion ∀u∃!v Reach_i(u,v) as a QBF and on converting a failure of ΓPSPACE into a failure of ΓTQBF by binary search, but the encoding of the uniqueness quantifier and the exact transformation of a failed PSPACE computation into a TQBF axiom violation are not spelled out. This equivalence is later used in Corollary 9.7 to transfer the FCon characterization, so the section would be easier to verify if the missing details were supplied.","section":"Section 5.1, Theorem 5.3 and Lemmas 5.4-5.5"}],"minor_comments":[{"comment":"The outline says that Section 4 shows the subclass arising from ⊕P is PPAD; the actual theorem (Theorem 4.1) says PPA. Please correct the typo.","section":"Section 1.5"},{"comment":"The sentence 'Retraction weak pigeon becomes Left pigeon if we replace [2n+1] with [2n+1]' is garbled; the intended comparison with Left pigeon, with the roles of pigeons and holes and the intervals involved, should be stated carefully.","section":"Definition 6.2(5)"},{"comment":"In the paragraph beginning 'For non-leaf nodes u', the nodes v and w are called 'parents' of u; in the tree T they should be 'children'. In addition, the construction of the circuit describing the graph G is only asserted, with the statement that the details are clear; a few explicit encoding sentences would help.","section":"Proof of Lemma 4.5"},{"comment":"In the displayed cedent for a clause of CNF(GI_4), the first disjunct is written as x1 ≠ f_i^1(x'_i), which appears to be a typo for x1 ≠ f_i^1(x'_1).","section":"Proof of Lemma 8.14"}],"recommendation":"major_revision","confidential_remarks":"The main gap is real and fixable: the authors need to add a formal treatment of the decision-tree versions of their Local-Γ problems and prove the type-2-to-TFNPdt transfer with explicit depth bounds. Once that is in place, I expect the Frege and constant-depth Frege characterizations to be defensible, and I would support acceptance. I would not require the authors to re-prove the bounded arithmetic characterizations of [ST11] and [BB17], but they should state exactly which version of those theorems they are importing."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper is worth reading. Thapen's Inspector-Adversary games give a clean, uniform way to generate TFNP subclasses from an axiomatization of a complexity class, and the concrete dividends are real: PPA from parity axioms, PLS from P^NP, a simplified APPROX, and direct reductions of Ramsey to it. The proofs of these parts are careful and mostly self-contained. The PPA-from-parity theorem (Theorem 4.1) is particularly nice, with a genuinely combinatorial proof of the hard direction.\n\nThe headline, though, is the Frege and constant-depth Frege characterizations of the Local-Γ classes (Proposition 8.7). These are important if true, but the proof leans on the equivalence between the type-2 versions of Local-Γ and the decision-tree classes GI_k and FCon (Corollaries 9.3 and 9.8). That bridge is the soft spot. Section 9.1 asserts that a type-2 problem naturally becomes a TFNPdt problem, but nothing in the text shows the required reduction depth is polylogarithmic. A protocol of depth log a can still produce queries of length poly(a), and evaluating a quantifier-free circuit with D-gates on such a query can require poly(a) bit queries to the oracle. So, as written, the decision-tree version of Local-ΓTQBF is not even clearly in TFNPdt under the natural conversion, and the equivalence with FCon is not established. The same issue affects the GI_k equivalence. This is not necessarily fatal—the author notes these characterizations are essentially implicit in [ST11, BB17]—but the paper should either prove the decision-tree equivalence directly or state it as an assumption.\n\nOther gaps are minor: Theorem 5.3 is a sketch, Lemma 4.5 leaves circuit details to the reader, Theorem 5.10 is described as a sketch. These are acceptable in a paper of this scope, but they do lower the soundness estimate a notch.\n\nWho is this for? Researchers in TFNP and proof complexity. They will get a new viewpoint and several useful reductions. The APPROX simplification is a genuine contribution. I would send this to a serious referee—it deserves expert scrutiny, not desk rejection. The referee should focus on Section 9.","headline":"A worthwhile framework paper whose Frege characterizations rest on an unproven type-2/decision-tree bridge in Section 9.","tokens_in":47515,"tokens_out":11201,"would_cite":true,"duration_ms":121060,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03F20","68Q15"],"pacs":[],"model":"deepseek-v4-flash","headline":"Large complexity classes such as PSPACE and the polynomial hierarchy can be encoded as TFNP subclasses whose complete problems are characterized by the Frege and constant-depth Frege proof systems.","keywords":["TFNP","total search problems","Inspector-Adversary games","counterexample reducibility","Frege proof system","constant-depth Frege","bounded arithmetic","approximate counting"],"falsifier":"Find a narrow unsatisfiable CNF family with quasipolynomial-size Frege refutations whose false-clause search problem is not reducible to $\\mathrm{Local}\\text{-}\\Gamma_{\\mathrm{TQBF}}$ (equivalently, to FCon). Proposition 8.7 predicts this cannot happen; the standard lower-bound methods for constant-depth Frege are the place to look for such a counterexample.","tokens_in":46510,"feed_emoji":"🧩","tokens_out":12046,"duration_ms":114597,"temperature":0.7,"pith_summary":"This paper gives two general ways to build subclasses of TFNP, the class of total NP search problems, from computational objects that live outside TFNP. The first is an Inspector-Adversary game: an untrustworthy Adversary claims to answer queries to some complexity class, and the resulting search problem asks for a run of a querying protocol that does not catch the Adversary in a contradiction. The second is counterexample reducibility for $\\mathrm{TF}\\Sigma_2^p$ problems, where a proposed solution is accepted unless a counterexample to the Adversary's answer is produced. The paper's headline results are that the subclass built from PSPACE is characterized by the Frege proof system, and the subclasses built from the polynomial hierarchy are characterized by the constant-depth Frege hierarchy. A reader should care because this extends the known dictionary between TFNP subclasses and propositional proof systems to much stronger systems, giving PSPACE and the polynomial hierarchy a concrete computational footprint inside total search problems.","feed_headline":"Frege proofs pin down a new TFNP subclass","feed_subtitle":"An Inspector-Adversary game turns PSPACE and the polynomial hierarchy into total search problems.","key_machinery":"The load-bearing object is the Inspector-Adversary game, packaged as $\\mathrm{Local}\\text{-}\\Gamma$. An Inspector sends queries about a formal oracle $A$ to an Adversary who is only constrained by universal axioms $\\Gamma$; the Adversary must answer consistently, and the Inspector wins by either producing a solution to a target search problem or exposing an axiom failure. When $\\Gamma$ has a real model, $\\mathrm{Local}\\text{-}\\Gamma$ is a total search problem and is complete for the problems solvable over $\\Gamma$. The second mechanism is counterexample reducibility: for a $\\mathrm{TF}\\Sigma_2^p$ problem $R$, the TFNP problem Checkable $R$ asks, given an input $x$ and a circuit $C$, to find $y$ such that $R(x,y,C(y))$ holds. This turns a coNP-verifiable totality notion into a concrete search problem, and yields PLS and PPADS as Checkable versions of $P^{NP}$ computation and Empty. The QBF axioms $\\Gamma_{\\mathrm{TQBF}}$ and their depth-restricted fragments $\\Gamma^k_{\\mathrm{TQBF}}$ are what connect the construction to proof systems: a run avoiding axiom failures corresponds to a Frege or depth-restricted Frege refutation via the decision-tree reductions of Section 8.","core_discovery":"At the center of the first construction is the problem $\\mathrm{Local}\\text{-}\\Gamma$: given a polynomial-time protocol with an oracle tape named $A$, find a sparse oracle of replies under which the protocol does not witness the failure of any axiom in a fixed finite list $\\Gamma$. If $\\Gamma$ holds for some genuine total oracle, $\\mathrm{Local}\\text{-}\\Gamma$ is total, and it is complete for the class of TFNP problems solvable over $\\Gamma$. The paper proves that parity axioms give a class complete for PPA; that two quite different axiomatizations of PSPACE, one by true quantified Boolean formulas and one by PSPACE computations, give equivalent problems; and that the restricted problems $\\mathrm{Local}\\text{-}\\Gamma^k_{\\mathrm{TQBF}}$ are equivalent to the previously studied $GI_k$ problems and are characterized by depth-$(k+1/2)$ Frege, while $\\mathrm{Local}\\text{-}\\Gamma_{\\mathrm{TQBF}}$ is equivalent to Frege consistency and is characterized by Frege. On the counting side, it recasts the approximate-counting class APPROX as the class of TFNP problems counterexample-reducible to the $\\mathrm{TF}\\Sigma_2^p$ weak pigeonhole principle, gives a direct reduction of Ramsey into APPROX, and shows that weakened forms of Long choice and Short choice live in APPROX.","pith_inferences":["A direct, logic-free reduction of Ramsey to $\\mathrm{Local}\\text{-}\\Gamma_{\\mathrm{TQBF}}$ (or to $\\mathrm{Local}\\text{-}\\Gamma^k_{\\mathrm{TQBF}}$) would be a clean certificate that the Frege characterization captures the right class; the paper's reduction to APPROX is an intermediate step in that direction.","If Toda's theorem can be simulated in the $\\Gamma_\\#$ game, then the entire polynomial-hierarchy class would collapse into the single problem $\\mathrm{Local}\\text{-}\\Gamma_\\#$, giving a new algebraic proof system equivalent to constant-depth Frege with counting gates; the paper explicitly leaves this as an open direction.","The same construction applied to EXPTIME, which the paper expects to be connected to extended Frege, would put a class above the Frege 'hat'; this is a natural next test of whether the Inspector-Adversary recipe is a general correspondence between oracle complexity classes and proof systems."],"forward_implications":["The single TFNP problem $\\mathrm{Local}\\text{-}\\Gamma_{\\mathrm{TQBF}}$ contains PLS, PPA, PPP and their subclasses by natural reductions, and any TFNP problem with quasipolynomial-size Frege proofs of totality reduces to it.","Consecutive levels of the polynomial-hierarchy-in-TFNP hierarchy $\\mathrm{Local}\\text{-}\\Gamma^k_{\\mathrm{TQBF}}$ are characterized by depth-$(k+1/2)$ Frege, so separating these levels is equivalent to the long-standing open problem of separating depth-$k$ from depth-$(k+1)$ Frege.","Every TFNP problem counterexample-reducible to the $\\mathrm{TF}\\Sigma_2^p$ weak pigeonhole principle lies in APPROX, and Ramsey, Weak pigeon, Localopt, Checkable tournament and Checkable Min all lie in APPROX, while APPROX does not contain PPAD.","Weak long choice is a nontrivial intermediate: both Ramsey and Weak pigeon reduce to it, yet it lies inside APPROX, so the counting power needed for Ramsey can be separated from precise counting."],"supporting_citations":[{"why":"Introduces TFNP and the many-one reduction notion that all the paper's classes build on.","marker":"[JPY88]"},{"why":"Supplies the parity-counting and Nullstellensatz techniques used to prove that the local parity game is complete for PPA.","marker":"[BKZ15]"},{"why":"Introduces the GI_k hierarchy and its bounded-arithmetic characterization, which Section 9 uses to identify the polynomial-hierarchy classes.","marker":"[ST11]"},{"why":"Introduces FCon and its bounded-arithmetic characterization, the bridge to the PSPACE class and the Frege characterization.","marker":"[BB17]"},{"why":"Provides the decision-tree TFNP and proof-system dictionary plus the separations used to position the new classes.","marker":"[GHJ+22]"},{"why":"Defines APPROX and its PLS counterexample reducibility, which Proposition 7.3 simplifies to plain counterexample reducibility.","marker":"[KT22]"},{"why":"Introduces Long choice and Short choice, the problems the paper weakens and places inside APPROX.","marker":"[PPY23]"},{"why":"Gives the bounded-arithmetic proof that Ramsey follows from weak pigeonhole counting, adapted here to a direct reduction to Weak long choice.","marker":"[Pud90]"}],"fun_headline_variants":["Oracle games turn PSPACE and parity into TFNP subclasses","A game for TQBF yields new TFNP classes linked to Frege","Ramsey reduces into a new TFNP class via counting","Local-Γ games characterize PPA, PLS, and Frege consistency"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The Section 9 equivalences between the $\\mathrm{Local}\\text{-}\\Gamma$ problems and the $GI_k$ and $FCon$ problems presuppose that the published bounded-arithmetic characterizations of $T^k_2$ and $U^1_2$ transfer unchanged to the type-2 versions of these problems, and that the type-2-to-decision-tree correspondence preserves the relevant reductions.","fun_headline_variants_meta":{"raw":{"variants":["Oracle games turn PSPACE and parity into TFNP subclasses","A game for TQBF yields new TFNP classes linked to Frege","Ramsey reduces into a new TFNP class via counting","Local-Γ games characterize PPA, PLS, and Frege consistency"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001063,"raw_usage":{"total_tokens":4493,"prompt_tokens":1014,"completion_tokens":3479,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":630,"completion_tokens_details":{"reasoning_tokens":3403}},"tokens_in":630,"tokens_out":3479,"duration_ms":33138,"temperature":1.0,"reasoning_tokens":3403,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T16:28:38.839730+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Find a narrow unsatisfiable CNF family with quasipolynomial-size Frege refutations whose false-clause search problem is not reducible to $\\mathrm{Local}\\text{-}\\Gamma_{\\mathrm{TQBF}}$ (equivalently, to FCon). Proposition 8.7 predicts this cannot happen; the standard lower-bound methods for constant-depth Frege are the place to look for such a counterexample.","supporting_citations":[],"review_version":1}