💻 computer science

Cryptographic certificates of validity for trustworthy AI

Dit artikel stelt een raamwerk voor betrouwbare agentische AI voor door beknopte cryptografische certificaten te genereren die wiskundig bewijzen dat de acties van een agent voldoen aan formeel gespecificeerde beleidsregels, wat onafhankelijke verificatie mogelijk maakt zonder heruitvoering of vertrouwen in de agent.

Oorspronkelijke auteurs: Murdoch J. Gabbay

Gepubliceerd 2026-06-24

📖 6 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Murdoch J. Gabbay

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Het Grote Idee: Vertrouw op het Bewijs, Niet op de Persoon

Stel je voor dat je een robot inhuurt om een vlucht voor je te boeken. In het verleden vertrouwden we robots (of AI-agenten) omdat we wisten wie ze gebouwd had of omdat ze een digitale handtekening hadden die zei: "Ik ben van Bedrijf X."

Maar wat als de robot een foutje bevat, of wat als het een "Byzantijnse" robot is (een chique term voor een robot die zich vreemd of kwaadwillig gedraagt)? Een handtekening bewijst alleen wie de boodschap heeft gestuurd, niet of de boodschap correct of veilig is.

Het paper van Murdoch Gabbay stelt een nieuwe manier voor om AI te vertrouwen: In plaats van de identiteit van de robot te vertrouwen, vertrouwen we op een cryptografisch certificaat dat bewijst dat de actie van de robot de regels volgt.

Denk er zo over na:

De Oude Manier: Je vertrouwt een chef omdat hij een specifieke hoed draagt en een licentie heeft. Je hoopt dat hij de soep niet heeft vergiftigd.
De Nieuwe Manier: De chef overhandigt je een verzegeld, onbreekbaar bonnetje. Dit bonnetje bewijst wiskundig dat de soep werd gekookt op de juiste temperatuur, met de juiste ingrediënten, en dat er geen gif aan is toegevoegd. Je hoeft niet de naam van de chef te kennen of hem te zien koken; je controleert gewoon het bonnetje.

Hoe het Werkt: De "Magische Vertaler"

Het paper beschrijft een proces van drie stappen om deze bonnetjes te maken.

1. De Regels Opschrijven (De "Wet")

Eerst nemen we de regels die we willen dat de AI volgt (bijv. "Geef nooit meer dan $500 uit" of "Vlieg alleen naar landen met een reisadvies") en schrijven we die op in een strikte wiskundige taal die logica wordt genoemd.

Analogie: Stel je voor dat je de regels van een bordspel opschrijft in een taal die een computer perfect kan begrijpen, zonder ruimte voor "misschien" of "ik denk dat".

2. De Vertaling (De "Compiler")

Vervolgens gebruiken we een speciale tool (een compiler) om die logische regels te vertalen naar een wiskundige puzzel.

De Magie: Het paper legt een slimme truc uit waarbij "Waar" wordt getransformeerd naar het getal 0, en "Onwaar" wordt een positief getal.
Analogie: Stel je een weegschaal voor. Als de AI de regels heeft gevolgd, balanceert de weegschaal perfect op nul. Als de AI een regel heeft overtreden, slaat de weegschaal door en toont een zwaar, positief getal. Het doel is te bewijzen dat de weegschaal op nul staat.

3. Het Certificaat (Het "Bonnetje")

De AI (of een helper) lost de wiskundige puzzel op en genereert een piepklein, cryptografisch bewijs. Dit bewijs zegt: "Ik heb een geheime oplossing die ervoor zorgt dat de weegschaal op nul balanceert."

Het Coole Deel: Een verifieerder (de persoon die de AI controleert) kan naar dit kleine bewijs kijken en direct weten dat de regels zijn gevolgd. Ze hoeven niet de private gedachten van de AI te zien, ze hoeven de hele berekening niet opnieuw uit te voeren, en ze hoeven de AI niet te vertrouwen. Ze controleren gewoon de wiskunde.

Een Concreet Voorbeeld: De Kracht van Twee

Het paper gebruikt een eenvoudig voorbeeld van het berekenen van $2^2$ (2 tot de macht 2) om te laten zien hoe dit werkt.

Stel je voor dat de AI beweert: "Ik heb berekend dat $2^2 = 4$ ."
Om te bewijzen dat dit geen leugen is, geeft de AI niet alleen "4" door. Het levert een derivation tree (een stapsgewijze geschiedenis):

Stap 1: $2^0 = 1$ (Het startpunt).
Stap 2: $2^1 = 2$ (Gebaseerd op Stap 1).
Stap 3: $2^2 = 4$ (Gebaseerd op Stap 2).

Het cryptografische certificaat bewijst dat deze stappen correct aan elkaar gekoppeld zijn. Als de AI een stap zou overslaan of een getal zou veranderen, zou de wiskundige puzzel falen en zou het certificaat ongeldig zijn.

Waarom Dit Belangrijk Is voor AI-agenten

Het paper betoogt dat naarmate AI-agenten echte dingen gaan doen (vluchten boeken, facturen goedkeuren, code implementeren), we een manier nodig hebben om hun acties te verifiëren voordat ze gebeuren, en niet alleen achteraf in de logs te kijken.

Geen Herhaling Nodig: Het controleren van het certificaat is snel. Je hoeft het werk van de AI niet opnieuw te doen.
Privacy: Door gebruik te maken van "Zero-Knowledge"-functies, kan de AI bewijzen dat hij de regels heeft gevolgd zonder zijn private gegevens prijs te geven (zoals je creditcardnummer of een geheim strategieplan).
Geen Blind Vertrouwen: Je hoeft de ontwikkelaar van de AI niet te vertrouwen. Je vertrouwt alleen de wiskunde.

Wat Dit Paper NIET Doet (Belangrijke Beperkingen)

De auteur is zeer voorzichtig in het vermelden wat deze technologie niet kan doen:

Het schrijft de regels niet voor je. Het certificaat bewijst dat de AI de regels heeft gevolgd die jij hem hebt gegeven. Als je een slechte regel hebt geschreven (bijv. "Geef al het geld uit"), dan zal het certificaat bewijzen dat de AI die slechte regel perfect heeft uitgevoerd.
Het garandeert geen veiligheid. Het garandeert alleen dat de specifieke wiskundige voorwaarde is vervuld. Het bewijst niet dat de voorwaarde zelf wijs, ethisch of veilig was.
Het vervangt menselijk toezicht niet. Mensen moeten nog steeds beslissen wat de regels moeten zijn en het systeem auditeren.

Samenvatting

Dit paper stelt een "Proof-Carrying Action"-systeem voor voor AI. Net zoals een bestuurder een rijbewijs bij zich kan hebben om te bewijzen dat hij mag rijden, zou een AI-agent een cryptografisch certificaat bij zich dragen om te bewijzen dat zijn actie correct is.

Het overbrugt de kloof tussen Formele Logica (de regels) en Cryptografie (het bewijs), waardoor we kunnen verifiëren dat een AI zich correct gedraagt zonder de AI te hoeven vertrouwen of zijn private gegevens te hoeven zien. Het is een manier om te zeggen: "Ik vertrouw je niet, maar ik vertrouw de wiskunde die je me net hebt overhandigd."

Probleemstelling

Naarmate AI-systemen overgaan van het produceren van aanbevelingen naar het uitvoeren van autonome acties (bijv. vluchten boeken, facturen goedkeuren, code implementeren), schieten traditionele waarborgmechanismen tekort. Cryptografische handtekeningen authenticeren de herkomst van een bericht, maar kunnen niet bewijzen dat een actie vooraf voldoet aan specifieande correctheids-, veiligheids- of nalevingsvoorwaarden. Evenzo kan retrospectieve logging geen beleidschendingen voorkomen voordat ze plaatsvinden. Het artikel behandelt de noodzaak van een mechanisme om onafhankelijk controleerbaar bewijs te leveren dat een actie van een agent voldoet aan een overeengekomen formeel beleid voordat de actie wordt geaccepteerd, zonder dat de verifieerder de interne implementatie van de agent hoeft te vertrouwen of de berekening opnieuw moet uitvoeren.

Methodologie

Het artikel stelt een framework voor het genereren van cryptografische certificaten van geldigheid door formele logica te overbruggen met beknopte cryptografische bewijzen. De methodologie volgt een driestaps-pipeline:

Formele Specificatie: De relevante beleid of correctheidsvoorwaarde wordt uitgedrukt als een logische predicaat in een specifieke eerste-orde logica.
Arithmetisering: Deze predicaat wordt gecompileerd naar een getuige-controleprobleem (witness-checking problem) over polynomiale restricties. De kern bijdrage van de wiskunde is een vertaling van de geldigheid van eerste-orde logica naar oordelen over polynomiale restricties waarbij:
- Waarheid (geldigheid) wordt gerepresenteerd door de waarde 0.
- Onwaarheid (ongeldigheid) wordt gerepresenteerd door een strikt positieve waarde.
- Logische connectieven worden in verband gebracht met algebraïsche operaties:
  - Gelijkheid ( $t=t'$ ) brengt naar $(t-t')^2$ .
  - Conjunctie ( $\phi \land \psi$ ) brengt naar de som $[\phi] + [\psi]$ .
  - Disjunctie ( $\phi \lor \psi$ ) brengt naar het product $[\phi] \times [\psi]$ .
  - Universele kwantificering over een bereik wordt in verband gebracht met een sommatie over dat bereik.
- Recursie en inductieve definities (bijv. exponentiëring) worden gecodeerd door de getuige-data (witness data) te structureren als matrices waarbij kolommen afleidingstappen representeren, met pointers in een speciale rij om ervoor te zorgen dat de recursieve structuur goed gevormd is.
Cryptografische Certificering: De agent (of een geassocieerde prover) genereert een beknopt cryptografisch bewijs (mogelijk zero-knowledge) dat aantoont dat de afgeleide polynomiale restricties van het beleid worden voldaan door de specifieke actie-data.

Het verificatieproces houdt in dat de verifieerder het bewijs controleert tegen een publieke sleutel en parameters. Als het bewijs wordt geverifieerd, accepteert het systeem dat de actie voldoet aan de formele predicaat, zonder dat de private getuige-data van de agent geïnspecteerd of de berekening opnieuw uitgevoerd hoeft te worden.

Belangrijkste Bijdragen

Wiskundige Vertaling: Het artikel biedt een compacte, applicatie-agnostische arithmetisering van de geldigheid van eerste-orde logica naar polynomiale restricties (Definities 2.3–2.7, Stelling 2.9). Het demonstreert hoe complexe logische structuren, inclusief recursie en inductieve afleidingen, kunnen worden gecodeerd in algebraïsche relaties die geschikt zijn voor cryptografische backends.
Proof-Carrying Agent Actions: Het conceptualiseert acties van agenten als "bewijs-dragend" (proof-carrying) in een specifieke cryptografische zin. In tegenstelling tot Proof-Carrying Code (PCC), dat vaak inspectie van de broncode vereist, staat deze aanpak onbetrouwbare, potentieel black-box agenten toe om beknacht bewijs van naleving te leveren.
Integratie met Bestaande Technologie: Het framework is ontworpen om te koppelen met bestaande succincte argument-systemen (bijv. SNARKs, zkVMs zoals Cairo of RISC0) en polynomiale commitment-schema's (bijv. Halo2, Zinc). Het positioneert de voorgestelde logica als een hoog-niveau specificatielaag die compileert naar deze cryptografische primitieven.
Onderscheid van Runtime Verification: De aanpak verschilt van runtime verificatie door een preventief, beknacht certificaat te bieden in plaats van een retrospectief spoor, en verschilt van standaard PCC door niet te vereisen dat het interne ontwerp van de agent open of vertrouwd is, enkel dat deze in staat is het certificaat te produceren.

Resultaten en Voorbeelden

Het artikel valideert de aanpak via theoretische voorbeelden in plaats van empirische benchmarks:

Basale Logica: Het demonstreert hoe waarheidswaarden, gelijkheid, conjunctie, disjunctie en bereikcontroles worden gecodeerd als polynomialen die nul evalueren indien en slechts indien de conditie standhoudt.
Recursieve Berekening: Een gedetailleerd voorbeeld codeert de inductieve definitie van exponentiëring ( $a^b$ ). Het artikel laat zien hoe een matrix van getuige-data een afleidingsboom kan coderen, waarbij rijen 1–3 input/output-samples opslaan en rij 4 pointers naar voorgaande stappen bevat. De geldigheidspredicaat zorgt ervoor dat deze pointers een goed gevormde recursieve structuur vormen.
Robuustheid: Het artikel merkt op dat een matrix correcte input-output waarden kan bevatten, maar toch kan falen voor de geldigheidspredicaat als de "bewijs-dragende" structuur (de pointers) ontbreend of defect is, wat illustreert dat het certificaat de afleiding van het resultaat valideert, en niet alleen het resultaat zelf.

Betekenis en Reikwijdte

Het artikel positioneert dit werk als een "middengrond" tussen de formele verificatie van broncode en cryptografische authenticatie. De primaire betekenis ligt in het bieden van een cryptografisch analoog van proof-carrying code voor agentische AI-systemen.

De auteur merkt expliciet de beperkingen en de reikwijdte van het voorstel op:

Reikwijdte: De wiskundige architectuur is algemeen en toepasbaar op elk domein waar onbetrouwbare partijen controleerbaar bewijs van correctheid moeten leveren. De specifieke toepassing op AI-agenten is gekozen omdat autonome actie een dringende behoefte aan preventieve zekerheid creëert.
Beperkingen: Een certificaat van geldigheid bewijst dat een formele specificatie is nageleefd. Het bewijst niet dat de formele specificatie zelf de "juiste" is (d.w.z. dat deze veiligheid, juridische of ethische vereisten correct vangt). Het artikel benadrukt dat het dichten van de kloof tussen formele predikaten en de echte wereld vereist dat governance, auditing en risicobeheer (verwijzend naar NIST-frameworks) worden toegepast, wat niet enkel door wiskunde of cryptografie kan worden opgelost.
Toekomstig Werk: Het artikel identificeert de noodzaak voor praktische implementatiedetails, waaronder compiler-ontwerp, het benchmarken van bewijskosten en het vaststellen van governance voor het schrijven en auditen van beleid.

Samenvattend stelt het artikel een theoretisch en wiskundig fundament voor om beknachte, cryptografisch verifieerbare bewijzen van beleidsnaleving te koppelen aan acties van AI-agenten, waarmee het vertrouwensmodel verschuift van "vertrouw de herkomst" naar "vertrouw het bewijs".