DHoTT: A Temporal Extension of Homotopy Type Theory for Semantic Drift
Fuente:
arXiv
Salvato in:
| Autore principale: | |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866917082521665536 |
|---|---|
| author | Poernomo, Iman |
| author_facet | Poernomo, Iman |
| contents | Dynamic HoTT (DHoTT) is a conservative extension of Homotopy Type Theory designed for evolving texts in conversational AI. In a chat system, a large language model (LLM) is queried with a growing prefix: at turn tau the input is C(tau), the concatenation of all previous prompts and replies, and the new answer extends C(tau+1). We study the logical semantics of these time indexed texts and how their meanings drift or break over time, linking Homotopy Type Theory with distributional semantics and topological data analysis on embedding spaces.
For each turn we embed all tokens seen so far using a frozen encoder and map them to the unit sphere, build a good cover by spherical caps, and form the Cech nerve. A Kan fibrant replacement yields a Kan complex ET(tau), the Evolving Text at time tau, where identity types are path spaces and dependent types support ordinary HoTT transport. Time is treated functorially so that all HoTT rules interpret fibrewise and standard substitution and conservativity properties hold.
On top of this fibrewise HoTT layer we add a small cross time calculus for semantic change. A carry records when a later use has a certified path back into an earlier fibre under an admissibility policy. A rupture is a positive sigma type storing finite, policy checked failed attempts together with an open horn tag. An append only ledger accumulates carries and ruptures so that earlier failures are not erased when later alignments appear.
We illustrate the construction on small, replicable examples from real human LLM dialogues using a concrete DeBERTa based embedding pipeline. This provides a principled, geometrically grounded core for analysing and auditing semantic drift in large language models and other embedding based systems. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_09671 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | DHoTT: A Temporal Extension of Homotopy Type Theory for Semantic Drift Poernomo, Iman Logic in Computer Science 03B70 F.4.1 Dynamic HoTT (DHoTT) is a conservative extension of Homotopy Type Theory designed for evolving texts in conversational AI. In a chat system, a large language model (LLM) is queried with a growing prefix: at turn tau the input is C(tau), the concatenation of all previous prompts and replies, and the new answer extends C(tau+1). We study the logical semantics of these time indexed texts and how their meanings drift or break over time, linking Homotopy Type Theory with distributional semantics and topological data analysis on embedding spaces. For each turn we embed all tokens seen so far using a frozen encoder and map them to the unit sphere, build a good cover by spherical caps, and form the Cech nerve. A Kan fibrant replacement yields a Kan complex ET(tau), the Evolving Text at time tau, where identity types are path spaces and dependent types support ordinary HoTT transport. Time is treated functorially so that all HoTT rules interpret fibrewise and standard substitution and conservativity properties hold. On top of this fibrewise HoTT layer we add a small cross time calculus for semantic change. A carry records when a later use has a certified path back into an earlier fibre under an admissibility policy. A rupture is a positive sigma type storing finite, policy checked failed attempts together with an open horn tag. An append only ledger accumulates carries and ruptures so that earlier failures are not erased when later alignments appear. We illustrate the construction on small, replicable examples from real human LLM dialogues using a concrete DeBERTa based embedding pipeline. This provides a principled, geometrically grounded core for analysing and auditing semantic drift in large language models and other embedding based systems. |
| title | DHoTT: A Temporal Extension of Homotopy Type Theory for Semantic Drift |
| topic | Logic in Computer Science 03B70 F.4.1 |
| url | https://arxiv.org/abs/2506.09671 |