Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Truth-Aware Decoding: A Program-Logic Approach to Factual Language Generation

Faruk Alpay, Hamdi Alakkad

TL;DR

Truth-Aware Decoding (TAD) introduces a runtime guard that couples large language models with knowledge-centric agents to constrain decoding to knowledge-consistent, oracle-approved tokens, thereby reducing hallucinations while maintaining throughput. The method is formalized with a semantic-language-model framework, a joint multi-agent verification dynamic, and rigorous guarantees on consistency and local likelihood dominance under soundness and completeness conditions. Empirical evaluation demonstrates substantial improvements in token-level truthfulness and calibrated risk via safe-mass metrics, alongside detailed performance analyses showing modest throughput overheads that can be mitigated with caching and engineering. This work provides a practical bridge between large-scale empirical language models and formal verification, enabling auditable, ethically guided, knowledge-bound generation in reasoning-intensive tasks.

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.

Truth-Aware Decoding: A Program-Logic Approach to Factual Language Generation

TL;DR

Truth-Aware Decoding (TAD) introduces a runtime guard that couples large language models with knowledge-centric agents to constrain decoding to knowledge-consistent, oracle-approved tokens, thereby reducing hallucinations while maintaining throughput. The method is formalized with a semantic-language-model framework, a joint multi-agent verification dynamic, and rigorous guarantees on consistency and local likelihood dominance under soundness and completeness conditions. Empirical evaluation demonstrates substantial improvements in token-level truthfulness and calibrated risk via safe-mass metrics, alongside detailed performance analyses showing modest throughput overheads that can be mitigated with caching and engineering. This work provides a practical bridge between large-scale empirical language models and formal verification, enabling auditable, ethically guided, knowledge-bound generation in reasoning-intensive tasks.

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.

Paper Structure

This paper contains 33 sections, 11 theorems, 22 equations, 1 table, 3 algorithms.

Table of Contents

  1. Introduction
  2. Semantic Agent Architecture
  3. Theoretical Framework
  4. Semantic Consistency as Constraint Satisfaction
  5. Main Results
  6. Decoding Procedures
  7. Computational Complexity of TAD
  8. Agent Specifications
  9. Multi-Agent Verification Dynamics
  10. Formal Agent Model
  11. Execution Semantics
  12. Analytical Foundations of Semantic Constraints
  13. Semantic Density and an Information Bound
  14. Limits and Responsible Evaluation
  15. Applications to Automated Reasoning
  16. ...and 18 more sections

Key Result

Lemma 2.4

Assume $\mathscr{O}$ is sound. If $x_{1:t-1}$ is knowledge-consistent and $w\in S_t$, then the concatenation $x_{1:t}=x_{1:t-1}\,\|\,w$ is knowledge-consistent.

Theorems & Definitions (30)

  • Definition 2.1: Semantic Language Model
  • Definition 2.2: Semantic Entropy
  • Definition 2.3: Knowledge-Consistent Prefix
  • Lemma 2.4: Safe Extension Invariance
  • proof
  • Theorem 2.5: Consistency Preservation
  • proof
  • Lemma 2.6: Stepwise Likelihood Superiority
  • proof
  • Theorem 2.7: Local Truthful Dominance
  • ...and 20 more