PICARD
Constrained beam search that rejects invalid tokens at every decoding step using an incremental Haskell SQL parser and database schema type-checker.
The loop
- Proposes
A sequence-to-sequence language model (T5) proposes top-k next tokens across active beam hypotheses.
- Judged by
An incremental monadic parser and relational schema checker verify lexical, syntactic, and column/table scoping validity on every partial prefix.
- Steers
Invalid token continuations are masked to negative infinity before beam pruning, keeping only grammar- and schema-valid queries in the beam.
Headline result
Boosted T5-3B exact-match and execution accuracy on Spider and CoSQL benchmarks by 4-7 percentage points and eliminated 98% of syntax and schema errors.
What this does not prove
Enforces grammatical and schema well-formedness, but cannot prevent a semantically plausible query that filters on the wrong column value.
How it generalizes the harness
An incremental formal parser and relational type-checker gate every step of beam search, pruning invalid prefixes online.
Classification
| What it proposes | Program |
|---|---|
| Generative model | T5-3B sequence-to-sequence model |
| Algorithmic authority | Incremental monadic SQL parser and relational schema type-checker |
| Feedback | Verifier errors |
| What gets updated | Search tree |
| When it runs | At inference time |
| Validity | Formal (machine-checked) |
| Evidence | Code released |
| Lineage | Original system |