中文

DHoTT:用于语义漂移的同伦类型论时间扩展

计算机科学中的逻辑 2025-11-18 v3

摘要

动态同伦类型论(DHoTT)是同伦类型论的一个保守扩展,专为对话人工智能中演化的文本而设计。在聊天系统中,大语言模型(LLM)接收一个不断增长的前缀进行查询:在第 τ\tau 轮,输入为 C(τ)C(\tau),即所有先前提示和回复的拼接,新的回答扩展了 C(τ+1)C(\tau+1)。我们研究这些时间索引文本的逻辑语义,以及它们的含义如何随时间漂移或断裂,将同伦类型论与分布语义学和嵌入空间上的拓扑数据分析联系起来。对于每一轮,我们使用冻结的编码器将所有已见 token 嵌入,并将它们映射到单位球面,通过球冠构建好覆盖,并构造 Cech 神经。Kan 纤维化替换得到一个 Kan 复形 ET(τ)ET(\tau),即时间 τ\tau 处的演化文本,其中恒等类型是路径空间,依赖类型支持普通的 HoTT 传输。时间被函式地处理,使得所有 HoTT 规则逐纤维地解释,且标准的替换和保守性性质成立。在这个逐纤维的 HoTT 层之上,我们添加了一个用于语义变化的小型跨时间演算。carry 记录在可接受性策略下,后续使用何时具有回到先前纤维的认证路径。rupture 是一个正的 sigma 类型,存储有限的、经过策略检查的失败尝试以及一个开口角标签。一个仅追加的账本累积 carry 和 rupture,使得当后续对齐出现时,之前的失败不会被擦除。我们在来自真实人类 LLM 对话的小型、可复现示例上,使用一个基于 DeBERTa 的具体嵌入管道说明了该构造。这为分析和审计大语言模型和其他基于嵌入的系统中的语义漂移提供了一个原则性的、几何基础的核心。

关键词

引用

@article{arxiv.2506.09671,
  title  = {DHoTT: A Temporal Extension of Homotopy Type Theory for Semantic Drift},
  author = {Iman Poernomo},
  journal= {arXiv preprint arXiv:2506.09671},
  year   = {2025}
}