arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 2510.07331cs.AIcs.LO
收藏

Truth-Aware Decoding:一种面向事实性语言生成的程序逻辑方法

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

Lightcap;Bahcesehir University(巴赫切塞希尔大学)

Faruk Alpay, Hamdi Alakkad

AI总结:

本文提出Truth-Aware Decoding(TAD),一种基于程序逻辑的验证导向解码方案,通过语义守卫格约束生成过程,在保持吞吐量的同时减少幻觉,并提供了理论证明与Lean形式化验证。

摘要:

本文提出了Truth-Aware Decoding(TAD),一种面向验证的解码方案,旨在将神经语言生成与知识库对齐。该方法植根于序列模型的概率程序语义传统,通过一组在解码时运行的语义守卫格(lattice of semantic guards)来增强现代指令微调系统。我们的贡献有四点:(i)一种基于约束的语义,将预言机过滤(oracle filtering)呈现为程序逻辑判定;(ii)证明了在健全且完备的守卫下,贪心选择享有局部似然优势(定理2.7);(iii)一种熵风格不变量,通过知识感知的安全质量(knowledge-aware safe mass)量化事实风险;以及(iv)一种多智能体操作演算,附带经过验证的Lean工件以认证实现行为。数值与算法案例研究证实,所提出的护栏能在不牺牲吞吐量的情况下减少幻觉,为大规模经验模型与形式验证之间架起了一座实用桥梁。

英文摘要:

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.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑