AI v matematických súťažiach: DeepSeek vs ChatGPT

V posledných rokoch sme svedkami toho, ako umelá inteligencia dokáže riešiť
zložité matematické problémy, ktoré boli kedysi výlučne doménou ľudí.
Medzi najdiskutovanejšie modely v tejto oblasti patria
DeepSeek-Math-V2 a ChatGPT-4,
ktoré boli testované na viacerých prestížnych matematických súťažiach
a benchmarkoch.

Výkony na olympiádach a súťažiach

DeepSeek-Math-V2 je špecializovaný model optimalizovaný na matematické riešenia
a formálne dôkazy. Naproti tomu ChatGPT-4 je všeobecný jazykový model,
ktorý zvláda široké spektrum úloh, no pri náročných matematických dôkazoch
a kreatívnych úlohách má prirodzené obmedzenia.

Tabuľka výsledkov

Interpretácia:
DeepSeek-Math-V2 dosahuje vo viacerých prípadoch výkony porovnateľné
s úrovňou gold-medal level.
ChatGPT-4 podáva priemerný až nadpriemerný výkon,
pričom jeho silnou stránkou je všeobecné uvažovanie a flexibilita,
nie striktne formálne matematické dôkazy.

Budúcnosť: dominancia AI v matematike?

Na základe súčasného vývoja možno realisticky očakávať,
že v horizonte približne nasledujúcich 10 rokov
budú veľké jazykové modely (LLM) schopné riešiť väčšinu matematických problémov.
S rastúcim výpočtovým výkonom, lepšou integráciou
formálnych dôkazových systémov a kvalitnejšími tréningovými dátami
budú AI modely spoľahlivo zvládať aj komplexné dôkazy.

Prečo je LISP vhodný pre matematickú AI?

Zaujímavou a odborne dôležitou úvahou je,
že vývoj špecializovaných systémov na riešenie matematických problémov
by sa mohol výrazne posunúť dopredu,
ak by symbolická a dôkazová vrstva bola implementovaná
v jazykoch typu LISP.

LISP je historicky a konceptuálne prispôsobený manipulácii so symbolickými výrazmi,
rekurziou a stromovými štruktúrami – základnými nástrojmi pre formálne
matematické dôkazy. Mnohé automatické dokazovacie systémy a symbolické
algebraické systémy boli vyvíjané práve v LISPe alebo jeho odnožiach.

Tento jazyk nie je magicky „najlepší“ na svete,
ale je obzvlášť vhodný pre implementáciu matematických algoritmov
a dôkazových procesov. Kombinácia LLM a LISP-like symbolickej vrstvy
by mohla priniesť kvalitatívny skok v schopnostiach AI riešiť
komplexné matematické úlohy. Ide o niečo také ako „Tool enhanced LLM“.

Tip pre čitateľa: Sledujte vývoj LLM v matematike

• Oficiálne benchmarky a súťaže: IMO, CMO, Putnam, AMC/AIME – často sa objavujú štúdie s AI riešeniami úloh.
• Výskumné články: ArXiv.org obsahuje publikácie o matematických LLM, symbolických dôkazových systémoch a ich kombinácii.
• GitHub projekty: Open-source projekty ako DeepSeek-Math, MiniF2F, Lean prover experimenty – umožňujú sledovať konkrétne výsledky a kód.
• Technologické blogy a mediálne správy: Sledujte vývoj OpenAI, DeepMind a ďalších, kde sa objavujú praktické ukážky riešenia zložitých matematických problémov.
• Vzdelávacie kurzy: Kurzy o symbolickej matematike, LISP, theorem proving alebo AI for mathematics vám umožnia lepšie pochopiť fungovanie týchto systémov.

Celkové vyhodnotenie:

• DeepSeek-Math-V2 demonštruje, že špecializované AI modely už dnes dosahujú
  výkony porovnateľné so špičkovými ľudskými riešiteľmi.
• ChatGPT-4 dosahuje slušné výsledky, no pri zložitých dôkazoch
  zaostáva za špecializovanými matematickými modelmi.
• Budúcnosť matematiky asi nebude patriť výlučne ľuďom ani výlučne AI,
  ale ich úzkej spolupráci, kde AI bude dominantným nástrojom
  a človek nositeľom významu, intuície a smerovania.