{"id":"8428af0c-ce2c-4aaf-bb41-560b2d285192","arxiv_id":"2509.06902","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":1,"one_line_summary":"Proof-Carrying Numbers binds each displayed LLM number to a structured claim and only marks it verified after a policy-based mechanical check, leaving all other numbers unverified.","lead":"This paper proposes a protocol called Proof-Carrying Numbers in which every number an LLM displays must be tagged with a claim identifier and mechanically checked against a structured data source before it can appear as verified. It argues that moving verification to the renderer, not the model, can turn numeric trust into a fail-closed contract.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Verified badge can attest to an irrelevant claim: PCN checks numeric consistency, not query relevance, so a distractor claim with a matching value passes verification.","rationale":"The reader's weakest_assumption correctly identifies the semantic gap between claim-consistency and query-relevance. I agree that the protocol's formal guarantees are definitionally sound but practically load-bearing on the LLM's claim-ID assignment and the retriever's claim set. The paper's own limitations section acknowledges dependence on LLM cooperation but does not isolate the specific failure mode where a Verified badge is attached to an irrelevant claim with a numerically matching value. A simple distractor test would quantify the practical impact and determine whether the overclaiming in the abstract requires correction. Since my analysis aligns with the reader's conditional verdict, I recommend no change to the verdict.","tokens_in":11386,"tokens_out":6130,"duration_ms":69414,"concrete_test":"Build a 'distractor benchmark' of queries such as 'What was the GDP growth of the Philippines in 2024?' and populate C with both the correct claim (PHL, 2024, 5.7%) and a distractor claim (VNM, 2024, 5.7%) with an identical numeric value. Run a PCN-compliant pipeline (retriever + LLM + verifier) on at least 100 such queries and measure: (a) how often the LLM emits any claim-bound token, and (b) how often the token's claim ID points to the correct claim versus a distractor. If the wrong-claim rate is non-negligible (e.g., >5%), then a Verified mark can be attached to a number that does not answer the query, directly invalidating the 'trustworthy numeric answers' framing. Report precision and recall of claim-ID binding separately.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's central guarantee is that a Verified mark is only displayed when the renderer matches the surfaced number to a structured claim under a declared policy (Theorem 5.1). This is true by construction but trusts the LLM's choice of claim ID. The verifier has no access to the user query q; the relation R(t,c;Π) compares only the token's numeric payload to the claim's reference value. Therefore, if the LLM emits a claim-bound token referencing a claim that is numerically consistent but semantically unrelated to q (e.g., same GDP growth value for the wrong country or year), the renderer labels it Verified. This is not a violation of the formal problem statement (Section 3.6), which only requires existence of some c∈C, but it undercuts the abstract promise of 'trustworthy numeric answers.' Section 6.3 mentions 'Identifier abuse' and 'Overconfidence in scope' but does not flag that claim-ID semantic correctness is an unverified assumption on which the practical value rests. Without it, a hallucinated number can carry the Verified badge whenever it coincides with any claim in C, making the mark a guarantee of consistency with some source, not correctness relative to the question.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes Proof-Carrying Numbers (PCN), a presentation-layer protocol intended to prevent numeric hallucination in LLM outputs. PCN requires numeric spans to be emitted as claim-bound tokens referencing structured claims; a renderer-side verifier checks each token against the referenced claim under a configurable policy (exact, rounding, alias, tolerance with qualifiers) and labels it Verified or Unverified. The authors formalize the protocol, state soundness, completeness, fail-closed, monotonicity, and renderer-robustness properties, and provide a TypeScript implementation sketch in the appendix. The central design idea is that verification status is computed by the renderer, not by the model, so fabricated numbers cannot display a verified badge unless they match a claim in the available claim set.","tokens_in":11717,"tokens_out":4486,"duration_ms":52231,"significance":"If the practical assumptions are met, PCN would provide a clean, testable contract for numeric claims in LLM interfaces: verified numbers are always traceable to a structured claim, and unverified numbers are visibly unmarked. The separation of verification from generation is a useful contribution and the policy layer is a sensible way to express application-specific tolerance. The appendix gives a concrete, executable implementation sketch, which strengthens reproducibility. However, the formal guarantees are largely definitional, and the protocol's practical value depends on two unverified assumptions: that LLMs can reliably emit claim-bound tokens with correct claim IDs, and that numeric consistency with some claim implies relevance to the user's query. The paper's advertised user contract ('trustworthy numeric answers') is stronger than the formal problem statement, which only ensures existence of some matching claim in C.","major_comments":[{"comment":"The central soundness guarantee is weaker than the paper's advertised contract. The acceptance function A labels a token as Verified iff there exists some c∈C with R(t,c;Π)=1; the verifier does not access the user query q and cannot check that c is the claim that answers q. Consequently, a numerically incorrect answer can receive a Verified badge if its value coincides with any distractor claim in C (e.g., a different country or year). Section 6.1 correctly limits the claim to 'verifiably consistent with a claim under a policy Π', but the abstract and §4.4's user contract promise 'trustworthy numeric answers' and treat the badge as a fidelity guarantee. Section 6.3 mentions 'Identifier abuse' only indirectly and does not flag that claim-ID semantic correctness is a load-bearing unverified assumption. The paper should either consistently restate the guarantee as 'consistency with some cla","section":"§3.6, §5.1, §4.4"},{"comment":"The protocol's practical value rests on the LLM's ability to emit claim-bound tokens with correct claim IDs and values at high recall. The paper states in §6.4 that 'Early experiments suggest that prompting or light fine-tuning enables models to emit claim tags with reasonable recall' and in §6.6 that effectiveness 'hinges on LLM cooperation', but no experimental data, dataset, or measurement are provided. Without any evaluation of token-emission compliance and claim-ID correctness, the feasibility claims in the abstract and §4.2 are unsupported. This is a major gap for a cs.CL paper; even a small-scale study measuring compliance rates and error types would substantially strengthen the contribution.","section":"§6.4, §6.6"},{"comment":"Theorems 5.1–5.4 are definitional rather than substantive. Because A is defined to label a token Verified iff R(t,c;Π)=1 for some c, each proof sketch simply unpacks the definition of A. These results do not establish that verified numbers are correct with respect to the query or that the underlying claims are trustworthy; they only restate the protocol's specification. The section would be more honest if reframed as a formal specification with invariants, with the substantive arguments focused on policy monotonicity, renderer robustness, and the practical properties that require reasoning beyond definitions (e.g., the relationship between token syntax and the renderer's parsing behavior).","section":"§5.1–§5.4"}],"minor_comments":[{"comment":"Lemma 5.4 is called 'Theorem 5.4' in §6.2. Please make the numbering and theorem/lemma labels consistent.","section":"§5.1, §6.2"},{"comment":"The normalization step is under-specified ('normalized into the claim's unit'), and the sample implementation strips only spaces and commas, not '%' or other units. This makes the exact-policy example in §A.1 depend on a formatting coincidence. Please specify normalization precisely and align the code with the formal definition.","section":"§3.4, §A.1"},{"comment":"The definitions of round_d, round0, and the alias set S are informal. For example, does rounding operate on the displayed string or the underlying float, and how are negative values handled? A compact formal definition would remove ambiguity.","section":"§3.4"},{"comment":"The figures are referenced but not described in the main text; their captions should state what behavior they illustrate (e.g., a verified badge vs. a pending/warning mark) so the reader can interpret them without guessing.","section":"Figures 2 and 3"}],"recommendation":"major_revision","confidential_remarks":"The paper is a protocol proposal rather than an empirical study. Its formal core is a specification, not deep theory, and the proofs are mostly definitional. The main risk is that the user-facing promise exceeds the formal guarantee: a Verified badge only indicates consistency with some claim, not relevance to the query. The absence of any LLM-compliance experiment is also a significant gap for a cs.CL submission. I believe the ideas are worthwhile and the protocol could be revised into a solid contribution, but the current claims need to be scaled back or accompanied by evidence."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"PCN is a neat, well-specified protocol: instead of trusting the LLM to output correct numbers, it moves verification to the renderer. Any displayed number must be emitted as a claim-bound token, and the renderer only marks it 'Verified' if it matches a structured claim under a declared policy. This design is genuinely novel as a combination—claim schema, policy modes (exact, rounding, alias, tolerance), and fail-closed default-unverified semantics—and it is clearly written and easy to follow. The formal properties are correct: Soundness, Fail-Closed, and Monotonicity are true by construction of the acceptance function, and the proofs unpack definitions properly. The Appendix's TypeScript implementation is a real, reproducible artifact.\n\nThe main weakness is not the math but the scope of the promise. The abstract says PCN 'guarantees numeric fidelity' and 'trustworthy numeric answers.' What it actually guarantees is that a verified number is numerically consistent with some claim in the claim set, assuming the LLM picked the right claim ID. The verifier never sees the user query; it only compares surface value to the referenced claim's value. So a model that binds the Philippines' 2024 GDP growth to the claim for, say, Vietnam's 2023 figure with the same rounded value will receive a Verified badge. Section 6.3 mentions 'Identifier abuse' but does not flag that claim-ID semantic correctness is a load-bearing assumption on which the practical value rests. That deserves explicit treatment.\n\nThe paper also provides no empirical evidence on the critical step: can LLMs reliably emit claim-bound tokens with correct IDs under prompt or light fine-tuning? The authors say 'early experiments suggest' but give no numbers. A small benchmark with two or three models and a handful of policies would substantially move the needle.\n\nThese are fixable issues. The protocol idea is sound and the presentation is honest about several limitations in Section 6.1 and 6.6. It deserves serious refereeing: the contribution is real, the formalization is clean, and the engineering is reproducible. I'd send it to peer review with a request for (1) an explicit statement that verification is relative to the chosen claim, not the query, (2) a tag-compliance experiment, and (3) toning down the abstract. I'd also be happy to cite it as a protocol proposal in the LLM-trust space, provided the authors address the claim-selection caveat.","headline":"PCN is a clean, honest protocol for renderer-side numeric verification, but its headline guarantee only holds conditional on the LLM citing the right claim—something the paper acknowledges obliquely and never tests.","tokens_in":12144,"tokens_out":2676,"would_cite":true,"duration_ms":29556,"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":"This paper proposes Proof-Carrying Numbers (PCN), a protocol in which every number an LLM displays is either mechanically verified against a structured claim under a declared policy or explicitly shown as unverified.","keywords":["proof-carrying numbers","numeric hallucination","claim verification","fail-closed protocol","LLM trust","provenance","verification policy","renderer-side verification"],"falsifier":"Run an end-to-end PCN system where the model answers a question about one indicator but binds the number to a claim for a different indicator with the same value. If the renderer displays the Verified badge, the protocol's guarantee as stated—that verified means honestly sourced—fails. The same test with a claim whose value matches only after an overly permissive tolerance policy would also show where the policy boundary must be tightened.","tokens_in":11319,"feed_emoji":"✅","tokens_out":5892,"duration_ms":54500,"temperature":0.7,"pith_summary":"The paper argues that numeric hallucination in LLMs is best fixed not by making the model more truthful but by controlling what the interface is permitted to mark as verified. It proposes Proof-Carrying Numbers (PCN), a presentation-layer protocol in which every numeric span is emitted either as a claim-bound token tied to a structured claim or as a bare number. A verifier running in the renderer applies a declared policy—exact match, rounding, alias equivalence, or tolerance with qualifiers—and marks a number as verified only when it deterministically matches a claim. If this works as described, users can treat a verified badge as proof of correspondence to an authoritative source, while the absence of a mark honestly signals uncertainty.","feed_headline":"LLM numbers get a verified badge only after a claim check","feed_subtitle":"A renderer-side protocol rejects unproven digits by default, so a verified mark means a source was matched mechanically.","key_machinery":"The central object is the claim-bound token: a numeric span wrapped as <claim id=\"CID\" policy=\"P\">VAL</claim>. It links a surface number to a structured claim c = ⟨claim id, indicator, entity, time, v*, u, m⟩. The verifier's relation R(t,c; Π) then decides acceptance using policy modes (exact, rounded, alias, tolerance with qualifiers). Because the renderer computes R, verification cannot be influenced by the model's text, which is what makes the fail-closed contract hold.","core_discovery":"PCN frames numeric hallucination as a presentation-layer problem: even when correct values are retrievable, the model may reproduce them incorrectly and the UI has no way to tell. The protocol requires values to appear as <claim id=\"CID\" policy=\"P\">VAL</claim> tokens, binds each token to a claim in the resolved claim set, and defines a verification relation that holds when the normalized value matches under the active policy. Verified status is computed by the renderer, not the model, so text like \"verified\" or checkmark symbols cannot spoof it; numbers without a valid claim reference are always unverified. The paper proves soundness, completeness under honest tokens, fail-closed behavior, m","pith_inferences":["The load-bearing step is the model's choice of which claim ID to attach; the verifier checks numeric consistency only. A model could bind a plausible number to an irrelevant but numerically matching claim, and the renderer would mark it Verified. A robust design should verify claim relevance to the query, not just value equality.","The protocol could be extended to derived numbers (ratios, aggregates) by verifying deterministic functions over atomic claims; the paper lists this as future work, but the same renderer-side contract would then need to check the derivation, not just the final span.","User trust depends on whether people understand that an unmarked number is merely unverified, not necessarily wrong; controlled studies of badge interpretation would tell whether the interface actually changes behavior.","Adoption incentives may be the real bottleneck: data custodians become trust anchors and may hesitate to publish canonical claims without governance frameworks; this is a deployment condition, not a protocol flaw."],"forward_implications":["A verified badge becomes a binding statement: the displayed number equals, rounds to, aliases, or tolerates to a value in a claim the system retrieved.","Any number without a claim tag is displayed unverified by default, so fabricated values cannot appear as fact even if the surrounding text looks fluent.","Policy presets let applications trade strictness for coverage predictably: tightening a policy only removes verified marks, never adds false ones.","Verification adds negligible latency—O(n) over numeric spans—so it can ride on existing RAG and chat pipelines.","With signatures or Merkle proofs, the same contract can certify that the claim itself has not been tampered with."],"supporting_citations":[{"why":"Supplies the proof-carrying idea that verification can be checked mechanically from the artifact itself, which PCN adapts from code to displayed numbers.","marker":"Necula, 1997"},{"why":"Defines retrieval-augmented generation, the baseline that improves grounding but cannot guarantee that a displayed number is faithful to the retrieved source.","marker":"Lewis et al., 2020"},{"why":"Documents an LLM 'correcting' a perturbed dosage to a different value, illustrating the numerically risky behavior PCN is designed to contain.","marker":"Wu et al., 2025a"},{"why":"Introduces symbolic references interleaved with generated text, the closest prior mechanism that stops short of guaranteed fidelity.","marker":"Hennigen et al., 2024"},{"why":"Supplies the running example's authoritative claim (Philippines 2024 GDP growth, 5.7%) used to illustrate verification.","marker":"The World Bank, 2025"},{"why":"Provides the FEVER claim-verification paradigm, which PCN contrasts as retrospective rather than enforced at display time.","marker":"Thorne et al., 2018"}],"fun_headline_variants":["Renderers verify LLM numbers, not the model","LLM digits: only proof earns the verified mark","Trustworthy numbers: claim-checked at display time","PCN: numeric answers get verified only if proven","No proof, no badge: renderer enforces LLM number trust"],"cache_read_input_tokens":2688,"weakest_assumption_plain":"The model must attach each number to the claim that actually answers the user's question; the verifier only checks that the number matches the cited claim's value, not that the claim is the right one.","fun_headline_variants_meta":{"raw":{"variants":["Renderers verify LLM numbers, not the model","LLM digits: only proof earns the verified mark","Trustworthy numbers: claim-checked at display time","PCN: numeric answers get verified only if proven","No proof, no badge: renderer enforces LLM number trust"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00016,"raw_usage":{"total_tokens":1099,"prompt_tokens":802,"completion_tokens":297,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":546,"completion_tokens_details":{"reasoning_tokens":217}},"tokens_in":546,"tokens_out":297,"duration_ms":3135,"temperature":1.0,"reasoning_tokens":217,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-04T22:50:57.886212+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run an end-to-end PCN system where the model answers a question about one indicator but binds the number to a claim for a different indicator with the same value. If the renderer displays the Verified badge, the protocol's guarantee as stated—that verified means honestly sourced—fails. The same test with a claim whose value matches only after an overly permissive tolerance policy would also show where the policy boundary must be tightened.","supporting_citations":[{"cited_title":"Retrieval-augmented generation for knowledge-intensive NLP tasks","cited_arxiv_id":null,"evidence_quote":"Defines retrieval-augmented generation, the baseline that improves grounding but cannot guarantee that a displayed number is faithful to the retrieved source."},{"cited_title":"Towards Verifiable Text Generation with Symbolic References","cited_arxiv_id":null,"evidence_quote":"Introduces symbolic references interleaved with generated text, the closest prior mechanism that stops short of guaranteed fidelity."},{"cited_title":"World Bank Open Data - World Development Indicators ( WDI ), 2025","cited_arxiv_id":null,"evidence_quote":"Supplies the running example's authoritative claim (Philippines 2024 GDP growth, 5.7%) used to illustrate verification."}],"review_version":1}