Kineski znanstvenici sa Sveučilišta u Pekingu razvili su sustav umjetne inteligencije koji je bez ljudske intervencije riješio matematički problem star više od deset godina, što predstavlja značajan iskorak u primjeni umjetne inteligencije u znanstvenim istraživanjima
Kako ističu u svom radu, pripremljenom za objavu, riječ je o problemu koji je 2014. godine postavio američki matematičar sa Sveučilišta Iowa, Dan Anderson, a postao je poznat kao Andersonova pretpostavka. Problem proizlazi iz područja komutativne algebre, a do sada nije imao potpuno razjašnjen dokaz. Novi sustav uspio je u svega nekoliko sati doći do rješenja i pritom generirati formalni matematički dokaz.
Sustav se temelji na kombinaciji više modela umjetne inteligencije, a ključnu ulogu imaju dva povezana AI agenta: jedan generira ideje i matematičke hipoteze na temelju dostupne literature (Rethlas) dok drugi provodi strogu formalnu provjeru i potvrđuje točnost dokaza (Archon).
vezane vijesti
Za razliku od ranijih pristupa, koji su se oslanjali na ljudsko vođenje ili ograničene zadatke, ovaj sustav može samostalno formulirati problem, razviti rješenje i verificirati ga bez dodatne intervencije istraživača.
'Rethlas oponaša tijek rada matematičara kombinirajući njihove zaključke s našim tražilicom teorema, Matlas, da bi istražio strategije rješenja i konstruirao kandidate za dokaze. Archon, opremljen našom formalnom tražilicom teorema LeanSearch, prevodi neformalne argumente u formalizirane projekte u Leanu 4 putem strukturirane dekompozicije zadataka, iterativnog usavršavanja i automatizirane sinteze dokaza, osiguravajući strojno provjerljivu ispravnost. Koristeći ovaj okvir, automatski rješavamo otvoreni problem u komutativnoj algebri i formalno provjeravamo dokaz u Leanu 4 bez ikakvog ljudskog sudjelovanja', pojasnili su u radu kineski znanstvenici.
Rezultati su objavljeni na platformi arXiv i zasad nisu prošli stručnu recenziju, što znači da će ih znanstvena zajednica još trebati provjeriti. Unatoč tome, istraživači ističu da ovaj primjer pokazuje potencijal umjetne inteligencije za rješavanje i automatizaciju složenih znanstvenih zadataka.
Razvoj velikih jezičnih modela i sustava za formalno dokazivanje posljednjih godina znatno je napredovao, pa umjetna inteligencija sve češće prelazi s rješavanja školskih zadataka na probleme istraživačke razine. Ovaj slučaj potvrđuje trend sve veće njezine uloge u matematici i drugim znanstvenim disciplinama.
