{"id":"344dabba-2945-4888-a6d1-80a2ea32ade2","arxiv_id":"2608.03065","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"PSC precompiles the acceptance conditions of all vocabulary tokens into one finite-state automaton over parser stacks, making grammar-constrained decoding mask computation independent of vocabulary size at runtime.","lead":"This paper introduces PSC, a grammar-constrained decoding method that precomputes a finite-state classifier of the parser stack, so each decoding step computes the valid token mask in one stack pass instead of checking every vocabulary token. It reports up to 700x faster mask computation than prior methods and end-to-end LLM throughput close to unconstrained decoding.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 1's proof that P_epsilon is a finite-state transducer is incomplete: termination of P only bounds each individual ε-run, not the union of states over all stacks, so preprocessing finiteness is unproven for general DCFGs.","rationale":"The paper's central efficiency claim—O(|stack|) runtime independent of |V|—depends on preprocessing producing a finite DFA A. The only place finiteness is argued is Theorem 1, and the argument is a non sequitur: termination of P gives, for each fixed stack, a finite ε-derivation, but the FST state set is the union of states over all stacks. The AA→A example shows a terminating DPDA can have unbounded ε-run lengths, so a uniform bound does not follow from the stated definition. The experiments all use Lark LALR parsers, where reduction chains are bounded; this explains why preprocessing terminated in practice and why the speedups are credible, but it also means the theorem as stated over all terminating DPDAs is unsupported. The correct fix is either to prove a bound using the structure of LR parsers or to restrict the claims to that class. This does not invalidate the experimental contribution, but it must be settled before the general claim is accepted. I therefore keep the reader's CONDITIONAL verdict unchanged.","tokens_in":27668,"tokens_out":31815,"duration_ms":332679,"concrete_test":"Write a script that, for each terminating deterministic PDA with stack alphabet size at most 3 and at most 4 ε-transitions (termination checked by bounded exhaustive exploration), constructs the state closure of Equations 5 and reports whether the closure is finite. A single PDA with an infinite closure refutes Theorem 1; if every small PDA yields a finite closure, use the observed maximum state lengths to formulate and prove the missing invariant (e.g., |α| ≤ max(2, max_ε |β|) + K for a grammar-dependent constant K) and add it to the proof. This test decides whether the concern is a proof gap only or a false theorem.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The load-bearing point is the finiteness of P_epsilon in Section 3.3, Theorem 1. The FST states are arbitrary strings over the stack alphabet Π (Equations 5a and 5c), and the proof argues that termination of P rules out an endless ε-transition sequence, so \"this process can only introduce a finite number of new states before reaching a stable stack.\" That inference is invalid: termination of P means each individual stack has a finite ε-run, but P_epsilon must be one finite automaton for all possible input stacks. A terminating DPDA can have ε-run length unbounded over stacks—for the ε-rule AA→A, the run from A^n has length n−1—and Equations 5c can produce states whose length is |β|+|α|−2, which is not bounded by the argument given. If some terminating DPDA therefore yields infinitely many reachable states, the closure in Equations 5 never terminates, and P_w, A_w, and the final mask DFA in Equation 9 are undefined. This is independent of the experimental speedups, which use Lark LALR parsers where reduction chains are bounded by grammar size, but it is load-bearing for the paper's general correctness claim and for the guarantee that preprocessing always terminates.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes PSC (Parser Stack Classification), a grammar-constrained decoding method that precomputes a deterministic finite automaton over (lexer state, parser stack) pairs, so that the per-step vocabulary mask is obtained by a single traversal of the parser stack rather than by invoking the parser once per vocabulary token. The authors formulate the acceptance condition of each token as a finite-state transducer on the parser stack, compose these to build a single DFA, and report up to 700x faster mask computation on programming-language grammars and up to 30x on JSON schemas, with end-to-end throughput close to unconstrained decoding. The paper also provides an analysis of preprocessing cost and a break-even point for when users should preprocess themselves.","tokens_in":27918,"tokens_out":9612,"duration_ms":87560,"significance":"If the theoretical foundation is made sound, PSC is a significant contribution: it changes the per-step cost of grammar-constrained decoding from O(|V|) to O(|stack|) and removes all runtime parser calls, which is especially valuable for the 128k-262k token vocabularies of modern LLMs. The empirical study is extensive and carefully controlled (teacher-forcing for fair comparison, three model families, batch-size sweeps, and multiple baselines), and the reported speedups are large and internally consistent. The paper ships open-source code, datasets, and preprocessing results, which strengthens reproducibility. The principal risk is the proof of finiteness of the epsilon-closure transducer in Theorem 1; this must be repaired before the general DCFG claim is credible, although the experimental results for LALR grammars may remain valid regardless.","major_comments":[{"comment":"The proof that P_epsilon is a finite-state transducer is invalid. Termination of P bounds each individual epsilon-run, but P_epsilon must be a single finite FST for all possible input stacks. Equation 5c can produce states whose length is |β|+|α|-2, and if β has length greater than 2, state length can grow without bound across different stacks (e.g., a terminating epsilon-transition that temporarily pushes two symbols before popping them yields intermediate stack prefixes of length proportional to the number of input symbols read). Consequently, the closure defined by Eqs. 5 may not terminate, and P_w, A_w, and the DFA A in Eq. 9 are not guaranteed to exist for general terminating DCFGs. This is load-bearing for the paper's general correctness claims (Theorems 2 and 3), though not directly for the LALR-based experiments, where reductions are length-decreasing. Please either prove finiteness under an appropriate bounded-stack condition, or restrict the theoretical claims to a class of grammars for which the construction is finite.","section":"§3.3, Theorem 1 (Eqs. 5a-5c)"},{"comment":"The composition order in Algorithm 1, line 6, contradicts Equation 8. Equation 8 defines P_w = P_epsilon ◦ \\tilde{P}_{w_1} ◦ P_epsilon ◦ ... ◦ \\tilde{P}_{w_n} ◦ P_epsilon, which processes the terminals in the order w_1, ..., w_n. Algorithm 1 line 6 lists the composition as P_epsilon ◦ \\tilde{P}_{w_n} ◦ ... ◦ \\tilde{P}_{w_1} ◦ P_epsilon, which would process the terminal sequence in reverse. Since FST composition is order-sensitive, one of the two must be corrected; please also confirm that the implementation matches the corrected version.","section":"§3.4 and Algorithm 1, line 6 (vs. Eq. 8)"},{"comment":"The equivalence in Eq. 3 relies on the assumption that reaching a stable stack after reading a realizable terminal sequence w implies the existence of some continuation y with T(xvy) ∈ P. The paper calls this a 'common assumption' but provides no proof or formal condition on the grammar, and it is load-bearing: if some stable stack cannot be extended to a complete accepted string, the computed mask would admit invalid tokens. Please state this as an explicit assumption on the grammars (or prove it for DCFGs), and confirm experimentally or by construction that the grammars used in the evaluation satisfy it.","section":"§3.2, Equation 3"}],"minor_comments":[{"comment":"The contributions bullet in Section 1 says experiments were conducted on 'Java, Go, Python, and schema-conformant JSON', but Section 4.1 lists only Java, Go, SQL, and JSON schemas; Python never appears in the evaluation. Please align the two descriptions.","section":"§4.1 and Contributions list"},{"comment":"Typos: 'programmaing' should be 'programming' and 'perprocessing' should be 'preprocessing'.","section":"§5.1.2"},{"comment":"The legend label 'Upper bound (uncostrained)' should read 'Upper bound (unconstrained)'.","section":"Figure 3"},{"comment":"The heading 'Offline constructon in PSC' should be 'Offline construction in PSC'.","section":"Algorithm 1 heading"},{"comment":"Several references have garbled author lists, notably the McEval reference (with malformed author tokens) and the Llama 3 reference (with duplicated names). These should be cleaned up.","section":"References"},{"comment":"The near-100% sample pass rate of PSC is inherited from the adopted GreatGramma lexer; RQ1 does not independently validate PSC's mask correctness against a gold standard for the cases where the lexer succeeds, because all methods are designed to compute the same masks. The text should state this more explicitly to avoid overstating the correctness evidence for PSC itself.","section":"§4.2"}],"recommendation":"major_revision","confidential_remarks":"The main blocking issue is the finiteness proof of the epsilon-closure transducer. The empirical contributions are strong and likely reproducible, and the composition-order bug and stable-stack assumption appear fixable. I would not reject on the current evidence, but the theoretical claim needs to be either proved under appropriate assumptions or scoped down to the grammar class where the construction is finite."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Let me give you the short version. PSC is a systems result that deserves a serious look: it precomputes, for each vocabulary token, the regular language of parser stacks that accept that token, unions them into one FSA, and at runtime runs the parser stack through that FSA once per step. The experiments support the practical claim: mask computation around 2.4 microseconds per step versus 1000+ microseconds for the best baseline, and end-to-end throughput on small models approaches unconstrained decoding. They also did the fairness homework (teacher-forcing, three tokenizers, pass-rate checks) and shipped code and preprocessing results.\n\nNow the soft spot. Theorem 1 claims Equations 5 construct a finite-state transducer P_epsilon for any terminating deterministic PDA. The proof argues that because P terminates, only finitely many states arise. That doesn't follow. Termination bounds each individual epsilon-run; it doesn't bound the union of states reached by reading all possible stacks. You can have a terminating DPDA with one epsilon-rule AB -> AAB and no other epsilon-rules. Every stack has at most one epsilon-step, so the PDA is terminating, but the P_epsilon states are A, AB, AAB, AABA, ... — infinitely many stack strings. The construction never reaches a finite closure. So the general theorem as stated is not just unproven; it appears to be false.\n\nThe interesting thing is that the experiments use Lark LALR parsers, where the stack alphabet is finite and the LR automaton's viable prefixes form a regular language. For that class, a finite construction likely exists (their preprocessing did terminate on all tested grammars). But the paper states the theory for all terminating DCFGs, and that statement cannot stand without a different proof or a restriction to LR(k). This is a load-bearing issue for Section 3, though not for the measured speedups.\n\nMinor items: Equation 8 and Algorithm 1 give opposite composition orders for P_w; one of them is a typo. Timings have no variance reported. Pre^3 is excluded for lack of code, which is fair, but if the authors can get it, a comparison would strengthen the novelty claim. The citation pattern looks fine.\n\nWho should read it: anyone building or benchmarking constrained-decoding libraries; the empirical numbers are useful. It deserves peer review — the systems contribution is real and the theory can be fixed by scoping it properly. I would not desk reject it.","headline":"PSC has a genuinely fast practical idea and credible experiments, but its headline theorem about finite-state epsilon-closure is unproven and likely false for general DCFGs.","tokens_in":28414,"tokens_out":14302,"would_cite":true,"duration_ms":138826,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"By merging the acceptance conditions of every vocabulary token into a single automaton over parser stacks, PSC computes the full legal-token mask in one stack pass per decoding step, with cost independent of vocabulary size.","keywords":["grammar-constrained decoding","parser stack classification","finite-state automata","deterministic pushdown automata","structured output generation","vocabulary masking","LLM code generation"],"falsifier":"Run the offline construction (Algorithm 1) on a deliberately engineered terminating grammar whose epsilon-transitions push symbols that enable further epsilon-transitions, and observe whether the $P_\\varepsilon$ construction terminates; if the number of closure states grows without bound, Theorem 1's finiteness claim fails. A complementary check: measure PSC's per-step mask time with two very different vocabulary sizes — the central claim predicts flat time, whereas linear growth would contradict the vocabulary-independence result.","tokens_in":27467,"feed_emoji":"⚡","tokens_out":16744,"duration_ms":127386,"temperature":0.7,"pith_summary":"Grammar-constrained decoding makes an LLM's output respect a context-free grammar by masking illegal tokens at every generation step, but the usual way to build that mask is to ask the parser, for every one of the model's 100,000-plus tokens, whether that token is legal — work that grows linearly with the vocabulary. This paper proposes Parser Stack Classification (PSC), which inverts the question: during preprocessing it computes, for each token, the exact condition on the parser stack under which the token is legal, and merges all these conditions into a single automaton that classifies stacks. At generation time the automaton is run once over the current stack and the full mask comes out, so the per-step cost is independent of vocabulary size. On programming-language grammars the paper reports mask computation up to 700 times faster than the fastest comparison baseline, and end-to-end constrained throughput close to unconstrained decoding.","feed_headline":"One stack pass computes the grammar mask, up to 700x faster","feed_subtitle":"Precomputed token-acceptance automata remove vocabulary size from the per-step cost of constrained LLM decoding.","key_machinery":"The load-bearing object is the combined classifier automaton $\\mathcal{A} = \\bigcup_{v,q} \\bigcup_{w \\in R_q(v)} I_q A_w I_v$ (Equation 9): a minimized deterministic finite-state automaton over the alphabet of lexer states, stack symbols, and vocabulary tokens, with every state pre-mapped to the vocabulary mask it implies. Each per-token automaton $A_w$ derives from the transducer $P_w = P_\\varepsilon \\circ \\tilde{P}_{w_1} \\circ P_\\varepsilon \\circ \\dots \\circ P_\\varepsilon \\circ \\tilde{P}_{w_n} \\circ P_\\varepsilon$, which simulates the parser consuming the terminal sequence $w$ from an arbitrary stack and returning the stabilized stack. The critical component is $P_\\varepsilon$, the epsilon-closure transducer that fires all needed epsilon transitions to stabilize a stack; finiteness of its state set is what keeps the whole construction finite, and is the property the paper justifies by the parser's termination. Theorems 1 through 3 chain together to show the transducer simulation is exact and the resulting acceptance language is regular, so the online step reduces to a single traversal of the stack plus a table lookup.","core_discovery":"The paper's central claim is that validity checking in grammar-constrained decoding does not need to be done online, token by token. For a grammar parsed by a terminating deterministic pushdown automaton with a lexer modeled as a deterministic finite-state transducer, the set of (lexer state, parser stack) configurations from which a given vocabulary token can be legally appended is a regular language (Theorem 3), and PSC constructs that language explicitly. The construction builds a transducer $P_w$ that simulates the parser reading any terminal sequence $w$ starting from an arbitrary stack — epsilon transitions are handled by a stabilizer transducer $P_\\varepsilon$, and each terminal by a single-step transducer — then strips outputs to get an automaton $A_w$ for each realizable terminal sequence. All these automata are unioned, marked with lexer-state and token markers, and determinized and minimized into one automaton $\\mathcal{A}$ whose states each correspond to a precomputed vocabulary mask. Running $\\mathcal{A}$ once over the current stack ($O(|\\alpha|)$ time) and looking up the mask ($O(1)$) therefore reproduces exactly the mask that repeated per-token parsing would produce; the paper reports this mask is correct on essentially all tested samples, and that preprocessing, done once per grammar-and-vocabulary pair, has a quantified break-even point for prospective users.","pith_inferences":["The structural claim implies a directly measurable scaling law: doubling or tripling a model's vocabulary should leave PSC's per-step mask time essentially flat while baseline costs grow roughly linearly, a test that can be run on tokenizers and grammars alone, without model inference.","Because the finiteness of $P_\\varepsilon$ is inferred from termination rather than bounded, a natural stress test is a family of deterministic grammars with cascading nullable productions; if any terminating deterministic grammar defeats preprocessing, the practical scope of PSC would be narrower than the theorem suggests.","The same offline/online split — classify the configuration once, reuse the decision for every token — is not inherently tied to context-free grammars; any constraint device whose acceptance sets over configurations are regular could be accelerated the same way, including indentation-sensitive or typed output specifications."],"forward_implications":["Per-step mask computation drops from $O(|V|)$ to $O(|\\alpha|)$ plus a constant-time lookup, so vocabulary sizes in the hundreds of thousands no longer set the cost of constrained decoding.","End-to-end throughput with grammar constraints approaches unconstrained decoding, with the remaining gap smallest on small models and large batch sizes, where inference time per token is not the dominant cost.","Preprocessing is done once per (grammar, vocabulary) pair and its results can be shared, so model providers can amortize minutes-to-an-hour preprocessing of programming-language grammars across all users, while JSON-schema preprocessing takes about half a minute per schema.","The break-even analysis gives users a decision rule: self-preprocessing pays off after roughly half a minute of decoding for JSON schemas, and after noticeably longer for the more complex programming-language grammars."],"supporting_citations":[{"why":"Supplies the formal definitions of deterministic finite-state transducers and terminating deterministic pushdown automata on which the entire construction rests.","marker":"[4]"},{"why":"Brzozowski derivatives are used in the proof of Theorem 3 to reverse the combined automaton's language, establishing that per-token acceptance conditions are regular.","marker":"[10]"},{"why":"A state-of-the-art constrained-decoding engine whose per-step mask cost is a comparison point for the reported speedups.","marker":"[16]"},{"why":"Provides FSA determinization and minimization, closure properties of regular languages, and the conversion of deterministic PDAs into terminating form.","marker":"[24]"},{"why":"Establishes the correspondence between LR parsers and deterministic pushdown automata, grounding the use of LALR(1) parsers as the parsing PDA.","marker":"[25]"},{"why":"The fastest baseline in the experiments, against which the up-to-700x mask-computation speedup is measured.","marker":"[30]"},{"why":"Supplies the lexer preprocessing PSC reuses and the simplification of the validity condition (Equation 3) from which PSC's construction starts.","marker":"[33]"},{"why":"Cited for transforming deterministic PDAs into equivalent terminating deterministic PDAs, a precondition for the epsilon-closure transducer construction.","marker":"[38]"}],"fun_headline_variants":["700x faster GCD: one stack check replaces all token scans","Grammar masks in O(stack) time, not O(vocab)","PSC: single stack pass yields full grammar mask, 700x faster","O(stack) per step: stack classifier masks 700x faster"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The entire preprocessing pipeline rests on the assumption that the epsilon-closure of any parser stack is captured by a finite-state transducer with only finitely many states; the proof cites the parser's termination, but no bound is given on how long an epsilon-chain can grow, so a deterministic grammar that drove epsilon-closure through unbounded stack prefixes would make preprocessing fail to terminate or produce an infinite automaton.","fun_headline_variants_meta":{"raw":{"variants":["700x faster GCD: one stack check replaces all token scans","Grammar masks in O(stack) time, not O(vocab)","PSC: single stack pass yields full grammar mask, 700x faster","O(stack) per step: stack classifier masks 700x faster"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001647,"raw_usage":{"total_tokens":6585,"prompt_tokens":1030,"completion_tokens":5555,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":646,"completion_tokens_details":{"reasoning_tokens":5479}},"tokens_in":646,"tokens_out":5555,"duration_ms":37299,"temperature":1.0,"reasoning_tokens":5479,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T14:53:53.835883+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the offline construction (Algorithm 1) on a deliberately engineered terminating grammar whose epsilon-transitions push symbols that enable further epsilon-transitions, and observe whether the $P_\\varepsilon$ construction terminates; if the number of closure states grows without bound, Theorem 1's finiteness claim fails. A complementary check: measure PSC's per-step mask time with two very different vocabulary sizes — the central claim predicts flat time, whereas linear growth would contradict the vocabulary-independence result.","supporting_citations":[{"cited_title":"Aho and Jeffrey D","cited_arxiv_id":null,"evidence_quote":"Supplies the formal definitions of deterministic finite-state transducers and terminating deterministic pushdown automata on which the entire construction rests."},{"cited_title":"Brzozowski","cited_arxiv_id":null,"evidence_quote":"Brzozowski derivatives are used in the proof of Theorem 3 to reverse the combined automaton's language, establishing that per-token acceptance conditions are regular."},{"cited_title":"Ruan, Yaxing Cai, Ziyi Xu, Yilong Zhao, Ruihang Lai, and Tianqi Chen","cited_arxiv_id":null,"evidence_quote":"A state-of-the-art constrained-decoding engine whose per-step mask cost is a comparison point for the reported speedups."},{"cited_title":"Hopcroft and Jeffrey D","cited_arxiv_id":null,"evidence_quote":"Provides FSA determinization and minimization, closure properties of regular languages, and the conversion of deterministic PDAs into terminating form."},{"cited_title":"2025.LLGuidance: Making Structured Outputs Go Brrr","cited_arxiv_id":null,"evidence_quote":"The fastest baseline in the experiments, against which the up-to-700x mask-computation speedup is measured."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the lexer preprocessing PSC reuses and the simplification of the validity condition (Equation 3) from which PSC's construction starts."},{"cited_title":"2013.Introduction to the Theory of Computation(third edition, international edition ed.)","cited_arxiv_id":null,"evidence_quote":"Cited for transforming deterministic PDAs into equivalent terminating deterministic PDAs, a precondition for the epsilon-closure transducer construction."}],"review_version":2}