Google DeepMind Эрдёшнинг тўққизта очиқ масаласини ечишга муваффақ бўлди
Google DeepMind компанияси АлпҳаProоф Нехус деб номланган янги математик фреймворкни тақдим этди. Ушбу тизим машҳур математик Паул Эрдос рўйхатидаги тўққизта очиқ масалани мустақил равишда ечишга муваффақ бўлди. Уларнинг айримлари ярим асрдан кўпроқ вақт давомида ечиmsиз қолиб келаётган эди. Шунингдек, тизим Бутун сонли кетма-кетликлар онлайн энциклопедиясидаги (ОEИС) 44 та гипотезани исботлади ва алгебраик геометриядаги 15 йиллик муаммони ҳал қилди. Бу ҳақда Ixbt.com хабар беради.
АлпҳаProоф Нехус тизимининг асосий хусусияти Gemini 3.1 Pro тил модели ва Леан расмий математик текшириш тизимининг уйғунлигидир. Оддий LLM моделларидан фарқли ўлароқ, ушбу тизим исботларни табиий тилда эмас, балки Леан дастурлаш тилида босқичма-босқич шакллантиради. Ҳар бир қадам компилятор томонидан автоматик текширилади. Агар хатолик юз берса, Леан аниқ хабар қайтаради ва модел кейинги уринишда ундан хулоса чиқаради. Бу ёндашув сунъий интеллектнинг мантиқий хатоларга йўл қўйишини (галлюцинация) олдини олади.
Тадқиқотчиларнинг сўзларига кўра, битта масалани ечиш учун сарфланган ҳисоблаш харажатлари бир неча юз долларни ташкил этган. Тизим айниқса комбинаторика, сонлар назарияси ва қабариқ оптималлаштириш каби Матлиб кутубхонаси яхши ривожланган соҳаларда юқори натижа кўрсатди. Шунга қарамай, Эрдёшнинг 353 та очиқ масаласидан ҳозирча фақат тўққизтаси ечилди, бу эса сунъий интеллект учун ҳали қилинадиган ишлар кўплигидан далолат беради.
DeepMind мутахассислари АлпҳаProоф Нехус математиклар ўрнини босмаслигини, балки янги тадқиқот воситасига айланишини таъкидламоқда. Тизим томонидан тақдим этилган барча расмий исботлар GitHub платформасида эълон қилинди. Ушбу иш OpenAI каби рақобатчиларнинг математик тадқиқотлар соҳасидаги ютуқлари фонида амалга оширилди. Масалан, аввалроқ OpenAI ўзининг реасонинг-модели ёрдамида Эрдёшнинг масофалар ҳақидаги гипотезасини рад этган эди.
