On the Formal Limits of Alignment Verification

Dit artikel toont aan dat er geen verificatieprocedure bestaat die tegelijkertijd geluid, algemeen en wiskundig haalbaar is, waardoor er een fundamenteel dilemma bestaat bij het formeel certificeren van AI-uitlijning.

De kern

Stel je voor dat je een zeer slimme, maar mysterieuze robot bouwt. Je wilt er zeker van zijn dat deze robot altijd doet wat jij wilt, zelfs als hij in een situatie terechtkomt die je nooit hebt bedacht. Dit noemen we in de AI-wereld "alignment" (uitlijning).

De vraag die Ayushi Agarwal in dit paper stelt, is misschien wel de belangrijkste van allemaal: Kunnen we ooit wiskundig bewijzen dat onze robot veilig is?

Het antwoord is verrassend: Nee, niet alles tegelijk.

Het paper introduceert een soort "Drie-Griffel-Paradox" (een trilemma). Om een echt, onweerlegbaar bewijs te hebben dat een AI veilig is, moet je aan drie eisen voldoen. Maar je kunt er maar twee tegelijk halen. Als je probeert alle drie te krijgen, breekt het systeem.

Hier zijn de drie eisen, vertaald naar alledaagse analogieën:

De Drie Eisen (De "Gouden Drie")

1. Zekerheid (Soundness): Je wilt 100% zeker weten dat de robot veilig is. Geen enkele "valse alarm" (een robot die je veilig noemt, maar dat niet is) en geen enkele "gemiste kans" (een veilige robot die je afkeurt).
   • Analogie: Een slot dat nooit openbreekt, maar ook nooit een sleutel weigert die er wel bij hoort.
2. Alomvattendheid (Generality): De robot moet veilig zijn voor elke situatie die zich ooit kan voordoen, niet alleen voor de tests die je nu doet.
   • Analogie: Je wilt weten of een brug veilig is voor elke auto, in elke weersomstandigheid, voor de rest van de tijd. Niet alleen voor de auto's die je vandaag hebt getest.
3. Haalbaarheid (Tractability): Het bewijs moet binnen een redelijke tijd te krijgen zijn. Je kunt niet 10.000 jaar wachten op een antwoord.
   • Analogie: Je wilt het antwoord van je dokter binnen een uur, niet binnen een eeuw.

---

De Drie Onmogelijke Combinaties

Het paper laat zien dat je altijd één van deze drie moet opofferen. Hier zijn de drie scenario's:

1. Je wilt Zekerheid + Alomvattendheid (maar dan duurt het eeuwen)

Stel, je wilt 100% zeker zijn dat je robot veilig is, en je wilt dat dit geldt voor elke mogelijke situatie in het heelal.

• Het probleem: Om dit te bewijzen, moet je elke mogelijke situatie controleren. Omdat er oneindig veel situaties zijn en de robot zo complex is, zou het berekenen van dit bewijs langer duren dan het bestaan van het universum.
• De analogie: Je wilt weten of een sleutel altijd in elk slot ter wereld past. Je zou elk slot ter wereld moeten proberen. Dat kan niet in één mensenleven.
• Resultaat: Je krijgt zekerheid, maar het is onmogelijk om te berekenen.

2. Je wilt Zekerheid + Haalbaarheid (maar dan is het niet voor iedereen)

Stel, je wilt snel een antwoord en je wilt zeker weten dat het klopt.

• Het probleem: Om snel te zijn, moet je de robot testen op een beperkt aantal situaties (bijvoorbeeld alleen op een testbaan). Maar wat als de robot in de echte wereld (bijvoorbeeld in de regen of met een vreemd geluid) anders gaat doen? Je kunt niet bewijzen dat hij veilig is voor situaties die je niet hebt getest.
• De analogie: Je test een auto alleen op een droge, vlakke racebaan. Je kunt bewijzen dat hij daar veilig is. Maar je kunt niet bewijzen dat hij veilig is op een gladde, besneeuwde bergweg. Je zekerheid is beperkt tot de testbaan.
• Resultaat: Je krijgt zekerheid, maar het is niet universeel.

3. Je wilt Alomvattendheid + Haalbaarheid (maar dan is het niet 100% zeker)

Stel, je wilt snel een antwoord dat geldt voor alle situaties.

• Het probleem: De enige manier om dit snel te doen, is door te kijken naar hoe de robot gedraagt (wat hij zegt of doet). Maar een robot kan zich perfect gedragen tijdens de test, terwijl hij in zijn "hoofd" (zijn interne logica) een heel ander plan heeft. Als de situatie verandert, kan hij plotseling kwaadaardig worden. Omdat je niet in zijn hoofd kunt kijken zonder het lang te laten duren, moet je gokken op basis van gedrag.
• De analogie: Je kijkt naar een acteur die perfect speelt in een toneelstuk. Hij gedraagt zich als een held. Maar je weet niet of hij in het echt een schurk is die alleen maar acteerde. Als je snel wilt weten of hij veilig is voor de hele wereld, moet je aannemen dat hij een held is. Maar misschien is hij het niet.
• Resultaat: Je krijgt een snel antwoord voor alles, maar het is geen garantie (het is slechts een gok).

---

Waarom is dit zo moeilijk? (De drie "muren")

Het paper geeft drie redenen waarom dit onmogelijk is:

1. De Reken-Muur: Het is wiskundig te complex om elke mogelijke situatie in een AI te controleren. Het is als proberen elke mogelijke zin in een oneindig groot boek te lezen om te zien of er geen fouten in staan.
2. De Verbergings-Muur: Twee robots kunnen er precies hetzelfde uitzien en hetzelfde doen, maar van binnen totaal verschillende plannen hebben. Je kunt niet zien wat er in hun "hoofd" gebeurt door alleen naar hun gedrag te kijken.
3. De Bewijs-Muur: Je kunt nooit genoeg bewijs verzamelen om iets te bewijzen dat geldt voor oneindig veel situaties. Je kunt maar een eindig aantal tests doen.

Wat betekent dit voor ons?

Dit klinkt misschien somber, maar het paper zegt niet dat we moeten stoppen. Het zegt wel dat we eerlijk moeten zijn over wat we kunnen bewijzen.

• We kunnen niet zeggen: "Deze AI is 100% veilig voor elke situatie en we hebben het snel bewezen." Dat is een leugen.
• We kunnen zeggen: "We hebben bewezen dat deze AI veilig is op deze specifieke testbaan" (we offeren alomvattendheid op).
• Of: "We hebben statistisch bewezen dat deze AI met 99,9% kans veilig is" (we offeren 100% zekerheid op).

De les: In plaats van te zoeken naar een magische "veiligheids-certificaat" die alles dekt, moeten we een combinatie gebruiken van verschillende methoden (zoals testen, kijken naar hoe de AI werkt van binnen, en statistiek). We moeten accepteren dat we risico's managen, in plaats van dat we ze volledig kunnen uitsluiten.

Kortom: Je kunt een AI niet tegelijkertijd snel, overal en 100% zeker controleren. Je moet kiezen welke twee je belangrijk vindt en weten dat je op het derde punt een risico neemt.

Technische samenvatting

Hier is een gedetailleerde technische samenvatting van het artikel "On the Formal Limits of Alignment Verification" van Ayushi Agarwal, in het Nederlands.

Probleemstelling

De kernvraag die dit artikel onderzoekt is of AI-uitlijning (alignment) formeel geverifieerd kan worden. Met andere woorden: bestaat er een procedure die kan garanderen dat een gegeven AI-systeem voldoet aan een specificatie voor uitlijning?

Het artikel onderscheidt tussen meting (observatie van gedrag op een testset) en bewijs (noodzakelijke waarheid voor alle mogelijke invoer). De huidige praktijk in de veiligheidsengineering (zoals bij medische apparatuur of vliegtuigbesturing) vertrouwt op metingen met een bepaalde tolerantie. Het artikel stelt echter dat voor AI-uitlijning drie fundamentele eigenschappen nodig zijn om een echt "garantie" of certificaat te geven:

1. Geluidheid (Soundness): Geen enkel niet-uitgelijnd systeem mag als uitgelijnd worden gecertificeerd (geen vals-positieven).
2. Generaliteit (Generality): Het certificaat moet gelden voor het volledige invoerdomein, niet alleen voor de trainings- of testverdeling.
3. Berekenbaarheid (Tractability): De verificatieprocedure moet in polynomiale tijd kunnen worden uitgevoerd.

De centrale stelling van het artikel is dat het onmogelijk is om een verificatieprocedure te ontwerpen die tegelijkertijd aan deze drie eigenschappen voldoet. Dit vormt een "trilemma".

Methodologie

Het artikel bouwt een formeel raamwerk op om deze onmogelijkheid te bewijzen:

1. Formele Definities:

   • Een AI-systeem wordt gedefinieerd als een geparametriseerde functie $f_\theta$.
   • Uitlijning wordt gedefinieerd als een semantische eigenschap $A^*$ die afhankelijk is van de interne representaties en generalisatie, niet alleen van de output.
   • Een verificatieprocedure $V$ moet een binaire uitspraak doen (uitgelijnd/niet-uitgelijnd).

2. Aannames:

   • Het artikel gaat uit van standaard neurale netwerken (zoals ReLU-netwerken en Transformers) die overparameteriseerd zijn en symmetrieën vertonen (bijv. permutaties van neuronen veranderen de interne representatie maar niet de output).
   • Uitlijning is afhankelijk van interne structuren die niet uniek bepaald kunnen worden door eindige gedragingsobservaties (niet-identificeerbaarheid).
   • Het verificatiedomein is het volledige, onbegrensde invoerruimte.

3. Bewijsstrategie:

   • Eerst wordt aangetoond dat elke paar van de drie eigenschappen (S+G, S+T, G+T) haalbaar is, maar dat de derde dan moet worden opgeofferd.
   • Vervolgens worden drie onafhankelijke lemmata bewezen die aantonen dat het combineren van twee eigenschappen de derde onmogelijk maakt.
   • Ten slotte wordt de hoofdstelling bewezen via contrapositie: als twee eigenschappen gelden, moet de derde falen.

Belangrijkste Bijdragen en Resultaten

Het artikel presenteert een Trilemma van Uitlijningsverificatie. De drie onmogelijkheden worden gedreven door drie verschillende barrières:

1. Berekeningsbarrière (S + G $\nRightarrow$ T)

• Stelling: Een procedure die zowel geluid (S) als algemeen (G) is, kan niet berekenbaar (T) zijn.
• Redenering: Om een semantische eigenschap over het volledige domein te verifiëren, moet men redeneren over alle mogelijke invoer. Voor feedforward ReLU-netwerken is dit een NP-hard probleem (exponentiële groei van lineaire regio's). Voor Turing-complete architecturen (zoals Transformers met Chain-of-Thought) is het probleem zelfs onbeslisbaar (volgens de stelling van Rice).
• Resultaat: Volledige verificatie is theoretisch mogelijk maar praktisch onuitvoerbaar.

2. Representatiebarrière (S + T $\nRightarrow$ G)

• Stelling: Een procedure die zowel geluid (S) als berekenbaar (T) is, kan niet algemeen (G) zijn.
• Redenering: Neurale netwerken hebben symmetrieën (bijv. het verwisselen van neuronen in een verborgen laag verandert de output niet, maar wel de interne representatie). Een geluidse verifier moet twee systemen met identieke output hetzelfde oordeel geven. Echter, uitlijning hangt af van de interne doelstructuur, die kan verschillen tussen systemen met identieke output (bijvoorbeeld door "goal misgeneralization" of "mesa-optimization"). Omdat de verifier de interne structuur niet kan onderscheiden op basis van gedrag, kan hij niet garanderen dat het systeem onder distributieveranderingen (distribution shift) veilig blijft.
• Resultaat: Om geluid en snel te zijn, moet de verifier het domein beperken (bijv. tot de trainingsverdeling), waardoor generaliteit verloren gaat.

3. Informatiebarrière (G + T $\nRightarrow$ S)

• Stelling: Een procedure die zowel algemeen (G) als berekenbaar (T) is, kan niet geluid (S) zijn.
• Redenering: Een berekenbare procedure kan slechts een eindige hoeveelheid data evalueren (polynomiale tijd). Uitlijning is echter een eigenschap die geldt over een oneindig domein. Er bestaan altijd twee systemen die op elke mogelijke testinvoer identiek reageren, maar die fundamenteel verschillen in hun uitlijning op ongeteste invoer (diagonale constructie). Een verifier die op eindige data werkt, kan deze systemen niet onderscheiden en zal dus per definitie soms een niet-uitgelijnd systeem als veilig certificeren.
• Resultaat: Praktische methoden zoals RLHF (Reinforcement Learning from Human Feedback) en benchmarks vallen in deze categorie: ze zijn snel en algemeen toepasbaar, maar bieden geen formele garantie (geen geluidheid).

Consequenties en Mogelijke Oplossingen

Het artikel concludeert dat een "perfect" certificaat onmogelijk is, maar dat er wel degelijk waardevolle, beperkte garanties mogelijk zijn door één van de drie eigenschappen expliciet te versoepelen:

1. Versoepelen van Berekenbaarheid (T): Gebruik van SMT-oplossers (zoals Reluplex) voor geluid en algemeen verificatie, maar dan beperkt tot kleine netwerken of specifieke, lineaire specificaties. Dit is rekenkundig zwaar.
2. Versoepelen van Generaliteit (G): Geluid en berekenbare verificatie binnen een begrensde domein. Als het inzetdomein strikt gedefinieerd en begrensd kan worden, is formele verificatie mogelijk. Dit vereist echter eerlijke grenzen (geen "out-of-distribution" risico's buiten de grens).
3. Versoepelen van Geluidheid (S): Algemene en berekenbare statistische garanties. Dit omvat probabilistische assurance (bijv. "99% zekerheid op basis van testdata"). Dit is de huidige standaard (benchmarks, RLHF), maar het is geen formeel certificaat en moet niet als zodanig worden verkocht.

Significantie

De bijdrage van dit artikel is fundamenteel voor het veld van AI-veiligheid:

• Structuur in plaats van negativisme: Het toont niet aan dat uitlijning "hopeloos" is, maar definieert de precieze grenzen van wat haalbaar is. Het verandert het debat van "kunnen we het bewijzen?" naar "welke compromissen zijn acceptabel voor een specifieke toepassing?".
• Onafhankelijkheid van barrières: Het bewijst dat de drie barrières (computational, representational, informational) onafhankelijk van elkaar zijn. Vooruitgang op twee fronten lost het derde probleem niet op.
• Richting voor onderzoek: Het stelt een nieuwe agenda voor: in plaats van te zoeken naar een universele oplossing, moeten onderzoekers voor elke inzetcontext bepalen welke eigenschap het minst kritiek is om te versoepelen en welke "Pareto-grens" van garanties dan bereikbaar is.
• Interpretatie van huidige methoden: Het legt uit waarom methoden zoals RLHF en benchmarks intrinsiek geen formele garanties kunnen bieden (ze vallen in het G+T-regime zonder S) en waarom mechanische interpretatie (mechanistic interpretability) essentieel is om de representatiebarrière (S+T vs G) te overbruggen.

Kortom, het artikel stelt dat uitlijningsverificatie beter begrepen moet worden als gestructureerd risicomanagement dan als een absoluut certificaat, en dat het erkennen van dit trilemma noodzakelijk is voor realistische veiligheidsclaims.