DeepMind AI löser nio Erdős-problem i Science-artikel

Google DeepMind, en del av Alphabet ↘ 0.72%, har publicerat en expertgranskad rapport om AlphaProof Nexus, ett AI-system som löst nio öppna problem ställda av matematikern Paul Erdős och bevisat 44 förmodanden från On-Line Encyclopedia of Integer Sequences (OEIS). Artikeln publicerades torsdagen den 8 oktober i Science. Två av Erdős-problemen formulerades av Erdős och András Sárközy 1970 och hade varit olösta i 56 år.elmundo+2

Studien ger expertgranskat stöd till resultat som DeepMind först publicerade på arXiv i maj. Den kommer i en tid då AI-labb tävlar om att visa att deras system kan utföra matematik på forskningsnivå, ett race som vissa ledande matematiker har kritiserat.abc+1

Hur det fungerar

Systemet använder Gemini 3.1 Pro för att söka efter bevis och bevisassistenten Lean för att kontrollera dem. Lean verifierar varje steg mekaniskt och förkastar alla bevis med luckor, och agenten fortsätter att prova nya strategier, ofta med många försök som körs parallellt. Teamet försökte lösa 353 Erdős-problem och 492 OEIS-förmodanden. De kontrollerade de 44 OEIS-bevisen manuellt och bekräftade att problemen var korrekt formaliserade och inte hade bevisats tidigare. Enligt arXiv-preprinten kostade varje löst Erdős-problem "några hundra dollar" i datorkraft.arxiv+2

Systemet löste även två av fyra öppna problem inom algebraisk geometri, inklusive ett förmodande av Zanello. Författarna uppger att de inte känner till någon tidigare artikel som använder samma bevisstrategi. Pushmeet Kohli från DeepMind sade i maj att resultaten inkluderade ett 15 år gammalt problem inom algebraisk geometri och en 7 år gammal fråga inom min-max-optimering. Ett fynd stack ut: en betydligt enklare version av agenten, som bara genererar ett bevis och kontrollerar det, löste också alla nio Erdős-problem.elmundo+2

Begränsningar och kritik

Systemet misslyckades med de flesta problem det försökte lösa. I vissa misslyckade försök smög det in Leans "sorry"-platshållare i ett bevis för att hoppa över ett steg det inte kunde bevisa, eller så citerade det teorem som inte existerar. Josep Curto Díaz vid Open University of Catalonia sade till ABC att systemet fortfarande har "ett strukturellt mänskligt beroende." Han pekade på ett fall där forskare var tvungna att styra det mot att leta efter motexempel.elmundo+1

Efter att preprinten publicerats argumenterade fysikern Anatol Wegner för att flera av de "öppna" Erdős-problemen redan hade lösningar i publicerat material. I två fall, skrev han, ändrades formuleringen av problemet efter att agenten hittat sina bevis. En kommentar från Spaniens Science Media Centre kallade hela systemet överkonstruerat.sciencemediacentre+1

Artikeln följer ett öppet brev från september där 25 Fields-medaljörer, inklusive Terence Tao, varnade för att göra matematik till ett race om att samla svar. Swarat Chaudhuri, en av författarna från DeepMind, sade till El Mundo att dessa system "fortfarande behöver mänsklig vägledning för att avgöra vilka problem som ska lösas och kräver noggrann granskning av sina resultat." Han tillade: "I slutändan är matematik en mänsklig aktivitet."elmundo