llama.cpp's GBNF constrained sampler is exact at codepoint boundaries but unsound for mixed-length character classes
Constrained decoding with GBNF is how the llama.cpp ecosystem (Ollama, LM Studio, llama-cpp-python, and the agent stacks built on them) forces a model to emit only strings a grammar allows: JSON, tool-call arguments, schemas. The advertised guarantee is that the per-token mask it applies at each step leaves a token unmasked if and only if appending that token's bytes keeps the output a viable prefix of the grammar language. This project audits that guarantee exactly. It builds an independent byte-level Earley recognizer, computes the true viable-prefix mask over the full 151936-token Qwen2.5 vocabulary at every reachable grammar state, and diffs it token-for-token against the mask llama.cpp actually produces.
The result has two parts. At every state reachable by whole Unicode codepoints, across a diverse grammar corpus, the two masks are identical: llama.cpp's simple byte-walking matcher is an exact token-level recognizer, which is not obvious (the guidance / XGrammar line of work builds token-aligned automata for exactly this and treats the naive matcher as merely a fallback). But there is a real hole. When a character class or alternation mixes codepoint literals of different UTF-8 byte lengths, and the decoder is in the middle of a multibyte codepoint, llama.cpp's mask is unsound: it leaves unmasked continuation bytes that can never encode the intended codepoint. Following only bytes the mask itself allows, the constrained decoder can then be led to emit a complete string that is not valid UTF-8 and not in the grammar language, with the sampler signalling end-of-sequence as if the output were a valid grammar member.
Oracle A is an independent GBNF frontend and a byte-level Earley recognizer, code-disjoint from llama.cpp. It expands every codepoint literal and range into explicit UTF-8 byte terminals, so partial-codepoint handling falls out of ordinary byte scanning, and answers two decidable queries on a byte prefix: viable (the Earley chart still has a live item) and member (a completed start item spans the whole input). The mask under audit is read through the libllama C API (Homebrew build 9760): construct a grammar sampler, drive it to a state by accepting tokens, apply it to a uniform logit array over the whole vocabulary, and record which tokens keep a finite logit. State space is walked by a bounded BFS that expands only through tokens both recognizers accept, so llama and the oracle stay in equivalent, well-defined states.
Two controls make the null (agreement) result meaningful and the oracle trustworthy:
- Positive control: drive llama and the oracle with deliberately mismatched grammars ([a-y]+ against [a-z]+), which injects a known set of deviations, and confirm the differential flags exactly that set. Recall and precision are both 1.0 (432 of 432, in both the over-restrictive and unsound directions), so the harness provably detects a real mask disagreement.
- Cross-oracle: Oracle A is checked against independent byte-logic recognizers over 24193 prefixes (0
mismatches) and against a lark Earley parser on JSON membership. This rules out the case where Oracle A is
wrong in the same way llama.cpp is, which would make agreement meaningless. This check earned its place: it
caught a malformed astral escape in an early grammar (a backslash-u escape written with five hex digits,
1f600, which a 4-hex-digit parser reads as U+1F60 followed by the literal 0); llama.cpp supports the 8-hex
\U0001F600, verified and adopted.
Corpus of eight grammars (ASCII repetition, a euro-sign repetition, multibyte alternations with 2-, 3-, and 4-byte codepoints, a mixed ASCII-and-multibyte sequence, an astral-in-structure grammar, and canonical and nested JSON). Over roughly 360 enumerated states, every state reached through whole codepoints shows the llama mask equal to the exact viable-prefix mask. The five grammars whose reachable states all sit on codepoint boundaries (the ASCII repetition, the euro repetition, the mixed sequence, and both JSON grammars) show zero deviations across every state: the ASCII grammar agrees on all 16833 lowercase-containing tokens, and the JSON grammars agree at every state. Byte-fallback tokens (lone 0x80-0xFF) are covered because the diff is over the entire vocabulary at every state, and none is ever wrongly unmasked at a clean state. EOS is unmasked exactly when the accepted string is a complete grammar member. So wherever a token boundary lands on a codepoint boundary, the byte-walking matcher is an exact recognizer.
The three grammars whose char class mixes codepoint lengths (the multibyte alternations) are the ones that deviate, and only at states in the middle of a multibyte codepoint. The automated audit flags both the spurious continuation byte (class UNSOUND) and, by following only bytes llama's own mask allows onward from it, the downstream state where llama signals EOS on a string the exact oracle rejects (class EOS_UNSOUND, the emitted invalid string). The next section is the minimal case.
The hole appears only when the decoder is partway through a multibyte codepoint, which happens whenever a byte-fallback token splits a codepoint, and only when the grammar offers a character class or alternation of codepoint literals of different UTF-8 lengths.
Minimal reproducer. Grammar root ::= ("\u4e16" | "\U0001F600") accepts exactly the 3-byte codepoint U+4E16
(bytes E4 B8 96) or the 4-byte codepoint U+1F600 (bytes F0 9F 98 80). Accept the lone byte F0 (a real
vocabulary token, and the only legal first byte of the emoji). The only viable next byte is 9F. But llama.cpp
also leaves the byte 0x84 unmasked, and the exact oracle rejects it:
grammar (U+4E16 | U+1F600): after F0, llama allows byte 0x84? True exact oracle: F0 84 viable? False
grammar (U+1F600) : after F0, llama allows byte 0x84? False exact oracle: F0 84 viable? False
The single-literal grammar is exact; the alternation is not. The cause is in llama_grammar_match_partial_char
(src/llama-grammar.cpp, build b9760). For a partial UTF-8 sequence it computes the numeric range of code
points that partial could complete to,
uint32_t low = partial_value << (n_remain * 6);
uint32_t high = low | ((1 << (n_remain * 6)) - 1);
and accepts if any alternative's code point falls in [low, high]. It never checks that the bytes already
consumed are consistent with that alternative's UTF-8 length. After F0 then 0x84 the partial value is 0x04
with two 6-bit groups still to come, giving the range [0x4000, 0x4FFF]. U+4E16 lands in that range, so the
byte is accepted, even though F0 is a 4-byte lead that cannot begin the 3-byte codepoint U+4E16 at all. This
is exactly why U+4E16 triggers the bug and the euro sign U+20AC does not: 0x4E16 is inside [0x4000, 0x4FFF]
and 0x20AC is not.
Predictive model. The single spurious byte admitted after F0 for a shorter class alternative C is exactly
0x80 | (C >> 12). Tested across six code points, the model is exact in every case; the only other byte ever
admitted is 0x9F, the emoji's legitimate second byte:
| shorter alternative C | C >> 12 | predicted spurious byte | observed |
|---|---|---|---|
| U+4E16 | 0x4 | 0x84 | 0x84 |
| U+5E16 | 0x5 | 0x85 | 0x85 |
| U+6E16 | 0x6 | 0x86 | 0x86 |
| U+4123 | 0x4 | 0x84 | 0x84 |
| U+7ABC | 0x7 | 0x87 | 0x87 |
| U+3055 | 0x3 | 0x83 | 0x83 |
Consequence. This is not a harmless dead end. Follow only the bytes llama's own mask leaves unmasked, starting from the spurious 0x84. After 0x84 the mask forces 0xB8, then 0x96, and then the sampler signals EOS:
after F0: 2 tokens allowed (0x84 spurious, 0x9F legal) oracle: viable, not member
after F0 84: 1 token allowed (0xB8) oracle: not viable
after F0 84 B8: 1 token allowed (0x96) oracle: not viable
after F0 84 B8 96: EOS allowed, sampler reports a complete member oracle: not a member
Every byte on that path was chosen from llama's own mask, so it is a genuine constrained-decoding output. The emitted string F0 84 B8 96 is the overlong four-byte encoding of U+4E16: it is not valid UTF-8, it is not the grammar's encoding of that codepoint (E4 B8 96), and it is not in the grammar language at all, yet the sampler accepts it and signals end-of-sequence. So the soundness guarantee, that a constrained decoder emits only strings in the grammar, is broken: this grammar class can emit a complete invalid, non-UTF-8 string and call it done.
Homebrew llama.cpp build 9760, Qwen2.5 tokenizer (151936 tokens), CPU only, vocabulary-only model load. The
exactness result and the bug both concern the per-token mask, which is the object that defines constrained
decoding correctness. The grammar subset covered is literals with escapes (including \uXXXX and
\U00XXXXXX), ASCII character classes, alternation, grouping, repetition, and the JSON grammars; general
multibyte character-class ranges are not modeled by the oracle and are out of scope. The bug is a property of
llama_grammar_match_partial_char and reproduces on any grammar whose character class mixes codepoint lengths;
it is reportable upstream with the minimal grammar above.
python bug_repro.py # minimal reproducer, predictive model, wedge consequence
python run_bfs.py # full differential audit over the grammar corpus -> results/bfs.json
python src/crossoracle.py # oracle cross-validationMIT.