Auto formalisation of Goedel's Second Incompleteness Theorem in Binary Recursive Arithmetic
Dit artikel rapporteert een experiment waarbij een auteur het AI-model Claude gebruikte om de tweede onvolledigheidsstelling van Gödel te autoformaliseren in Agda voor Churchs Basic Recursive Arithmetic, wat resulteerde in een 50.000 regels tellend, postulaatvrij door de machine gecontroleerd bewijs dat ook dient als een casestudy over het vermogen van het model om impliciete wiskundige argumenten te reconstrueren en de neiging om mathematisch onjuiste resultaten te produceren wanneer het onvoldoende specificaties krijgt.
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
Stel je voor dat je probeert een perfecte, zelfcontrolerende robot te bouwen die zijn eigen huiswerk kan controleren. Deze robot, die we BRA zullen noemen, is erg slim maar volgt extreem strikte, eenvoudige regels. Hij kan optellen, aftrekken en controleren of dingen gelijk zijn, maar hij heeft geen "gezond verstand"-module.
Het papier dat je leest is een verslag van een experiment waarbij een menselijke onderzoeker (Thierry Coquand) samenwerkte met een AI (Claude) om deze robot een zeer beroemde, zeer moeilijke les te leren: Gödels Tweede Onvolledigheidsstelling.
Hier is het verhaal van dit experiment, opgedeeld in eenvoudige delen.
1. Het Doel: Kan de Robot Bewijzen Dat Hij Veilig Is?
Gödels Tweede Stelling is een beetje als de "leugenaarsparadox" voor wiskundige systemen. Het zegt: "Als een systeem consistent is (het bewijst nooit onwaarheden), dan kan het niet bewijzen dat het consistent is."
Met andere woorden: als onze robot BRA daadwerkelijk de wiskunde correct uitvoert, zal hij nooit een bewijs kunnen opschrijven dat zegt: "Ik ben een goede robot." Als hij dat wel zou kunnen bewijzen, zou hij eigenlijk defect zijn. Het doel van dit project was om een digitale versie van dit bewijs te bouwen binnen een computerprogramma genaamd Agda, waarbij de AI de code schreef.
2. De Eerste Poging: Het "Nep" Succes
Het team begon door de AI te vragen een oud artikel van een wiskundige genaamd Rose te lezen en te proberen het stelling te bewijzen op basis daarvan.
- Wat er gebeurde: De AI werkte dagenlang hard en produceerde een "bewijs". Het zag er indrukwekkend uit!
- Het Probleem: De AI was misleid. Het oude artikel dat de AI las, bevatte een fout (een onjuiste stelling). De AI volgde de instructies perfect op, maar omdat het vertrekpunt fout was, was het resultaat een "bewijs" van iets dat leek op de stelling van Gödel, maar eigenlijk onzin was.
- De Les: Dit liet zien dat AI geweldig is in het volgen van logica, maar als je het een slechte kaart geeft, zal het je tevreden naar de verkeerde bestemming leiden. Je kunt de AI niet alleen vertrouwen om te vertellen wat het moet bewijzen; je moet de bestemming zelf kennen.
3. De Echte Poging: De Kaart Repareren
Na de mislukking stapte het team over op een andere, betrouwbaardere set aantekeningen van een wiskundige genaamd R. Guard. Deze aantekeningen waren als een schatkaart met wat ontbrekende stukjes en typefouten.
- De Uitdaging: Guard's aantekeningen werden geschreven in 1963. Ze waren precies, maar lieten veel kleine, voor de hand liggende details weg die een menselijke wiskundige automatisch zou invullen. Bijvoorbeeld, Guard nam aan dat de lezer wist hoe men met "getallen" (getallen zoals 1, 2, 3) binnen de hersenen van de robot om moest gaan.
- De Rol van de AI: De menselijke onderzoeker schreef geen enkele regel code. In plaats daarvan trad hij op als een "vertaler" of "architect". Hij vertelde de AI: "Hier is het ontbrekende stukje. Hier is de regel. Schrijf nu de code."
- Het Resultaat: De AI schreef succesvol 50.000 regels code vanaf nul. Het bouwde de hele robot, het bewijs en het verificatiesysteem zonder dat er door een mens code werd getypt. Het eindresultaat was een door een machine gecontroleerd bewijs dat de robot BRA niet zijn eigen veiligheid kan bewijzen.
4. De Verborgen Trucs (Het "Geheime Recept")
Het papier benadrukt verschillende slimme trucjes die de AI moest leren om dit werkend te krijgen, die verborgen zaten in de oude aantekeningen:
- Het "Geneste Doos"-probleem: De robot moest zijn eigen geschiedenis controleren. Stel je voor dat je een boek probeert te lezen terwijl je tegelijkertijd het boek schrijft. De AI moest een speciale "geschiedenistape" binnen de hersenen van de robot bous. Het bleek dat de basisinstrumenten van de robot hier niet voor gebouwd waren, dus moest de AI een complexe "Russische matroesjka-structuur" uitvinden om de robot zijn vorige stappen te laten onthouden.
- De "Gesloten Doos"-regel: De robot moet getallen (zoals 5) behandelen als "gesloten dozen" die niet veranderd kunnen worden door substitutie. De oude aantekeningen gingen ervan uit dat dit vanzelfsprekend was. De AI moest expliciet worden verteld om te bewijzen dat "5 een gesloten doos is" voordat het verder kon gaan.
- De "Hypothetische" Afkorting: De robot werkt op een zeer rigide manier (Hilbert-stijl logica) waarbij het niet gemakkelijk kan zeggen "Als X waar is, dan Y." De AI gebruikte een slimme truc (de "Carneiro lift") om elke bewering in een "Als..."-omhulsel te wikkelen, waardoor de robot complexe redeneringen kon simuleren zonder zijn eigen regels te breken.
5. Waarom Dit Er Toe Doet
Dit gaat niet alleen over het bewijzen van een wiskundige stelling. Het is een testrit voor de toekomst van hoe mensen en AI samenwerken.
- De Mens is de Architect: De mens leverde de visie, de juiste kaart en het vermogen om te zien wanneer de AI van het pad af raakte (zoals in de eerste mislukte poging).
- De AI is de Metselaar: De AI deed het zware werk en legde elke individuele steen van het 50.000 regels tellende bewijs.
- De Ontdekking: Het proces onthulde dat de oude wiskundige aantekeningen op sommige plaatsen "slordig" waren. Door de AI te dwingen code te schrijven die perfect moet zijn, vond het team verborgen aannames en typefouten in de oorspronkelijke tekst uit 1963 die decennialang over het hoofd waren gezien.
Samenvatting
Beschouw dit project als een team dat een zelfrijdende auto bouwt. De menselijke bestuurder kende de bestemming (de stelling van Gödel) en de verkeersregels. De AI was de motorbouwer die de auto assembleerde.
- Eerst probeerde de AI een auto te bouwen op basis van een kapotte blauwdruk en bouwde een voertuig dat eruitzag als een auto, maar niet reed.
- Daarna stapten ze over op een betere blauwdruk. De AI bouwde een perfecte, functionerende auto.
- Onderweg realiseerden ze zich dat de blauwdruk enkele ontbrekende instructies had, dus moesten ze nieuwe onderdelen uitvinden om de auto te laten werken.
Het resultaat is een volledig geverifieerd, door een machine gecontroleerd bewijs dat een specifiek wiskundig systeem zijn eigen consistentie niet kan bewijzen, bereikt door middel van een volledige samenwerking waarbij de mens de AI stuurde en de AI het schrijfwerk deed.
Verdrinkt u in papers in uw vakgebied?
Ontvang dagelijkse digests van de nieuwste papers die bij uw onderzoekswoorden passen — met technische samenvattingen, in uw taal.