Alignment zal nooit volstaan.

Bij taalmodellen is alignment de training die op de pre-training volgt: instruction tuning, daarna reinforcement learning op basis van feedback van mensen of van AI (RLHF, DPO en hun varianten).^{1, 2} Het model wordt beloond voor de antwoorden die beoordelaars verkiezen: behulpzaam, beleefd en binnen de regels die het heeft meegekregen. Zo werden ruwe tekstvoorspellers bruikbare assistenten, en de techniek wordt nog steeds beter.

Alignment werkt echter in op tendensen, niet op afzonderlijke antwoorden. Het maakt een goed antwoord waarschijnlijker, maar zegt u niet of dit antwoord juist is. En omdat beoordelaars antwoorden belonen die juist lijken, kan een model leren om zelfverzekerd te klinken of de vraagsteller gelijk te geven terwijl dat niet terecht is, een probleem dat bekendstaat als sycofantie.³ Met een goed afgestemd model werkt u prettiger samen, maar het kan nog steeds niet aantonen dat een cijfer klopt.

Nergens anders werkt vertrouwen zo. We vertrouwen een boekhoudafdeling niet omdat het personeel goed is opgeleid, maar vanwege procedures: de audit, de tweede handtekening, rekeningen die sluitend moeten zijn.

Vertrouwen op schaal berust op de mogelijkheid om te controleren, niet op hoe goed een systeem is getraind.

Natuurlijke taal is hoe we hardop denken, en ze is van nature dubbelzinnig. Telkens wanneer er meer op het spel stond, bouwden mensen er iets strengers bovenop. Getallen en boekhouding, zodat een schuld voor beide partijen hetzelfde betekende. Algebra, zodat een resultaat opnieuw kon worden afgeleid door iemand die de auteur niet vertrouwde. Vastgelegd recht, logica, bewijs, en uiteindelijk programmeertalen.

Geen van deze systemen verving de intuïtie. Een wiskundige raadt de stelling nog steeds voordat hij haar bewijst. Wat formele systemen ons gaven, is een manier om te communiceren zonder dat men ons op ons woord hoeft te geloven: de redenering reist mee met de conclusie, en een buitenstaander kan haar controleren.

Taalmodellen bevinden zich in de positie waarin wij waren vóór die stap. Vloeiend, snel, vaak juist, en zonder manier om hun redenering over te dragen in een vorm die iemand kan verifiëren.

Met formele systemen communiceren mensen zonder dat ze op hun woord geloofd hoeven te worden.

Dit bedoelen wij met neurosymbolische AI. Het neurale deel doet waar het goed in is: een vraag begrijpen die in gewone woorden is gesteld, in de context van een bedrijf. Het symbolische deel doet wat taal niet kan: het legt het antwoord vast als een regel die kan worden gelezen, geverifieerd, opnieuw uitgevoerd en vergeleken.

De formele laag geeft de machine het instrument dat mensen voor zichzelf hebben gebouwd. Een model dat een regel in een logische taal schrijft, moet zich vastleggen: welke orders tellen mee, over welke periode, op welke kolom. Die keuze kan vervolgens worden gecontroleerd door een verifier, door de data en door de persoon die verantwoordelijk is voor het cijfer.

Een regel blijft ook bestaan. Een alinea gegenereerde uitleg verdwijnt met het gesprek. Een regel wordt bewaard, krijgt een naam en dient als basis, zoals wiskundigen een lemma bewaren: een klein resultaat dat wordt vastgehouden zodat grotere redeneringen erop kunnen steunen. Ook bewaard in git, zodat de geschiedenis van de redenering van een bedrijf kan worden geaudit zoals de geschiedenis van zijn code: wie wat besliste, en wanneer.

Het model vertaalt. De formele laag redeneert. Daardoor is de redenering controleerbaar.

Dat zullen ze, en dat is het sterkste argument voor een formele laag. Een capabeler model krijgt grotere taken en meer autonomie, en produceert meer conclusies dan iemand door lezen kan beoordelen. De kloof tussen wat een model kan produceren en wat een mens kan controleren, groeit met elke generatie.

De uitleg van het model lezen is de eerste controle die niet meer werkt. Wanneer een systeem beter redeneert dan de persoon die het beoordeelt, kan die persoon een deugdelijk argument niet meer onderscheiden van een overtuigend argument. De enige controles die bijblijven, zijn controles die niet afhangen van de intelligentie van wie controleert: een verifier die vaste regels toepast, een query die op de data draait, een tegenvoorbeeld dat wel of niet bestaat.

De wiskunde heeft dit al meegemaakt. Het bewijs van de vierkleurenstelling door Appel en Haken uit 1976 berustte op computerberekeningen die te lang waren om met de hand te controleren. In 2005 verifieerden Georges Gonthier en Benjamin Werner het formeel in de bewijsassistent Coq, zodat alleen de kleine kernel van Coq nog vertrouwd hoeft te worden.⁴ Samuel Ferguson en Thomas Hales bewezen het vermoeden van Kepler in 1998, maar het volledige bewijs werd pas in 2006 gepubliceerd, omdat de referenten het computergedeelte niet konden verifiëren. Het Flyspeck-project verifieerde het daarna formeel in de bewijsassistenten HOL Light en Isabelle, en die controles werden in 2014 afgerond.⁵ Naarmate bewijzen groter werden dan mensen konden lezen, werd formele verificatie belangrijker.

Controleren is ook goedkoper dan vinden. Een verifier hoeft niet zo slim te zijn als het model; hij hoeft alleen stap voor stap te bevestigen wat het model beweert. Een slimmer model concurreert dus niet met de formele laag. Het schrijft betere regels, sneller, en de laag maakt van elk daarvan een resultaat waarop iedereen kan vertrouwen.

Hoe capabeler het model, hoe meer zijn werk een controle nodig heeft die niet afhangt van vertrouwen in het model.

Dat een tweede model kan oordelen over het eerste. Dat is één mening meer, met dezelfde zwakke punten. Verificatie moet komen van iets dat van een andere aard is dan wat wordt geverifieerd.

Dat achteraf toegevoegde vangrails volstaan. Filteren wat een model heeft gezegd, is iets anders dan beperken wat het kan beweren. De controle moet plaatsvinden voordat het antwoord wordt gegeven.

Naar bedrijven waarvan de kennis niet langer verspreid is over hoofden, dashboards en documenten die elkaar tegenspreken, maar één keer is vastgelegd als definities die draaien. Naar agents die een geheugen delen dat bestaat uit geverifieerde regels, en die kunnen worden vervangen zonder te verliezen wat is geleerd. Naar AI die u in gebruik neemt zoals elk serieus instrument: omdat u kunt zien hoe zij tot haar resultaat komt.

Wij bouwen de onderdelen van die laag in de openbaarheid, en het product dat ze aan het werk zet.