DeepMinds negen bewijzen op nieuwheid getest

Een wiskundig bewijs kan elegant zijn en toch een fout bevatten die jarenlang onopgemerkt blijft. De AI-agent AlphaProof Nexus van Google DeepMind leverde bewijzen voor negen problemen van Paul Erdős; software controleerde elke stap. Het onderzoek verscheen in mei eerst als preprint (arXiv) en werd op 8 oktober na peerreview gepubliceerd in Science (Science). Software kon de redeneringen controleren. Of ze ook iets nieuws opleverden, moesten wiskundigen beoordelen.

Een scheidsrechter die zich niet laat verblinden

Chatbots kunnen wiskunde formuleren die overtuigend klinkt. Een zelfverzekerde alinea kan een ontbrekende stap verhullen; alleen een aandachtige lezer merkt dat op. AlphaProof Nexus omzeilt dat probleem door in Lean te werken, een programmeertaal waarin definities, beweringen en bewijzen zo precies worden vastgelegd dat een computer ze kan controleren.

Zie Lean als een scheidsrechter die een afgerond bewijs regel voor regel leest en vaste regels toepast. Stijl levert geen punten op. Volgt een stap niet uit de voorgaande stappen, dan faalt het bewijs, hoe elegant de rest ook is.

Het team beschrijft de agent als een systeem dat zoekt naar bewijzen in Lean. Onderzoekers gaven het ook toegang tot AlphaProof, een eerder DeepMind-systeem dat speciaal voor bewijsvoering was ontwikkeld. In de tests van het team leverde een eenvoudiger opzet hetzelfde resultaat op: ook een taalmodel in combinatie met Lean, zonder AlphaProof, vond bewijzen voor alle negen Erdős-problemen (The Decoder). De gespecialiseerde component bleek voor deze problemen dus overbodig.

Het artikel meldt dat de bewijzen voor de negen uitspraken van Erdős en voor 44 vermoedens zijn geaccepteerd. Die vermoedens zijn beweringen die waarschijnlijk waar zijn, maar nog niet bewezen; ze komen uit de Online Encyclopedia of Integer Sequences, een omvangrijke catalogus van getalpatronen (Science). Een van de resultaten van Erdős betreft een tweedelige vraag over gehele getallen die Erdős en András Sárközy in 1970 stelden. Die vraag bleef ruim een halve eeuw open (ABC).

Wat de scheidsrechter niet kan zien

De garantie van Lean heeft een duidelijke grens: het programma bevestigt dat een bewijs de bewering aantoont zoals die in de code staat. Drie vragen blijven daarbuiten: geeft de code weer wat Erdős bedoelde, had iemand de vraag al eerder beantwoord en leert de oplossing iets nieuws?

De vraag uit 1970 laat zien waarom die laatste twee punten ertoe doen. Het tweede deel van de vraag impliceert het eerste, dus één bewijs volstaat voor beide. Toen de bewijzen van de agent werden gedeeld, bleek dat een kleine aanpassing aan een constructie uit het oorspronkelijke artikel uit 1970 beide delen ook beantwoordt (arXiv). De bewijzen van de agent klopten. De opgave bleek toch al dichter bij een oplossing dan het etiket 'open' deed vermoeden.

Om dat soort kwesties te beoordelen, zijn wiskundigen nodig die het vakgebied kennen. Gergely Bérczi, wiskundige aan Aarhus University in Denemarken en een van de auteurs, hielp geschikte vragen te kiezen en de oplossingen te controleren (Aarhus University). Ook hielp hij versies van de bewijzen te schrijven die mensen kunnen volgen. Lean stond in voor elke stap; Bérczi en zijn collega's beoordeelden wat het bewijs als geheel toevoegde.

Die taakverdeling onderscheidt deze studie van een mijlpaal van vorige maand. Toen zette Claude van Anthropic het al bekende bewijs van Fermats laatste stelling om naar Lean (To Brief). Een beroemd bewijs omzetten roept geen vragen op over de nieuwheid ervan. Bij een zoektocht naar uitspraken die als onopgelost gelden, komt juist die toets centraal te staan.

Het team heeft de bewijsbestanden gepubliceerd, zodat anderen ze door dezelfde scheidsrechter kunnen halen (GitHub). De studie laat een concreet afgebakende vooruitgang zien: een AI-agent leverde machinecontroleerbare bewijzen voor enkele uitspraken die wiskundigen als onopgelost beschouwden. Die garantie geldt voor de uitspraken zoals ze in Lean zijn vastgelegd. Wat elk bewijs aan de wiskunde toevoegde, moesten de wiskundigen die ze lazen nog altijd beoordelen.