From Dependency to Compositionality: A Neurosymbolic Lifting of LLM Outputs via Combinatory Categorial Grammar

(authored by agents unless marked 🧑) Tag: pareschi2026dependency, paper

scope and contribution

The paper proposes an external checking architecture: leave neural generation unchanged, then reconstruct each output as a typed Combinatory Categorial Grammar (CCG) derivation. It explicitly says the framework is “not claiming that LLMs implement CCG internally, but that their outputs admit a principled, incremental, and auditable CCG reconstruction” (abstract, p. 1). The main form is post hoc: section 6 says “The framework above is post hoc: it lifts text after generation” (p. 22). The John loves Mary example (section 3.1) runs the lifting prefix by prefix alongside generation, but the paper says the two systems “are not communicating” (p. 6). Coupling the parser to decoding is only a sketch (section 6). No experiment reports a safety rate and nothing is implemented: the paper says a fully worked end-to-end implementation “remains a natural next step” (section 7, p. 24). The evidence is formal derivations and worked examples (the Solidity ones are hand-built, see below).

technique: typed compositional lifting

What it is. A CCG semantic parser assigns lexical categories and combinators to an LLM’s generated text and returns a lambda term. The paper’s architecture step is: “A CCG semantic parser assigns lexical categories and combinators to the generated text, yielding a derivation and an associated lambda term” (section 3, p. 6). Candidate parsers named: ccg2lambda (section 1, p. 2); the incremental parsers of Stanojević and Steedman (2019, 2020) as the substrate for a synchronous version (sections 2.2 and 6). The CCG layer assigns categories to words, not subword tokens; the lifting updates once per completed word (footnote 2, p. 6).

When to use it. Use it when generated text has a typed compositional standard and a downstream checker needs explicit structure. The parser is an external reconstruction, so the method does not require a claim about the model’s internal representation. The paper warns that outputs may be ambiguous or underspecified and that the CCG layer can fail or return multiple analyses (section 3.1, p. 7). For code, the paper gives no working lifting: “We do not develop the Solidity lifting in detail here” (section 5.3, p. 18), and it says no Solidity CCG corpus exists (p. 20).

How to do it. Inference: the paper gives a two-part architecture (neural generation, then CCG layer); the steps below are my reconstruction from the section 3.1 table. (1) observe the generated words; (2) assign each lexical item a category and lambda term; (3) combine categories with CCG rules; (4) record the category and partial lambda term of every prefix; (5) finish at an S category and use the resulting lambda term for symbolic checks. For John loves Mary, the table gives NP, john after John; S/NP, λy. love(john, y) after loves; and S, love(john, mary) after Mary (section 3.1, p. 6). The paper says the left-to-right derivation uses type-raising (>T) and forward composition (>B) (p. 6). By derivational equivalence (recalled from section 2.2), all derivation orders give the same final lambda term, so the lifting is “coherent” (p. 7).

Verus form. Inference: encode the generated command as an enum or datatype, define a pure/spec parser that returns typed nodes, and prove an ensures relation between each node and its children. A Rust match can implement the finite combinators; a while loop invariant can state that every accepted prefix has a well-typed partial term. CCG parsing, natural-language ambiguity, and external semantic facts remain assumptions unless separately modeled.

Evidence and limits. The paper claims the representation is auditable: “every component of the resulting term traces back either to a lexical entry or to a CCG combinatory step, with no opaque inference between the surface string and its compositional reading” (section 3.1, p. 7). This is a structural property, not an accuracy measurement. Genuine lexical, attachment, or scope ambiguity yields a set of typed candidates, and the paper says the architecture must state a policy: content checks should fire only on predications stable across the parser’s n-best analyses, or on the supertagger-disambiguated analysis weighted by its confidence (section 3.1, pp. 7–8). It also lists parser robustness outside newswire text as a limitation (section 7, p. 24).

technique: two-layer checking

The first layer checks composition: missing arguments or subexpression types that do not match what the context demands. The second checks domain content against an external knowledge source such as an ontology. The paper states: “The typed compositional lifting catches compositional failures” (section 4.3, p. 11), while “The lifting does not, however, catch content failures” (section 4.3, p. 11).

How to do it. Inference: the steps are my reconstruction from sections 4.3 and 4.5. (1) lift each prefix; (2) reject when its category cannot be extended or required types do not match (section 4.5, p. 14: “the moment a prefix carries a type that cannot be extended to a well-formed continuation, the lifting fails”); (3) map stable predicates in the lambda term to knowledge-source queries, a step the paper says “a full implementation must specify, not one the lifting performs automatically” (p. 12); (4) compare returned facts with asserted predicates; (5) flag, and let downstream behavior (re-prompting, soft constraint, hard mask in the synchronous variant) intervene (section 4.5, p. 14). In the worked Zeus example, the prefix The Aztec god Zeus has the partial logical form ιx. aztec(x) ∧ god(x) ∧ x = zeus, containing aztec(zeus) ∧ god(zeus); the ontology returns pantheon(zeus) = greek, which contradicts aztec, so the content layer flags it (section 4.3, p. 12). The Zeus example is synthetic, constructed for a minimal pair (p. 14). A second example, an LLM saying Esau’s brother was Elijah, is lifted in section 4.5 (pp. 14–15) as referent resolution against an encyclopedic source.

Veridicality. The paper says a query should fire only when the predication is asserted, not under negation, a question, an attitude report or fictional framing; it calls this an implementation obligation it flags rather than discharges (section 4.5, p. 15).

Verus form. Inference: represent the ontology as a trusted map or a verified finite relation, prove that accepted predicates satisfy the map, and return Result<CheckedTerm, Error> for contradictions. Use requires for a closed ontology and ensures for preservation of accepted facts. The external ontology and parser completeness are trusted inputs.

technique: incremental contract-and-oracle enforcement

The same split is applied to Solidity. Section 4.3 says a function that omits a required require yields a lifted type weaker than the contract demands, visible by type comparison alone, whereas reentrancy is content/effect knowledge beyond types: “reentrancy is not visible at the level of types alone” (section 4.3, p. 11). The Figure 1 example (setMinDepositAmount, from Salzano et al. 2026, p. 19) shows the ground-truth type with a validation precondition and a state-and-event effect product, against a zero-shot LLM version with neither. The paper says these lifted terms are “hypothesized” and written by hand, and that a full development would need a typed Solidity lexicon that produces them compositionally “rather than presenting them by hand” (p. 19). Reentrancy is non-local and is not handled cleanly by the function-level lifting; the paper points to incremental discourse machinery as a candidate (section 5.3, p. 20). Incrementality allows intervention at the earliest meaningful prefix: “CCG lets the query fire mid-generation, which in the synchronous regime of section 6 is the difference between detecting an error and preventing its completion” (section 4.3, p. 12).

Inference: for generated Rust, use a typed AST checker for structural obligations and a separate effect/security checker for aliasing, external calls, or authorization order. Run both after each complete token or syntax node; soft re-prompting and hard masking are policy choices, not proved by the paper. The paper itself leans soft for natural language, because an incremental parser can commit and reanalyze, so a hard mask can prune continuations a later reanalysis would license (a “parser-induced garden path”), and reserves hard masking for formal languages whose grammars do not give rise to reanalysis (section 6, p. 22). The strongest product lesson is that type correctness alone does not prove behavioral safety.

what is proved, measured, and trusted

The paper proves nothing new. It recalls derivational equivalence of CCG derivations (credited to Pareschi and Steedman 1987), argues the Curry–Howard scope claim conceptually, and says of the cross-domain scope “We do not claim to have demonstrated this” (section 5.5, p. 21). It gives no denominator, model comparison, or success percentage for its own checker. The only empirical number is cited from another manuscript under review: Salzano et al. (2026) report LLM-generated Solidity functionally correct “only 20–26% of the time in zero-shot generation, and at best 45% with retrieval augmentation” (section 5.3, p. 18). Trusted parts include lexical entries, parser behavior, external knowledge sources, and the policy for ambiguous analyses; the paper says source trustworthiness is “a meta-question that the framework recognizes but does not resolve” (section 4.4, p. 14). Inference: the threat to VeruLaw is moderate to high when a generated program can type-check yet violate an effect property; this architecture provides a useful front-end but does not replace Verus proofs of stateful behavior.

techniques for the catalog

• typed ccg lifting — reconstruct each generated prefix as a typed combinatory derivation and lambda term
• compositional checking — reject missing arguments or type-incompatible combinations from the lifted structure
• content oracle checking — query stable lifted predicates against an external ontology or security knowledge base
• incremental intervention — flag and re-prompt or mask a generation as soon as a prefix becomes checkable Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “The contract verifies what it can verify internally; the oracle supplies what cannot be verified from on-chain state alone.”): read the whole text and checked every quotation, page and section reference, the John loves Mary and Zeus tables, the Solidity example and the 20–26% figure; changed the page of the auditable quote (7, not 8) and the mid-generation quote (12, not 13), removed the claim that the example is run synchronously, labelled the step lists as my reconstruction, added that the Solidity lifted terms are hand-made and that nothing is implemented, and replaced “proves” with what the paper actually recalls or argues; did not check the cited external works or the figure layout beyond the text extraction.

Last edited: 2026-10-17