Изкуственият интелект на Google реши проблеми, които измъчваха поколения математици

Изкуственият интелект все по-уверено навлиза в сфера, в която преди години работеха само математици. Системата AlphaProof Nexus на Google DeepMind реши девет нерешени задачи на унгарския математик Пал Ердьош, като две от тях оставаха без отговор в продължение на 56 години.

AlphaProof Nexus не просто предложи красиви идеи, а подготви доказателства, които могат да бъдат проверени машинно. За проверката системата използва Lean – специална среда, в която всеки логически ход трябва да премине строг контрол. Ако доказателството не издържи проверката, системата се връща и търси отново.

Според данни на Google DeepMind, системата AlphaProof Nexus е работила с набор от 353 нерешени задачи на Ердьош и е решила 9 от тях. Задачите се отнасят до комбинаториката и теорията на графите. Освен това системата е доказала 44 нерешени хипотези от „Онлайн енциклопедията на целочислените последователности“. Стойността на решаването на всяка задача възлиза на няколкостотин долара, според оценката на авторите на работата.

Системата съчетава голям езиков модел и строга проверка на доказателствата. Моделът предлага ход на решението, а Lean проверява дали заключението следва от предходните стъпки. Такъв подход намалява риска изкуственият интелект да даде правдоподобен, но неправилен отговор.

Резултатът на Google DeepMind се появи скоро след обявяването от OpenAI на собствен пробив в задачата на Ердьош, формулирана през 1946 година. AI моделът на OpenAI намери нов подход към задачата за точките на равнината и разстоянията между тях. Няколко математици вече определиха резултата като сериозно постижение, въпреки че работата с такива доказателства все пак изисква проверка и обсъждане в професионалната общност.

AlphaProof Nexus все още е далеч от универсалния „математик в компютъра“. Повечето задачи от проверения набор останаха нерешени, а там, където се изискваха принципно нови математически конструкции, системата често не се справяше. Но самият факт, че програмата успя да реши задачи, които десетилетия наред не се поддавали на хората, показва колко бързо се променя ролята на изкуствения интелект в науката. За математиката такъв подход може да се окаже особено важен. Изкуственият интелект е способен бързо да пресява идеи, а формалната проверка отсява погрешните разсъждения. Заедно двата механизма превръщат системата не просто в помощник за изчисления, а в инструмент за търсене на нови доказателства.