DeepMinds ni beviser prøves for nyhedsværdi

Et matematisk bevis kan være elegant og stadig rumme et hul, som ingen opdager i årevis. Google DeepMinds AI-agent AlphaProof Nexus har udarbejdet beviser for ni problemer stillet af Paul Erdős, og software har kontrolleret hvert trin. Arbejdet blev først offentliggjort som preprint i maj (arXiv) og udkom efter fagfællebedømmelse i Science 8. oktober (Science). Softwaren kunne bekræfte logikken, men spørgsmålet om, hvorvidt beviserne bidrog med noget nyt, måtte matematikerne afgøre.

En kontrollant, der ikke lader sig charmere

Chatbots er gode til at skrive matematik, der lyder overbevisende. Et selvsikkert formuleret afsnit kan skjule et manglende led, som kun en omhyggelig læser opdager. AlphaProof Nexus undgår den fælde ved at arbejde i Lean, et programmeringssprog til at formulere definitioner, påstande og beviser så præcist, at en computer kan kontrollere dem.

Man kan se Lean som en dommer, der gennemgår hvert trin i et færdigt bevis og følger faste regler. Stil giver ingen point. Hvis ét trin ikke følger af de foregående, forkastes beviset, uanset hvor elegant resten ser ud.

Forskerne beskriver agenten som et system, der leder efter beviser formuleret i Lean. De gav den også adgang til AlphaProof, et tidligere DeepMind-system udviklet specifikt til beviser. I holdets test gav en enklere opsætning samme resultat: En sprogmodel koblet til Lean, men uden AlphaProof, fandt stadig beviser for alle ni Erdős-problemer (The Decoder). På de problemer viste specialistsystemet sig overflødigt.

Artiklen fremlægger beviser, som Lean accepterede, for de ni Erdős-udsagn og for 44 formodninger fra Online Encyclopedia of Integer Sequences, et omfattende katalog over talmønstre (Science). Formodninger er påstande, man anser for sande, men endnu ikke har bevist. Blandt Erdős-resultaterne er et todelt spørgsmål om hele tal, som Erdős og András Sárközy stillede i 1970. Det stod ubesvaret i mere end et halvt århundrede (ABC).

Hvad kontrollanten ikke kan se

Leans garanti har en klar grænse: Den bekræfter, at beviset fastslår udsagnet, præcis som det står i koden. Tre spørgsmål ligger uden for kontrollen: om koden indfanger, hvad Erdős mente; om nogen allerede har besvaret spørgsmålet; og om svaret giver ny matematisk indsigt.

Problemet fra 1970 viser, hvorfor de sidste to spørgsmål betyder noget. Dets anden del indebærer den første, så ét bevis afgør begge. Da agentens beviser blev delt, viste det sig, at en mindre ændring af en konstruktion i den oprindelige artikel fra 1970 også besvarer begge dele (arXiv). Agentens beviser var korrekte. Problemet var blot tættere på en løsning, end betegnelsen »åbent« gav indtryk af.

Det kræver fagfolk at opdage den slags. Gergely Bérczi, matematiker ved Aarhus Universitet og en af artiklens forfattere, var med til at udvælge egnede spørgsmål og kontrollere løsningerne (Aarhus University). Han bidrog også til at skrive versioner af beviserne, som mennesker kan følge. Lean godkendte hvert trin, mens Bérczi og kollegerne vurderede, hvad beviserne samlet set tilføjede.

Den arbejdsdeling adskiller studiet fra et gennembrud måneden før. Da omsatte Anthropic’s Claude det allerede kendte bevis for Fermats sidste sætning til Lean (To Brief). En oversættelse af et berømt bevis rejser ikke tvivl om nyhedsværdien. En søgning blandt udsagn, der regnes for uløste, gør derimod spørgsmålet om nyhedsværdi afgørende.

Holdet har offentliggjort bevisfilerne, så andre kan lade den samme kontrollant gennemgå dem (GitHub). Fremskridtet i studiet er afgrænset: En AI-agent har udarbejdet maskinkontrollerbare beviser for nogle udsagn, som matematikere regnede for uløste, og garantien gælder de udsagn, sådan som de er formuleret i Lean. Det var fortsat matematikerne, der måtte afgøre, hvad hvert bevis tilføjede til faget.