Truth-Aware Decoding: A Program-Logic Approach to Factual Language Generation
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916997795676160 |
|---|---|
| author | Alpay, Faruk Alakkad, Hamdi |
| author_facet | Alpay, Faruk Alakkad, Hamdi |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_07331 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Truth-Aware Decoding: A Program-Logic Approach to Factual Language Generation Alpay, Faruk Alakkad, Hamdi Artificial Intelligence Logic in Computer Science 68N15, 68Q55, 68Q60, 03B35 D.3.1; F.3.1; F.3.2 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. |
| title | Truth-Aware Decoding: A Program-Logic Approach to Factual Language Generation |
| topic | Artificial Intelligence Logic in Computer Science 68N15, 68Q55, 68Q60, 03B35 D.3.1; F.3.1; F.3.2 |
| url | https://arxiv.org/abs/2510.07331 |