Provably Robust Multi-bit Watermarking for AI-generated Text

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

scope and formal object

Inference: The human notes already mention this paper in text_watermarking.md; this study supplies the missing algorithm steps, Verus translation, robustness model, and trust boundaries.

The paper defines multi-bit watermarking as two functions over an LLM, prompt, message, and generated token sequence. “Given an LLM, a message K, and a prompt token sequence P = [P0 · · · PN−1 ], a multi-bit watermark algorithm consists of the following two functions” (Definition 3.1, §3.1, p. 205). Embedding produces S and extraction produces K′. The target property is exact recovery after an edit-distance-bounded attack: “The edit distance between S and S′ is bounded by D (S, S′ ) ≤ η” (§3.2, p. 205). The design also requires efficient embedding/extraction (§3.2).

technique: segment assignment with green-list sampling

Use this when a message has many bits and assigning each bit independently to tokens creates severe frequency imbalance. The authors observe that previous methods partition continuous token groups (fragile to sentence deletion) or assign each token a bit segment (long messages receive too few samples for some positions) (§4.1.1, pp. 205–206). Their method packs b bits into k segments, with each segment holding b/k bits, and pseudo-randomly assigns every generated token to one segment using its previous token (§4.1.2, p. 206).

Steps from §4.1.2 (pp. 206–207) and §4.2 (p. 208): (1) choose k and divide K into k equal segments (in §4.2 these are then Reed–Solomon-encoded into n̂ segments, see below); (2) for each token, query a secret-keyed token-to-segment mapping M using the previous token; (3) compute seed s = hash(sk, previous token, segment value); (4) use s to select a green list G of half the vocabulary; (5) add bias δ to logits of G and sample the next token; (6) at extraction, enumerate every value for each segment, count how often each candidate’s green list contains observed tokens, and select the arg-max candidate. Figure 2 gives the concrete 8-bit message “01100011”, packed as segment values [1, 2, 0, 3], and labels the three operations as determining the segment index from the previous token, obtaining the seed from the previous token and segment value, and selecting the green list (p. 207).

The trade-off is explicit: extraction complexity is O(k·2^(b/k)); smaller k gives more tokens per segment and better accuracy but costs more enumeration, while larger k is cheaper and slightly less accurate (§4.1.2, p. 207). The paper’s Algorithm 1 and Algorithm 2 are executable pseudocode for embedding and extraction, including initialization, mapping, hashing, biasing, counting, and returning the decoded message (p. 209).

Inference: in Verus, represent the token sequence and segment counts as executable Rust, specify requires for key, vocabulary, and segment parameters, and ensures that each segment’s output is an arg-max of its counts and that the counts match the token sequence. Exact recovery even without edits is only probable in the paper (default match rate 97.6%, not 100%), so it cannot be a deterministic postcondition. A loop invariant would state that each processed token contributes to exactly one segment’s counts. The cryptographic hash and LLM sampler need trusted specifications or external_body; Verus cannot prove their statistical assumptions from this paper.

technique: frequency-balanced dynamic-programming mapping

Natural token frequencies make M imbalanced (§4.1.3, p. 207). The paper shuffles token IDs with the secret key, splits the shuffled vocabulary into n̂ groups of consecutive IDs, and chooses the split points by dynamic programming to minimize the sum of squared group frequency sums, which it states is equivalent to minimizing the variance of the group sums (§4.2, p. 208). It avoids an arbitrary (non-consecutive) split because that version reduces to the NP-hard partition problem (p. 208). Its recurrence D(i, j) partitions tokens with IDs in [0, i] into j groups; the stated complexity is O(n̂·|V|²), acceptable because it is performed once per Reed–Solomon scheme (p. 208).

Inference: implement the recurrence as a pure Verus spec fn plus a proved executable reconstruction, with an invariant that each dynamic-programming cell is the optimum over its stated prefix partition. The paper does not prove this in Verus; this is a translation of its algorithm.

technique: Reed–Solomon error correction and adaptive code selection

For substantial edits, segment values can be wrong. The method encodes K with a Reed–Solomon code over GF(2^m), then chooses (n,k,t) by filtering candidates with km = b, code rate k/n ≥ Rc, and recovery rate t/n ≥ Rr, selecting the lowest n (§4.2, p. 208; Algorithm 3, Appendix B, p. 219). Table 3’s discussion nonetheless says the selection does not always pick the smallest n (p. 213). Extraction takes arg-max segment values and Reed–Solomon-decodes them (Algorithm 2, p. 209).

Theorem 4.1 bounds extraction error after at most η token insertions, deletions, or substitutions as 1 − Σ_{i=0}^{t} p_i^(n)(2η, 2η, c, d), where p_i^(n) is the probability that exactly i of the n segments are extracted incorrectly given per-segment allocated token counts c and green token counts d (Definition 4.1, Theorem 4.1, p. 209). “We provide our main theorem as follows” immediately precedes it (p. 209). The proof (Appendix A, pp. 217–218) assumes hash is a pseudo-random function (Assumption 1), shows each edit removes at most two and adds at most two previous-token/token pairs, and computes p_i^(n) by a recursion over segments using binomial and hypergeometric distributions. The robust bound B is the largest η whose bound is at most α; it is found by binary search (Definition 4.2, p. 209; Algorithm 4, Appendix B, p. 220). B is computed per generated paragraph from that paragraph’s c and d, not once for all texts.

Inference: a Verus version can specify a finite-field codec and prove decode(encode(K)) = K for the selected parameter range, then separately prove that the counting algorithm supplies the decoder’s input. The probabilistic edit bound remains a theorem about a stochastic model, not a direct functional postcondition.

evidence, assumptions, and limits

Experiments use OpenGen (3,000 two-sentence WikiText-103 chunks), C4 news, and Essays; default model LLaMA-2-7B, with Guanaco-7B and Falcon-7B; greedy decoding by default, with multinomial and nucleus sampling named for a decoding study (§5.1, p. 210). Defaults: δ = 6, T = 200 tokens, b = 20 bits, Rc = 0.6, Rr = 0.15, Reed–Solomon (6, 4, 1) over GF(2^5), α = 10^−3 (§5.1, p. 211). Match rate is the proportion of generated texts whose whole message is recovered; bit accuracy is the fraction of recovered bits (§5.1, p. 210). Reported results: match rate across datasets, models and bit lengths (Figure 3), robust bound (Figure 4), perplexity (Figures 5 and 7), a 25-participant user study (Table 4), baselines with extraction time (Table 2), Reed–Solomon parameters (Table 3), and six attacks, four of them set to change 10% of tokens (Figure 6, §5.3, p. 213). Example numbers: at 20 bits and 200 tokens, 97.6% match rate versus 49.2% for Yoo et al. (Table 2, p. 212); 90.0% versus 32.4% under copy-paste (p. 213); an average robust bound of 17 edits per paragraph (abstract, p. 201). The paper text does not state how many generated texts underlie each match rate. The text names a decoding-algorithm study but contains no decoding-algorithm results. The ROM analysis assumes hash(sk, ·) is a random oracle and bounds key-recovery advantage by Q/2^n (§4.4, p. 210).

Inference: the paper demonstrates an algorithmic proof bound and empirical robustness, but its assumptions include a pseudo-random hash, a token edit-distance metric, correct parameter selection, and an honest secret key. It does not establish semantic preservation of watermarked text, robustness to paraphrase beyond token edits (paraphrasing is measured only empirically, about 80% match rate, p. 213), or correctness of an LLM implementation; it excludes emoji attacks and manual rewriting from its threat model (p. 213). For VL, the reusable work is the explicit contracts, dynamic-programming invariants, finite-field codec proof, and a separate probabilistic model; redoing only the segment-counting idea would duplicate this result. Inference: threat to a product of agent-written verified Rust is medium: proofs can catch indexing, codec, and count-consistency bugs, while LLM behavior, hash security, and distributional claims remain trusted.

techniques for the catalog

• segment assignment watermark: pack bits into segments, map tokens by keyed previous-token hashing, bias a green list, and extract by candidate counting
• frequency-balanced mapping: use dynamic programming to split a key-shuffled vocabulary into consecutive groups with balanced natural frequencies
• Reed–Solomon protection: select an error-correcting code meeting rate and recovery constraints, then decode noisy segment values
• edit-distance robustness bound: compute segment error probabilities and binary-search the largest guaranteed edit budget Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “From the above analysis, we can see that it is very difficult to extract the secret key even by directly observing the hash outputs.”): checked every quotation, number, section and page reference, and technique step against the full paper text; changed the link to the publisher page printed in the paper, Algorithm 1–2 pages (208→209), Algorithm 3 and robust-bound locations, the dynamic-programming objective (was “largest deviation”, is sum of squared group sums over consecutive shuffled IDs), the theorem’s meaning of p_i^(n), the claimed decoding-effect plots (no such results in the text), and the Verus inference that wrongly implied deterministic no-edit recovery; added default parameters, key numbers, the proof’s pseudo-random-function assumption and per-paragraph bound; did not check the proof’s algebra, figure values read from plots, or the cited works.

Last edited: 2026-10-17