Pred niekoľkými rokmi ChatGPT začal džavotať, Google vyvinul veľmi odlišný druh umela inteligencia program s názvom AlphaGo ktorí sa naučili hrať stolovú hru Go s nadľudskými schopnosťami prostredníctvom neúnavného cvičenia.
Výskumníci zo spoločnosti teraz zverejnili výskum, ktorý kombinuje schopnosti veľkého jazykového modelu (AI za dnešnými chatbotmi) so schopnosťami AlphaZero, nástupcu AlphaGo, ktorý je tiež schopný hrať šach, aby vyriešil veľmi zložité matematické dôkazy.
Ich nový frankensteinovský výtvor s názvom AlphaProof preukázal svoju zdatnosť riešením niekoľkých problémov od roku 2024. Medzinárodná matematická olympiáda (IMO), prestížna súťaž pre stredoškolákov.
AlphaProof používa model veľkého jazyka Gemini na konverziu prirodzene formulovaných matematických otázok do programovacieho jazyka tzv Lean. Toto poskytuje trénovaciu potravu pre druhý algoritmus, ktorý sa pomocou pokusov a omylov naučí, ako nájsť dôkazy, ktoré možno potvrdiť ako správne.
Začiatkom tohto roka Google DeepMind odhalil ďalší matematický algoritmus s názvom AlphaGeometry, ktorý tiež kombinuje jazykový model s odlišným prístupom AI. AlphaGeometry používa Gemini na prevod geometrických problémov do formy, s ktorou možno manipulovať a testovať ju program, ktorý spracováva geometrické prvky. Google dnes tiež oznámil novú a vylepšenú verziu AlphaGeometry.
Výskumníci zistili, že ich dva matematické programy by mohli poskytnúť dôkazy pre hádanky IMO rovnako ako strieborný medailista. Z celkového počtu šiestich problémov AlphaProof vyriešil dva problémy algebry a jednu teóriu čísel, zatiaľ čo AlphaGeometry vyriešil problém s geometriou. Programy zaznamenali jeden problém v priebehu niekoľkých minút, ale trvalo niekoľko dní, kým prišli na iné. Google DeepMind nezverejnil, koľko počítačového výkonu spôsobilo problémy.
Google DeepMind nazýva prístup použitý pre AlphaProof a AlphaGeometry „neuro-symbolický“, pretože kombinuje čisté strojové učenie umelá neurónová sieťtechnológia, ktorá v poslednej dobe podporuje najväčší pokrok v AI, s jazykom konvenčného programovania.
„Videli sme tu, že môžete spojiť prístup, ktorý bol taký úspešný, a veci ako AlphaGo, s veľkými jazykovými modelmi a vytvoriť niečo, čo je mimoriadne schopné,“ hovorí David Silver, výskumník Google DeepMind, ktorý viedol prácu na AlphaZero. Silver hovorí, že techniky demonštrované pomocou AlphaProof by sa teoreticky mali rozšíriť aj do iných oblastí matematiky.
Výskum skutočne zvyšuje vyhliadky na riešenie najhorších tendencií veľkých jazykových modelov uplatňovaním logiky a uvažovania uzemnenejším spôsobom. Akokoľvek zázračné môžu byť veľké jazykové modely, často sa snažia pochopiť čo i len základnú matematiku alebo logicky uvažovať o problémoch.
Neurónovo-symbolická metóda by mohla v budúcnosti poskytnúť systémom AI prostriedky na premenu otázok alebo úloh do formy, ktorú možno zdôvodniť spôsobom, ktorý prináša spoľahlivé výsledky. O OpenAI sa tiež hovorí, že pracuje na takomto systéme, s kódovým názvom „Jahoda“.
Dnes však odhalené systémy majú jedno kľúčové obmedzenie, ako priznáva Silver. Matematické riešenia sú správne alebo nesprávne, čo umožňuje AlphaProof a AlphaGeometry dopracovať sa k správnej odpovedi. Mnoho problémov v reálnom svete – napríklad vymyslenie ideálneho itinerára výletu – má veľa možných riešení a môže byť nejasné, ktoré z nich je ideálne. Silver hovorí, že riešením na nejednoznačnejšie otázky môže byť jazykový model, ktorý sa počas školenia pokúsi určiť, čo predstavuje „správnu“ odpoveď. „Existuje spektrum rôznych vecí, ktoré možno vyskúšať,“ hovorí.
Silver je tiež opatrný, aby poznamenal, že Google DeepMind nezradí ľudských matematikov o prácu. „Naším cieľom je poskytnúť systém, ktorý dokáže čokoľvek, ale to nie je koniec toho, čo robia matematici,“ hovorí. „Veľkou časťou matematiky je klásť problémy a hľadať zaujímavé otázky, ktoré je potrebné položiť. Môžete si to predstaviť ako ďalší nástroj v štýle posuvného pravítka, kalkulačky alebo výpočtových nástrojov.“
Aktualizované 25.7.24 13:25 ET: Tento príbeh bol aktualizovaný, aby objasnil, koľko problémov AlphaProof a AlphaGeometry vyriešili a akého typu.