MAZE.AI: De Toekomst van Betrouwbare Kunstmatige Intelligentie

On By konstapelIn Uncategorized

Bezoek Maze.AI hier.

J.Konstapel,Leiden, 20-9-2026

Inleiding

Kunstmatige intelligentie (KI) heeft de afgelopen jaren een ongekende vlucht genomen. Large Language Models (LLMs) zoals die van OpenAI, Google en Mistral AI kunnen teksten genereren die bijna niet van menselijk werk te onderscheiden zijn. Toch blijft er een fundamenteel probleem: hoe weten we of de informatie die deze modellen produceren betrouwbaar is? In een tijdperk waarin desinformatie en deepfakes de ronde doen, is vertrouwen in KI-systemen essentieel. De traditionele benadering — het proberen te bewijzen dat een model altijd de waarheid spreekt — is echter onhaalbaar. De wiskundige logicus Alfred Tarski toonde al in 1936 aan dat voor een voldoende rijke taal (zoals natuurlijke taal) een totale, certificeerbare waarheidspredikaat onmogelijk is.

Hier komt MAZE.AI om de hoek kijken, een systeem ontwikkeld door J. Konstapel in Leiden. MAZE.AI stelt niet dat het alle antwoorden weet, maar wel dat elke bewering die het doet, herleidbaar en verifieerbaar is. Dit whitepaper-essay verkent hoe MAZE.AI dit bereikt, welke theoretische en technische innovaties het introduceert, en wat de implicaties zijn voor de toekomst van betrouwbare KI.

Het Probleem: Ongebonden Beweringen

De Illusie van Betrouwbaarheid

Large Language Models produceren vloeiende teksten die vaak klinken alsof ze op feiten zijn gebaseerd. Toch is er een cruciaal verschil tussen een zin die iets rapporteert (bijvoorbeeld: “De hoofdstad van Frankrijk is Parijs”) en een zin die iets voortzet (bijvoorbeeld: “De hoofdstad van Frankrijk is een prachtige stad”). Een LLM maakt dit onderscheid niet. Het genereert gewoon de meest waarschijnlijke volgende woorden, zonder garantie dat de informatie correct is.

Retrieval-Augmented Generation (RAG) probeert dit probleem aan te pakken door modellen toegang te geven tot externe kennisbronnen. Het model kan dan citaten toevoegen aan zijn antwoorden. Toch blijft het probleem bestaan: het model kiest zelf welke citaten het gebruikt en hoe het deze interpreteert. Voor een lezer is het onmogelijk om te weten welke delen van het antwoord daadwerkelijk afkomstig zijn uit de bronnen en welke delen door het model zijn “verzonnen”.

Theoretische Beperkingen

Het idee om een KI-model “correct” te bewijzen — dat wil zeggen, om te bewijzen dat het altijd de waarheid spreekt — stuit op fundamentele wiskundige beperkingen. Tarski’s ondefinieerbaarheidstheorema toont aan dat voor een taal die rijk genoeg is (zoals natuurlijke taal), een totale waarheidspredikaat niet kan worden gedefinieerd. Dit betekent dat we niet kunnen bewijzen dat een model altijd de waarheid spreekt, omdat “waarheid” zelf niet op een totale, certificeerbare manier kan worden gedefinieerd.

Dit inzicht dwingt ons om op zoek te gaan naar een haalbaarder criterium voor betrouwbaarheid.

Het Criterium: Bewijsbare Herleidbaarheid

Van Waarheid naar Herleidbaarheid

MAZE.AI stelt voor om niet te streven naar het bewijzen van de waarheid van een bewering, maar naar het bewijzen van de herleidbaarheid (provenance) ervan. Dit betekent dat elke output van het systeem moet kunnen worden herleid tot een specifieke, gecertificeerde bron. Concreet houdt dit in:

  1. Gecertificeerde Opslag (Store): Een verzameling van (adres, inhoud)-paren waar lidmaatschap beslisbaar is. Dit betekent dat we voor elk adres kunnen controleren of het al dan niet in de opslag aanwezig is.
  2. Outputtypes: MAZE.AI kent slechts vier soorten output, elk met een adres:
    • Afgeleid (Derived): De inhoud staat op het opgegeven adres in de opslag.
    • Geattesteerd (Attested): Een entry in de grootboekledger (ledger) bevestigt dat dit adres voor deze canonieke vraag is bevestigd door een persoon, op een bepaalde datum.
    • Vacature (Vacancy): Het adres is leeg; er is geen inhoud beschikbaar.
    • Voorstel (Proposal): Voorgesteld door een taalmodel, maar verlaat het systeem alleen als afgeleid of vacature.

Scheiding van Verantwoordelijkheden

MAZE.AI maakt een duidelijke scheiding tussen de rol van de machine en die van de mens:

  • Machine: Bewijst de herleidbaarheid (dat een bepaalde inhoud op een bepaald adres staat).
  • Mens: Bepaalt of een adres daadwerkelijk een vraag beantwoordt (via de ledger).

Deze scheiding zorgt ervoor dat geen van beide partijen het werk van de andere overneemt. De machine bewijst niet de betekenis van een antwoord, en de mens hoeft niet te controleren of de inhoud daadwerkelijk op het adres staat.

De Technische Constructie van MAZE.AI

De Vijf Kerncomponenten

MAZE.AI bestaat uit vijf kleine, maar krachtige componenten die samen een betrouwbaar systeem vormen:

1. De Kernel: Adresberekening in Balanced Ternary

Adressen in MAZE.AI zijn lijsten van trits (driewaardegetallen: -1, 0, +1) in balanced ternary. De kernel zorgt voor een bijection (één-op-één correspondentie) tussen adressen van diepte n en integerwaarden in het bereik [- (3^n - 1)/2, (3^n - 1)/2]. Dit betekent dat elk adres uniek is en dat truncatie (het inkorten van een adres) idempotent (herhaalbaar zonder effect) en prefix-stabiel is.

  • Voordelen: Balanced ternary geeft adressen een metrische structuur. Een prefix van een adres kan worden gezien als een grovere klasse, wat het mogelijk maakt om te zoeken in hiërarchische structuren.
  • Bewijs: In Lean zijn theorema’s als waarde_bereik (de absolute waarde van een adres ligt binnen een bepaald bereik) en waarde_inj (gelijke diepte en waarde impliceren gelijk adres) bewezen.

2. De Store: Opslag van Inhoud

De productie-opslag is een PostgreSQL-database die (adres, inhoud, ontvangstbewijs)-paren bevat. Voor de theoretische validatie zijn er twee Lean-modellen:

  • Een lijst van paren (adres, inhoud).
  • Een finite map (een lijst met een bewijs dat elk adres hooguit één inhoud draagt).
  • Invariant: Een adres wordt nooit herschreven na toelating tot de store. Dit wordt bewezen in Winkel.lean met theorema’s als Winkel.voeg_bewoond (invoegen op een bewoond adres verandert niets).

3. De Loop: Antwoordgeneratie

De loop is het hart van MAZE.AI. Het is één functie met één outputtype (met vier constructoren). De werking is als volgt:

  1. Ledger check: Eerst wordt de ledger gecontroleerd op een settlement voor de canonieke vraag. Als er een match is en de inhoud nog in de store staat, wordt geattesteerd geretourneerd.
  2. Store check: Als er geen match in de ledger is, wordt de store gecontroleerd op het berekende adres. Als er inhoud is, wordt afgeleid geretourneerd; als het adres leeg is, wordt vacature geretourneerd.
  3. Taalmodel: Een taalmodel kan een voorstel doen (bijvoorbeeld een formulering met citaten), maar dit verlaat de loop alleen als afgeleid of vacature.
  • Bewijs: In Lus.lean zijn theorema’s als lus_afgeleid_store (als de output afgeleid is, dan staat de inhoud in de store) bewezen.

4. De Verifier: Onafhankelijke Validatie

De verifier is een afzonderlijke module die elke output controleert voordat deze wordt uitgezonden. Het vertrouwt de loop niet blindelings: het herleest de store en de ledger en checkt de invarianten op de output. Als de invarianten niet kloppen, weigert de verifier de output (geen stille correctie).

  • Belang: Dit zorgt voor een extra laag van vertrouwen, omdat de output alleen wordt geaccepteerd als deze voldoet aan de bewijsbare voorwaarden.

5. De Ledger: Auditlog van Settlements

De ledger is een append-only (alleen toevoegen, geen wijzigingen) grootboek met hash-gechainde en gesigneerde entries. Elke entry bevat:

  • Canonieke versie van de vraag.
  • Materiaal-ID.
  • Adres.
  • Wie de settlement heeft goedgekeurd.
  • Datum.
  • Vorige hash, hash, handtekening, en key fingerprint.
  • Hash-chain: Elke entry’s hash is een SHA-256 hash van de vorige hash en de velden van de huidige entry. Dit zorgt voor onveranderlijkheid: als een entry wordt gewijzigd, verandert de hele keten.
  • Handtekening: Elke entry is gesigneerd met een HMAC (Hash-based Message Authentication Code) met de sleutel die de settlement heeft goedgekeurd.
  • Bewijs: In Keten.lean zijn theorema’s als chain_deterministic (de keten is deterministisch) en chain_last_changes (wijziging van de laatste entry verandert de finale hash) bewezen.

Het MAZE Net: Een Zelf-Adresserend Kennisnetwerk

Structuur en Omvang

MAZE.AI draait op het MAZE Net, een zelf-adresserend ternair kennisnetwerk van 8,19 miljoen stukken, waaronder:

  • Wikipedia-artikelen.
  • Mathlib-theorema’s.
  • EPO-patenten.
  • Kunst en muziek.
  • Open vragen.

Elk stuk in het netwerk heeft een adres dat is berekend uit de inhoud (content-addressable). Dit betekent dat de inhoud zelf het adres bepaalt, wat zorgt voor uniciteit en consistentie.

Adresberekening en Zoeken

  • Adresberekening: Voor een gegeven vraag wordt een 24-trit adres berekend via embedding. Vervolgens wordt gezocht naar het diepste bewoonde prefix (minimaal diepte 6) en wordt binnen die buurt een cosine ranking toegepast.
  • Naam-brug: Voor exacte namen (bijvoorbeeld een vraag die de naam is van een inwoner van het net) wordt de vraag direct opgelost via identiteit.
  • Canonisatie: Vragen worden gecanoniseerd (gestandaardiseerd) via canon(q):
    • NFKC-normalisatie.
    • Lowercase.
    • Alleen letters, cijfers, en spaties.
    • Enkelvoudige spaties.
    • Afkappen op 400 karakters.

Semantische Gap

Een belangrijk concept in MAZE.AI is de semantische gap tussen:

  • “Gevonden op een image van het adres”: De inhoud staat op een prefix van het berekende adres.
  • “Gevonden op het adres”: De inhoud staat exact op het berekende adres.

De verifier checkt beide gevallen:

  1. Store-lidmaatschap: Staat de inhoud in de store?
  2. Adres-provenance: Is de inhoud gekoppeld aan het adres (of een prefix daarvan)?
  • Zwakke vlag: Als de top-inwoner (de inhoud op het diepste bewoonde prefix) een cosine-similariteit < 0,32 heeft met de vraag, wordt deze gemarkeerd als “zwak”. Dit is een vroege waarschuwing voor mogelijke onnauwkeurigheden.

Theorema’s en Binding aan Productiecode

Bewijzen in Lean 4

Alle theorema’s in MAZE.AI zijn machine-gecheckt met Lean 4.34, zonder additionele axioma’s (behalve propext, Classical.choice, en Quot.sound). Enkele belangrijke theorema’s:

CategorieTheoremaBetekenis
Kernelwaarde_bereikDe absolute waarde van een adres ligt binnen (3^|a| - 1)/2.
Kernelwaarde_injGelijke diepte en waarde impliceren gelijk adres.
Kerneltrunc_idemTruncatie is idempotent (herhaalbaar zonder effect).
Loop (Lijst-Store)lus_afgeleid_storeAls de output afgeleid is, dan staat de inhoud in de store.
Loop (Lijst-Store)lus_vacature_leegAls de output vacature is, dan is het adres leeg in de store.
Loop (Lijst-Store)lus_geattesteerd_grootboekAls de output geattesteerd is, dan matcht de ledger-entry het adres, de inhoud, de persoon, en de datum.
Loop (Finite-Map-Store)antwoordW_iffDe loop emit exact wat de store bevat (equivalentie).
Ledgerchain_deterministicDe keten is deterministisch.
Ledgerchain_last_changesWijziging van de laatste entry verandert de finale hash.

Binding aan Productiecode

Om ervoor te zorgen dat de bewijzen ook gelden voor de daadwerkelijke productiecode, gebruikt MAZE.AI drie bindingmechanismen:

  1. Differentiële Kerntest:
    • De Lean-kernel en de JavaScript-kernel produceren 30.572 adressen (dieptes 12 en 42).
    • Een diff toont 0 verschillen tussen de output van beide kernels.
  2. Productie-Pad Test:
    • De echte loop draait op de echte store voor een vaste lijst van vragen.
    • Elke output gaat door de verifier, die de store en ledger herleest.
    • Rode fouten: Als de invarianten niet kloppen, wordt de output geweigerd.
  3. Controlecommando: node maze/ai/controle.mjs Dit commando:
    • Rebuildt het Lean-project.
    • Print een axiom-rapport (alleen de drie standaard axioma’s zijn toegestaan).
    • Voert de differentiële test en canon-determinisme test uit.
    • Voert (met een database) de productie-pad test uit.
    • Stopt bij de eerste rode stap.

Metingen en Validatie

De 20-Vragen Placement Test

Om de prestaties van MAZE.AI te meten, is een 20-vragen placement test uitgevoerd:

  • Opzet: 20 open vragen in het Nederlands en Engels, met vooraf gedefinieerde verwachte inwoners van het MAZE Net.
  • Plan Hash: sha256 8bc2f1fe... (vooraf vastgelegd).
  • Drempel: ≥14/20.

Resultaat: 15/20 (2 zwak, 5 misses).

Analyse van de Misses

  1. Naam-brug: Te algemene lemma’s:
    • “Lithium” in plaats van “lithium-ion batterij”.
    • “Theory” in plaats van “MOND” (Modified Newtonian Dynamics).
  2. Niet-lemma namen:
    • “Sardex” en “Grokking” werden teruggegeven als verre buren (zwakke match).
    • Eerlijke output: Had een vacature moeten zijn.
  • Zwakke vlag: Ving 4 van de 5 misses.
  • Latentie: 2–11 seconden per vraag (gedomineerd door externe lookups in de naam-brug).

Archive-Level Union Test

  • MAZE Net: 4,08 miljoen unieke adressen.
  • Overlap: 0,06% gedeeld door twee onafhankelijke bronnen.

Claims en Niet-Claims

Wat MAZE.AI Claimt

✅ Elke output van de loop:

  • Is 1 van 4 types (afgeleid, geattesteerd, vacature, voorstel).
  • Draagt een adres.
  • Voldoet aan een bewijsbare uitspraak over de store.

✅ Proposal verlaat de loop nooit als assertie (alleen als afgeleid of vacature).

✅ Settlement is een auditeerbaar event (via de ledger).

✅ Bewijzen zijn gebonden aan de code via differentiële en productie-pad tests.

✅ Novelty: MAZE.AI combineert:

  • Proof assistant (Lean).
  • Retrieval met citaten.
  • Transparency logs.
  • Human-in-the-loop review.
  • Één outputpad met claim-complete types + machine-gecheckte invarianten.

Wat MAZE.AI Niet Claimt

❌ Antwoorden zijn waar (alleen provenance is gecertificeerd).
❌ Placement is betrouwbaar (15/20 is een eerste meting, geen garantie).
❌ Ledger is onvergetelijk (HMAC-handtekeningen met toelatings-sleutel; geen persoonlijke sleutels per mens).
❌ SHA-256 is collision-vrij (aangenomen, maar niet bewezen).

Relatie met Bestaand Werk

MAZE.AI bouwt voort op verschillende bestaande concepten en systemen, maar combineert deze op een unieke manier:

WerkRelatieVerschil
Tarski (1936)Theoretische onderbouwingOnmogelijkheid van totale waarheidspredikaat → motivatie voor criterium P.
seL4 (Klein et al., 2009)Methodologische inspiratieBewijzen van een draaiend systeem tegen specificaties. Verschil: MAZE.AI bewijst een kleine loop + kernel, niet een compiler.
CompCert (Leroy, 2009)Binding bewijs → codeExtractie vs. differentiële testing. MAZE.AI gebruikt differentiële tests (Lean vs. JavaScript).
Certificate Transparency (Laurie, 2014)Ledger-ontwerpAppend-only, hash-gechaind, publiek controleerbaar. Verschil: Ledger entries zijn feiten over events, niet oordelen.
RAG (Lewis et al., 2020)Retrieval + generatieMAZE.AI verandert de outputtype: retrieved content is de output, niet de generatie.
WebGPT (Nakano et al., 2021)Citaten door modelMAZE.AI: citaten zijn machine-gecheckt (provenance).
Lean 4 (de Moura & Ullrich, 2021)BewijstoolStatement = program. Gebruikt voor alle theorema’s in §4.
Knuth (1997)Balanced ternaryArithmetica van de adres-kernel.

Discussie: Sterke Punten en Beperkingen

Sterke Punten

✔ Theoretische Fundering: Criterium P is een haalbare, certificeerbare oplossing voor het ondefinieerbaarheidsprobleem van Tarski. Het systeem is niet afhankelijk van een onmogelijke totale waarheidspredikaat, maar van herleidbaarheid, wat wel certificeerbaar is.

✔ Transparantie: De ledger is append-only, hash-gechaind, en publiek controleerbaar. Dit zorgt voor een audit trail die niet kan worden gemanipuleerd zonder detectie.

✔ Scheiding van Verantwoordelijkheden: De machine (provenance) en de mens (betekenis) hebben duidelijke, gescheiden rollen. Dit voorkomt dat een van beide partijen de verantwoordelijkheid van de andere overneemt.

✔ Binding aan Productie: Differentiële tests en productie-pad tests zorgen voor vertrouwen in de implementatie. De bewijzen zijn niet alleen theoretisch, maar ook praktisch toepasbaar.

✔ Praktische Validatie: De 20-vragen test toont aan dat het systeem goed presteert (15/20), met een zwakke vlag die vroege waarschuwingen geeft voor mogelijke onnauwkeurigheden.

Beperkingen en Risico’s

⚠ Semantische Gap: Het onderscheid tussen “gevonden op een image van het adres” en “gevonden op het adres” blijft een uitdaging. Fouten in de naam-brug (bijvoorbeeld “Lithium” in plaats van “lithium-ion batterij”) zijn moeilijk te voorkomen.

⚠ Afhankelijkheid van de Ledger:

  • Geen persoonlijke sleutels: Momenteel is wie een naam naast een key fingerprint, niet een cryptografische identiteit. Dit betekent dat de ledger niet volledig onveranderlijk is voor de sleutelhouder.
  • Risico: Als de sleutelhouder kwaadwillig is, kan de ledger worden gemanipuleerd.

⚠ Schaalbaarheid:

  • MAZE Net: 8,19 miljoen stukken. Hoe schaalt dit op naar miljarden?
  • Latentie: 2–11 seconden per vraag (externe lookups in de naam-brug zijn een bottleneck).

⚠ Afhankelijkheid van SHA-256: MAZE.AI neemt aan dat SHA-256 collision-vrij is. Hoewel dit in de praktijk zeer onwaarschijnlijk is, is het theoretisch niet bewezen.

⚠ Taalmodel als Proposer:

  • Voordelen: Flexibiliteit in formulering.
  • Risico: Proposals kunnen misleidend zijn (bijvoorbeeld als het model een verkeerd adres citeert).

Conclusie: Een Nieuwe Standaard voor Betrouwbare KI

MAZE.AI introduceert een radicaal nieuwe benadering voor betrouwbare kunstmatige intelligentie. In plaats van te proberen de waarheid van elke bewering te bewijzen — wat onmogelijk is — richt het systeem zich op herleidbaarheid. Elke output is gekoppeld aan een adres in een gecertificeerde store, en deze koppeling is machine-gecheckt.

De combinatie van:

  • Theoretische fundering (Tarski, Lean).
  • Praktische implementatie (MAZE Net, PostgreSQL, JavaScript).
  • Validatie (20-vragen test, differentiële tests).

maakt MAZE.AI tot een baanbrekend systeem dat het vertrouwen in KI naar een hoger niveau tilt.

Toekomstperspectieven

MAZE.AI opent de deur naar nieuwe onderzoeksgebieden en toepassingen:

  • Academisch Onderzoek: Gebruik MAZE.AI als een vertrouwde kennisbank voor literatuurstudies.
  • Juridische Toepassingen: De ledger kan dienen als bewijsvoering voor contracten of wetgeving.
  • Medische Diagnose: Provenance voor medische kennis (bijvoorbeeld: “dit adres bevat de laatste richtlijnen voor diabetesbehandeling”).
  • Integratie met Bestaande Systemen: MAZE.AI kan worden geïntegreerd in systemen als Swarm als een vertrouwde laag voor kennisretrieval.

Slotgedachte

In een wereld waarin desinformatie en onbetrouwbare informatie een steeds grotere bedreiging vormen, biedt MAZE.AI een concreet en haalbaar alternatief. Het systeem toont aan dat we niet hoeven te wachten op een onmogelijke, totale waarheidspredikaat om vertrouwen in KI te hebben. In plaats daarvan kunnen we ons richten op herleidbaarheid, transparantie, en verifieerbaarheid — en dat is precies wat MAZE.AI doet.

Geannoteerde Referentielijst

  1. Tarski, A. (1936).Der Wahrheitsbegriff in den formalisierten Sprachen. Studia Philosophica 1.
    • Annotatie: Dit werk legde de basis voor het inzicht dat een totale waarheidspredikaat voor een voldoende rijke taal (zoals natuurlijke taal) onmogelijk is. MAZE.AI gebruikt dit inzicht om te focussen op herleidbaarheid in plaats van waarheid.
  2. Klein, G., et al. (2009).seL4: Formal Verification of an OS Kernel. SOSP.
    • Annotatie: seL4 is een voorbeeld van een systeem waarbij de correctheid van een draaiend besturingssysteem is bewezen. MAZE.AI volgt een vergelijkbare methodologie, maar dan toegepast op een KI-systeem in plaats van een besturingssysteem.
  3. Leroy, X. (2009).Formal Verification of a Realistic Compiler. CACM 52(7).
    • Annotatie: CompCert toont aan hoe een compiler kan worden geverifieerd tegen een formele specificatie. MAZE.AI gebruikt differentiële testing in plaats van code-extractie om de binding tussen bewijzen en productiecode te waarborgen.
  4. Laurie, B. (2014).Certificate Transparency. CACM 57(10).
    • Annotatie: Certificate Transparency introduceert het concept van een append-only, hash-gechaind logboek voor certificaten. MAZE.AI past dit concept toe op KI-antwoorden, waarbij elke settlement in de ledger een auditeerbaar event is.
  5. Lewis, P., et al. (2020).Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks. NeurIPS.
    • Annotatie: RAG is een standaardbenadering voor het verbeteren van de feitenaccuraatheid van LLM’s door externe kennisbronnen te gebruiken. MAZE.AI gaat een stap verder door niet alleen de bronnen te citeren, maar ook te garanderen dat de output direct afkomstig is uit deze bronnen.
  6. Nakano, R., et al. (2021).WebGPT: Browser-Assisted Question-Answering with Human Feedback. arXiv:2112.09332.
    • Annotatie: WebGPT laat zien hoe modellen citaten kunnen selecteren, maar de citaten worden nog steeds door het model zelf gekozen. MAZE.AI zorgt ervoor dat citaten machine-gecheckt zijn en direct gekoppeld aan de output.
  7. de Moura, L., Ullrich, S. (2021).The Lean 4 Theorem Prover and Programming Language. CADE.
    • Annotatie: Lean 4 is de tool die wordt gebruikt om alle theorema’s in MAZE.AI te bewijzen. Het unieke aan Lean is dat statements en programs dezelfde objecten zijn, wat het mogelijk maakt om bewijzen direct te koppelen aan uitvoerbare code.
  8. Knuth, D. E. (1997).The Art of Computer Programming, Vol. 2, §4.1.
    • Annotatie: Dit werk beschrijft de wiskundige basis van balanced ternary, de numerieke representatie die wordt gebruikt in de adres-kernel van MAZE.AI.
  9. Konstapel, J. (2026).Provable AI. en maze.ai/1 — Specification.
    • Annotatie: Deze werken beschrijven het criterium P, de grensargumenten, en het werkprogramma waar MAZE.AI op is gebaseerd. Elke component van het programma is ofwel gebouwd of opgesomd als open punt in het whitepaper.
maze-ai-whitepaperDownload