Tio problem, 4 802 sidor svar
Ramanujan Challenge lade ut tio talteoretiska problem på forskningsnivå offentligt. Åtta hade bevisats av arrangörerna men aldrig publicerats, vilket håller dem utanför varje träningsmängd; två var öppna förmodanden. Varje problem var en konkret formel för en matematisk konstant, så riktigheten kunde kontrolleras numeriskt även där beviset krävde icke-självklar matematik.
Deltagarna skickade in 228 bidrag. Tillsammans innehöll de 4 802 sidor bevis på naturligt språk och 1 079 380 rader kod i Lean, Python, Mathematica och Sage. Resultatartikeln, publicerad den 29 oktober av gruppen Ramanujan Machine vid Technion i Haifa med medförfattare vid universitetet i Gent, Research Institute for Symbolic Computation i Linz och Toronto Metropolitan University, handlar lika mycket om att läsa den högen som om vad som finns i den.
Vilka som löste dem
De bidrag som producerade korrekta bevis på naturligt språk använde oftast modeller ur Claude- och GPT-familjerna. Bidrag som kombinerade Lean med ett datoralgebrasystem slog dem som förlitade sig på ett enda verktyg, vilket författarna läser som en vinst av diversifierat stödmaterial snarare än som någon enskild bevisares förtjänst.
Ett av de två publicerade öppna förmodandena fick flera korrekta bevis. Några av de kompletta bevisen kom från amatörmatematiker. En inlämnare hade ingen högre matematisk utbildning, och lösningen till ett av problemen visade sig vara enklare än arrangörernas egen. En gymnasieelev kom betydande steg mot att bevisa en av förmodandena.
Det är resultatet som är värt att skilja från riktmärkets poäng. Utmaningen konstruerades för att mäta modeller, och vad den mätte var en förändring i vilka som alls kan nå talteori på forskningsnivå.
Det andra problemet utmaningen skapade
Att bedöma bidragen visade sig vara den svårare uppgiften. Författarna beskriver en boom i AI-assisterad matematik som producerar “en lavin av matematiska påståenden”, ett problem som sträcker sig långt utanför deras eget riktmärke: 4 802 sidor kan inte granskas som tio artiklar kan.
Befintliga riktmärken hanterar detta på olika sätt — en enda språkmodell som domare, en modell som kontrollerar likvärdighet mot känd sanning, eller deterministisk kod som verifierar en modells svar. Teamet byggde i stället en AI-assisterad kedja som bedömer semantisk och logisk riktighet i alla tre inlämningsformaten: naturligt språk, datoralgebrakod och Lean-formaliseringar.
Mot konventionell bedömning med en språkmodell i ett svep sänkte kedjan falska positiva utslag på bevis i naturligt språk från 23 % till 6 %. Bedömningens träffsäkerhet på stödjande kod gick från 46 % till 58 %.
Lästa i andra riktningen är det de siffror som betyder något. En domare i ett svep släppte igenom ungefär ett av fyra felaktiga bevis på naturligt språk, och hade rätt om stödjande kod mindre än hälften av gångerna. Varje topplista som poängsätts så rapporterar sin domare lika mycket som sina modeller.
Vad man ska bevaka
Om riktmärken för matematik på forskningsnivå publicerar sin bedömningsfelfrekvens vid sidan av poängen. De återstående 6 % är fortfarande ett falskt positivt utslag i ett bidrag av sexton, och 58 % på kod är en förbättring från en låg bas, inte ett löst problem. Arrangörerna föreslår sin metod som en metodik för att bedöma matematik på forskningsnivå i stor skala, med tillämpningar inom AI för vetenskap. Artikeln är ett preprint och inte kollegialt granskad; den ges ut under CC BY-SA 4.0.
