Az Anthropic AI-szörny 11 nap alatt formalizálta Fermat tételét
Az Anthropic tucatnyi Claude-ügynöke 11 nap alatt 13 millió sornyi Lean kódot írt, és 30 300 köztes tételt bizonyított be, hogy végül egy teljes, számítógép által ellenőrzött bizonyítást hozzanak Pierre de Fermat 1637 körüli sejtésére.
Kevin Buzzard, az Imperial College London matematikusa, aki a sejtés formalizálására irányuló közösségi erőfeszítést vezeti, maga fordította le az Anthropic kódját és futtatta le a szokásos ellenőrző eszközt. Buzzard szerint az eredmény nem hoz új matematikai ismeretet, de demonstrálja az AI képességét a több ezer oldalnyi szakirodalom end-to-end feldolgozására mindössze 11 nap alatt. (TNW)
Buzzard, akinek ötéves, 1 millió font értékű EPSRC-s kutatási támogatása van a projektre, megjegyezte, hogy az Anthropic 11 napos munkája valószínűleg jelentős költségekkel járt. Az Anthropic becslései szerint a folyamat körülbelül hat milliárd kimeneti tokent használt fel, ami a listaáron számolva mintegy 300 000 dollárnak felel meg. Ez egy belső kutatási modell, amely nagyjából a Claude Fable 5.1-hez hasonlítható, és bár a tényleges költség ennél alacsonyabb lehet, ez az egyetlen publikusan elérhető pénzügyi adat.
Az első kísérlet kudarca és a Prove2Me szerepe
Az Anthropic őszintén beszámolt arról, hogy az első kísérlet kudarcba fulladt. Az ügynökök kezdetben haladtak, de elvesztették a projekt állapotának nyomon követését, és abbahagyták az együttműködést. A sikertelen futások is hozzájárultak a végső bizonyítás nem-boilerplate sorainak mintegy 7%-ához.
A probléma megoldását nem egy jobb modell hozta el, hanem a Prove2Me platform, amelyet Tianyi Peng, az Anthropic kutatója fejlesztett ki a Columbia Egyetem munkatársaival. A Prove2Me fenntart egy tételszámokból álló gráfot, így az ügynökök láthatják, mit kell következőként megkísérelniük, és felgyorsítja a fordítási folyamatot a tételek és bizonyítások külön fájlokba bontásával.
Az emberi beavatkozás és a kód minősége
Az ügynököknek adott emberi utasítások rendkívül rövidek voltak, mindössze két mondatból álltak, például: „Jacobian sémaként magas prioritásúnak tűnik.” és „Nyomjuk Mazurt, hogy legyen meg hamar.” A bizonyítás a Wiles-érvelés 1995-ös, Darmon, Diamond és Taylor által publikált expozícióját követi, és csak a Lean három standard axiómáját használja. Buzzard ellenőrizte a kódot, és megállapította, hogy az nem tartalmazott csalást, és a Lean verziója nem mutatott hangolási problémákat. Az OpenAI modelljei is átnézték a Lean kódját, és nem találtak hangolási problémákat a használt verzióban.
A szűk keresztmetszet eltolódott
A 13 millió sornyi kód jelenleg nem léphet be a Mathlib-be, a közösség matematikai könyvtárába, mivel a könyvtár jelenleg nem fogad el AI által generált ellenőrzéseket, és a legtöbb ilyen benyújtás gyenge minőségű. A Mathlib-ben már mintegy 3000 nyitott pull request van, amelyek közül több mint 600 aktív a felülvizsgálati sorban. Ez azt jelenti, hogy a szűk keresztmetszet az írásról az olvasásra tolódott el.
Buzzard továbbra is dolgozik a projektjén, amelynek keretében alapvető számelméleti tételeket kell benyújtania a Mathlib-be, és létre kell hoznia egy dokumentumot, amely lehetővé teszi az emberek számára a modern bizonyítások feltárását. Kétkedik abban, hogy az Anthropic elvégzi-e ezt a második feladatot. A három kutató, akik személyes Claude-előfizetéssel a Vinogradov-féle Három Prímszám Tételét formalizálták három nap alatt, szintén a közelmúltbeli AI-s matematikai áttörések közé tartozik.