Направи дарение на училище!

Досега компютрите са се проваляли с решаването на сложни математически проблеми. Въпреки това изкуственият интелект на Google AlphaGeometry успешно се справи с доказването на десетки теореми от Международната олимпиада по математика (IMO). 

Международната олимпиада по математика е може би едно от най-престижните състезания на гимназиално ниво. Всяка година ученици от цял свят се състезават за заветните златни, сребърни и бронзови медали. Скоро обаче те може да се изправят не само помежду си, но и срещу изкуствен интелект. 

През януари екип, ръководен от Trieu H. Trinh от Google DeepMind и Нюйоркския университет разкриха работата си по нова програма, наречена AlphaGeometry в научнопопулярното списание Nature. Изследователите в областта съобщиха, че програмата им е успяла да реши 25 от общо 30 геометрични задачи от минали издания на олимпиадата – успех, достиган само от златни медалисти. Програмата бе и способна да намери по-общо решение на задача от изданието на Олимпиадата през 2004, която дълго време бе убягвала на експерти и специалисти в областта. 

Разбери повече за БГ Наука:

***

В продължение на два дни участниците на състезанието трябва да решат общо 6 задачи от различни сфери на математиката. Някои от тях са толкова сложни, че дори експерти не могат да се справят с тях. Те имат кратки и елеганти решения, за които обаче се изискват големи нива на креативност и творческо мислене. Именно поради тази причина са от огромен интерес за учените, работещи с изкуствен интелект. 

Да успееш да преведеш математическо доказателство на програмен език, който да бъде разбран от компютъра не е никак лесна работа. Има специално разработени формални езици, създадени именно за работа с геометрия, но са ограничаващи, защото не използват методи от други сфери на математиката. Ако в доказателството на задачата се изисква междинна стъпка, която използва например, комплексни числа, такива програмни езици не могат да бъдат използвани. 

За да намери решение на този проблем, Trinh и екипът му създават специална база данни, която не се нуждае от преминаването на човешките математически доказателства към формален език. Техният алгоритъм първо задава „условия“ или начални опорни точки – например, триъгълник с начертани измервания и допълнителни точки, маркирани по страните му. Чрез дедуктивен алгоритъм по-късно, учените успяват да изведат допълнителни свойства за този триъгълник, като например кои страни са перпендикулярни една на друга или кои ъгли се допълват. С комбинирането на условните начални точки и по-късно извлечените от тях свойства се създава база данни от теореми и прилежащите им доказателства. Нека вземем за пример по-конкретен проблем, а именно доказване на някои от свойствата на триъгълник – два ъгъла, които са равни. Решението, което отговаря на този проблем би се състояло от стъпките, които водят дедуктивния алгоритъм към него. 

Въпреки тези впечатляващи умения, за да може AlphaGeometry да решава задачи на нивото на олимпиец, трябва да усвои и други тактики.
„Най-важното липсващо звено е генерирането на нови условия на доказателства“, пишат Trinh и екипът му в публикацията си. Например, за да може да се докаже нещо за триъгълник, може да се наложи да се въведат нови точки и линии, не задължително използвани в първоначалната формулировка на условието. Именно това е нещо, което големите езикови модели (от анг. Large Language Models, LLMs) са създадени да правят.

Тези модели са способни да генерират текстове като пресмятат вероятността, с която една дума би се намирала след друга в последователността на писмената реч. Точно по подобен начин Trinh и екипът му са способни да тренират AlphaGeometry чрез база данни от теореми и доказателства. LLM-ите не се научават на дедуктивните стъпки, които съставят решаването на даден проблем, тази работа все още се върши от други алгоритми. Вместо това ИИ моделът се концентрира върху това да намира точки, линии и други обекти, които биха били полезни в решаването на определен проблем. 

Първото нещо, което прави AlphaGeometry при решаването на дадена задача, е да извлече списък с всички неща, дадени в условието. Ако съответното становище, което трябва да бъде доказано, не фигурира в този списък, ИИ се намесва. Може да добави нова точка Х към триъгълника АВС така, че АВСХ да представлява паралелограма – нещо, което програмата знае как да прави от предишни тренирания. По този начин дедуктивният алгоритъм бива снабдяван с нова информация от изкуствения интелект. Този процес се повтаря, докато ИИ или алгоритъмът достигнат до желаното заключение. „Методът звучи подобавашо и напомня начинът, по който се тренират самите участници в олимпиадата“, съобщава Питър Шолци, носител на Филдсовата награда и бивш трикратен златен медалист на Международната олимпиада по математика.

За да тестват изобретението си, учените избират 30 геометрични задачи, появявали се във формата на състезанието от 2000-та година насам. Програмата, която бе използвана преди в решаването на такива проблеми, наречена Wu’s algorithm, успява да реши едва 10, докато друг известен LLM, GPT-4, се проваля на всеки един от тях. За сметка на това AlphaGeometry се справя успешно с 25 задачи. Според учените ИИ се справя по-добре от повечето състезатели на Олимпиадата, които успяват да решат средно по 12.5 задачи от 30 (златните медалисти обикновено решават правилно по 25.9)

Когато екипът на Трин разглежда решенията на модела, те забелязват нещо много интересно. При решаването на един определен проблем, програмата не е използвала цялата предоставена информация, т.е AlphaGeometry сама се е опитала да намери решение на близка, но по-обща теорема. Също така става ясно, че с по-сложни задачи, такива, с които участниците обикновено не успяват да се справят толкова добре, изискват и по-дълги доказателства от ИИ. Машината, изглежда, се затруднява със същите неща, с които и хората.

AlphaGeometry все още не може да участва в състезанието, тъй като геометрията е едва една трета от него, но Трин и колегите му са убедени във факта, че техният подход може да бъде прилаган и към други сфери на математиката, като например комбинаторика. Кой знае, може би след някоя друга година не-човеци ще могат да се състезават наравно с нас. Може би дори биха спечелили злато?

Превод: Траяна Христова

Източник: https://www.scientificamerican.com/article/ai-matches-the-abilities-of-the-best-math-olympians/

Вземете (Доживотен) абонамент и Подарете един на училище по избор!