Jako velký skok ve vývoji umělé inteligence vyvinul výzkumný tým z Peking University systém umělé inteligence, který dokáže samostatně řešit složité, nevyřešené matematické problémy. Systém úspěšně vyřešil deset let starou algebraickou domněnku, což znamenalo přechod od používání umělé inteligence jako pouhého pomocníka k její roli autonomního výzkumníka.
Řešení algebraické hypotézy
V centru tohoto průlomu byla algebraická domněnka, kterou poprvé navrhl v roce 2014 zesnulý Dan Anderson, bývalý profesor na University of Iowa. Po deset let zůstával tento problém otevřenou výzvou v oblasti komutativní algebry.
Na rozdíl od předchozích modelů umělé inteligence, které vyžadovaly neustálé lidské vedení, tento nový systém zpracoval desetiletí matematické literatury k vyřešení hypotézy a – kriticky – autonomně ověřil její výsledky bez lidského zásahu. Celý proces trval pouze 80 hodin práce.
Architektura autonomie: Rethlas a Archon
Aby vědci překonali tradiční omezení AI v matematice, ustoupili od standardních velkých jazykových modelů (LLM), které jsou často náchylné k „halucinacím“ nebo logickým chybám. Místo toho vytvořili rámec pro dva agenty navržený tak, aby napodoboval přísný pracovní postup profesionálních matematiků:
- Reasoning Agent (Rethlas): Tento systém funguje jako „myslitel“. Používá teorémový vyhledávač nazvaný Matlas ke zkoumání různých strategií a matematických způsobů řešení problému.
- Formalizační agent (Archon): Jakmile je nalezen potenciální důkaz, řízení přechází na Archona. Pomocí nástroje LeanSearch převádí neformální úvahy do formálního, strojově ověřitelného formátu.
- Verifier (Lean 4): Systém využívá Lean 4 – specializovaný programovací jazyk a interaktivního pomocníka pro dokazování teorémů – aby bylo zajištěno, že důkaz je matematicky správný a bezchybný.
Proč na tom záleží: od asistence po automatizaci
Současné trendy v AI ukazují silný vektor pro trénovací modely v matematice, ale většina stále čelí „problému přísnosti“. Zatímco lidé jsou schopni psát důkazy, mohou dělat chyby; zatímco LLM mohou generovat text rychle, často jim chybí logická přesnost potřebná pro vyšší matematiku.
Výzkum Pekingské univerzity řeší tuto mezeru integrací uvažování v přirozeném jazyce s formálním ověřováním. Tento duální přístup zajišťuje, že AI pouze „neuhádne“ odpověď, ale vytvoří důkaz, jehož správnost lze matematicky ověřit.
Kromě toho výzkumníci poznamenali, že umělá inteligence prokázala jedinečnou schopnost vykonávat úkoly, které obvykle vyžadují mezioborovou spolupráci, v podstatě působí jako skupina odborníků pracujících v tandemu.
Budoucnost matematického výzkumu
I když systém fungoval autonomně, vědci poznamenali, že lidský zásah může stále sloužit jako urychlovač. Matematik, který vede archonského agenta, může urychlit proces formalizace a připravit cestu pro budoucnost, kde lidé a AI budou fungovat ve vysokorychlostním symbiotickém cyklu.
„Tato práce je konkrétním příkladem toho, jak může být matematický výzkum výrazně automatizován pomocí AI,“ uvedli vědci.
Závěr
Tato nová architektura, která kombinuje logické uvažování s přísným formálním ověřováním, posouvá umělou inteligenci za hranice jednoduchých výpočtů do oblasti autonomního vědeckého objevování. Tento průlom dláždí cestu umělé inteligenci k řešení stále složitějších problémů v matematice a dalších špičkových vědeckých oborech.
