{"ID":2861175,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2510.07331","arxiv_id":"2510.07331","title":"Truth-Aware Decoding: A Program-Logic Approach to Factual Language Generation","abstract":"This paper introduces Truth-Aware Decoding (TAD), a verification-oriented decoding scheme that aligns neural language generation with knowledge bases. Situated in the tradition of probabilistic program semantics for sequence models, TAD augments modern instruction-tuned systems with a lattice of semantic guards that operate at decode time. Our contributions are fourfold: (i) a constraint-based semantics that renders oracle filtering as a program-logic judgment, (ii) a proof that greedy selection enjoys local likelihood dominance under sound and complete guards (Theorem 2.7), (iii) an entropy-style invariant that quantifies factual risk via knowledge-aware safe mass, and (iv) a multi-agent operational calculus with verified Lean artefacts to certify implementation behaviour. Numerical and algorithmic case studies confirm that the resulting guardrails reduce hallucinations without sacrificing throughput, yielding a pragmatic bridge between large-scale empirical models and formal verification.","short_abstract":"This paper introduces Truth-Aware Decoding (TAD), a verification-oriented decoding scheme that aligns neural language generation with knowledge bases. Situated in the tradition of probabilistic program semantics for sequence models, TAD augments modern instruction-tuned systems with a lattice of semantic guards that op...","url_abs":"https://arxiv.org/abs/2510.07331","url_pdf":"https://arxiv.org/pdf/2510.07331v1","authors":"[\"Faruk Alpay\",\"Hamdi Alakkad\"]","published":"2025-10-03T22:11:15Z","proceeding":"cs.AI","tasks":"[\"cs.AI\",\"cs.LO\"]","methods":"[]","has_code":false}