Nové spuštění AI Math právě prolomilo 4 dříve nevyřešené problémy

před pěti lety, matematici Dawei Chen a Quentin Gendron se pokoušeli rozmotat obtížnou oblast algebraické geometrie zahrnující diferenciály, prvky kalkulu používané k měření vzdálenosti podél zakřivených povrchů. Při práci na jedné větě narazili na nečekanou překážku: Jejich argument závisel na podivném vzorci z teorie čísel, ale nebyli schopni jej vyřešit ani zdůvodnit. Nakonec Chen a Gendron napsali práci, ve které představili svůj nápad spíše jako domněnku než jako větu.

Chen nedávno strávil hodiny pobízením ChatGPT v naději, že přiměje AI, aby přišla s řešením stále nevyřešeného problému, ale nefungovalo to. Pak, během recepce na matematické konferenci ve Washingtonu, minulý měsíc, Chen narazil na Ken Ono, známého matematika, který nedávno opustil svou práci na University of Virginia, aby se připojil k Axiomu, startupu s umělou inteligencí, který spoluzaložila jedna z jeho svěřenkyň, Carina Hong.

Chen řekl Onovi o problému a následujícího rána mu Ono předložil důkaz, laskavost jeho startupové umělé inteligence, která řeší matematiku, AxiomProver. „Potom vše přirozeně zapadlo,“ říká Chen, který spolupracoval s Axiomem na sepsání důkazu, který byl nyní umístěn na arXiv, veřejné úložiště akademických prací.

Nástroj umělé inteligence společnosti Axiom našel souvislost mezi problémem a numerickým jevem, který byl poprvé studován v 19. století. Následně vymyslela důkaz, který si sama užitečně ověřila. „To, co AxiomProver našel, bylo něco, co všichni lidé minuli,“ říká Ono WIRED.

Důkazem je jedno z několika řešení nevyřešených matematických problémů, se kterými Axiom podle svých slov přišel v posledních týdnech. Umělá inteligence zatím nevyřešila žádný z nejslavnějších (nebo lukrativních) problémů v oblasti matematiky, ale našla odpovědi na otázky, které už roky lámou hlavu odborníkům v různých oblastech. Důkazy jsou důkazem neustále se rozvíjejících matematických schopností AI. V posledních měsících jiní matematici hlásili, že používají nástroje AI ke zkoumání nových nápadů a řešení stávajících problémů.

Techniky vyvinuté Axiomem se mohou ukázat jako užitečné mimo svět pokročilé matematiky. Stejné přístupy lze například použít k vývoji softwaru, který je odolnější vůči určitým druhům kybernetických útoků. To by zahrnovalo použití AI k ověření, že kód je prokazatelně spolehlivý a důvěryhodný.

„Matematika je skutečně skvělým testovacím polem a pískovištěm reality,“ říká Hong, generální ředitel společnosti Axiom. „Věříme, že existuje mnoho velmi důležitých případů použití s ​​vysokou komerční hodnotou.“

Přístup společnosti Axiom zahrnuje kombinaci velkých jazykových modelů s proprietárním systémem umělé inteligence zvaným AxiomProver, který je trénován tak, aby uvažoval prostřednictvím matematických problémů, aby dosáhl řešení, která jsou prokazatelně správná. V roce 2024 předvedl Google podobný nápad se systémem s názvem AlphaProof. Hong říká, že AxiomSolver zahrnuje několik významných pokroků a novějších technik.

Ono říká, že důkaz vytvořený umělou inteligencí pro domněnku Chen-Gendron ukazuje, jak může umělá inteligence nyní smysluplně pomáhat profesionálním matematikům. „Toto je nové paradigma pro dokazování teorémů,“ říká.

Systém Axiom je více než jen běžný model umělé inteligence, protože je schopen ověřovat důkazy pomocí specializovaného matematického jazyka zvaného Lean. Spíše než jen prohledávat literaturu to AxiomProveru umožňuje vyvinout skutečně nové způsoby řešení problémů.

Další z nových důkazů generovaných AxiomProver ukazuje, jak je umělá inteligence schopna řešit matematické problémy zcela sama. Tento důkaz, který byl také popsán v článku zveřejněném na arXiv, poskytuje řešení Felovy domněnky, která se týká syzygie neboli matematických výrazů, kde se čísla v algebře řadí do řady. Pozoruhodné je, že tato domněnka zahrnuje vzorce, které byly poprvé nalezeny v zápisníku legendárního indického matematika Srinivasy Ramanujana před více než 100 lety. V tomto případě AxiomProver nejenom doplnil chybějící dílek skládačky, ale vymyslel důkaz od začátku do konce.