AI od DeepMind vyřešila devět Erdősových problémů

Google DeepMind, součást společnosti Alphabet ↗ 0.89%, publikoval recenzovanou zprávu o AlphaProof Nexus, systému umělé inteligence, který vyřešil devět otevřených problémů matematika Paula Erdőse a dokázal 44 domněnek z On-Line encyklopedie celočíselných posloupností (OEIS). Článek vyšel ve čtvrtek 8. října v časopise Science. Dva z Erdősových problémů položili Erdős a András Sárközy v roce 1970 a zůstaly otevřené 56 let.elmundo+2

Studie poskytuje recenzovanou podporu výsledkům, které DeepMind poprvé zveřejnil na arXiv v květnu. Přichází v době, kdy AI laboratoře soupeří o to, aby ukázaly, že jejich systémy zvládnou matematiku na výzkumné úrovni, což je závod, který někteří přední matematici kritizovali.abc+1

Jak to funguje

Systém využívá Gemini 3.1 Pro k hledání důkazů a asistenta Lean k jejich kontrole. Lean mechanicky ověřuje každý krok a odmítá jakýkoli důkaz s mezerami, přičemž agent neustále zkouší nové strategie, často s mnoha pokusy běžícími paralelně. Tým se pokusil o 353 Erdősových problémů a 492 domněnek OEIS. Těch 44 důkazů OEIS zkontrolovali ručně a potvrdili, že problémy byly správně formalizovány a dříve nebyly dokázány. Podle preprintu na arXiv stál každý vyřešený Erdősův problém "několik stovek dolarů" ve výpočetním čase.arxiv+2

Systém také vyřešil dva ze čtyř otevřených problémů v algebraické geometrii, včetně domněnky Zanella. Autoři uvádějí, že neví o žádném dřívějším článku, který by používal stejnou strategii důkazu. Pushmeet Kohli z DeepMind v květnu řekl, že výsledky zahrnovaly 15 let starý problém algebraické geometrie a 7 let starou otázku v min-max optimalizaci. Jeden výsledek vyčníval: mnohem jednodušší verze agenta, která pouze vygeneruje důkaz a zkontroluje jej, vyřešila všech devět Erdősových problémů také.elmundo+2

Limity a kritika

Systém u většiny problémů, o které se pokusil, selhal. V některých neúspěšných pokusech vložil do důkazu zástupný symbol "sorry" systému Lean, aby přeskočil krok, který nedokázal dokázat, nebo citoval neexistující věty. Josep Curto Díaz z Katalánské otevřené univerzity pro ABC uvedl, že systém má stále "strukturální lidskou závislost". Poukázal na případ, kdy jej výzkumníci museli nasměrovat k hledání protipříkladů.elmundo+1

Poté, co preprint vyšel, fyzik Anatol Wegner argumentoval, že několik "otevřených" Erdősových problémů již mělo řešení v publikovaných pracích. Ve dvou případech napsal, že znění problému bylo změněno poté, co agent našel své důkazy. Komentář ze španělského Science Media Centre označil celý systém za překombinovaný.sciencemediacentre+1

Článek následuje po zářijovém otevřeném dopise, v němž 25 držitelů Fieldsovy medaile, včetně Terence Taa, varovalo před přeměnou matematiky v závod o hromadění odpovědí. Swarat Chaudhuri, jeden z autorů z DeepMind, řekl El Mundo, že tyto systémy "stále potřebují lidské vedení, aby rozhodly, které problémy řešit, a vyžadují pečlivou kontrolu svých výsledků." Dodal: "Matematika je v konečném důsledku lidská činnost."elmundo