ИИ постигна огромен успех на Международната олимпиада по математика: AlphaProof за първи път спечели сребърен медал

Машина, която сама търси и поправя своите грешки.

На Международната олимпиада по математика 2025 г. се случи необичаен случай: сред решенията, класирани на ниво сребърен медал, не беше човешко решение, а произведение, създадено от изкуствен интелект. Преди това нито една система с изкуствен интелект не беше демонстрирала на олимпиада резултат, сравним с нивото на силните ученици, които традиционно доминират на подобни състезания.

Тази система носи името AlphaProof – разработка на Google DeepMind, предназначена за решаване на математически задачи под формата на строги формални доказателства. Само по себе си нейното издигане до нивото на международната олимпиада вече беше впечатляващо, но много по-важна е способността на програмата да открива собствените си грешки и да ги поправя. Конвенционалните големи езикови модели наистина могат да решават уравнения и логически задачи, но техните заключения често съдържат фини грешки: формулировката изглежда убедителна, но се разпада при проверка.

Подходът на AlphaProof е коренно различен. Всяка стъпка от разсъжденията се подлага на формална проверка в средата Lean – специализирана система, разработена в Microsoft Research и предназначена за строга проверка на математически доказателства. Lean приема само напълно правилни вериги от разсъждения, така че AlphaProof не се ограничава до генериране на чист текст, а създава доказателство, потвърдено от формалната логика.

Създаването на подобна система изискваше три етапа на подготовка. Първо, AlphaProof е обучена върху масив от около 300 милиарда лексеми, включително програмен код, материали за обучение и научни текстове. Това е дало на модела основни познания за логическите структури, формалния език и принципите за конструиране на доказателства. След това изследователите са заредили в системата 300 000 готови доказателства, предварително форматирани в Lean. Те отразявали стила на мислене на професионалните математици и служели като отправна точка за по-нататъшно обучение.

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

За най-сложните проблеми екипът добавя допълнителен инструмент – Test-Time Reinforcement Learning (TTRL). Тази схема създава много опростени версии на първоначалния проблем, които системата решава една по една, събирайки полезни логически модели. След това AlphaProof прехвърля изработените стратегии към оригиналната, много по-трудна задача.

Авторите на изследването отбелязват, че количеството натрупан опит е позволило на системата да създава сложни, разработени вериги от разсъждения и да доказва твърдения, които преди това са били достъпни само за специалисти. Потенциалът на технологията не се ограничава само до олимпиадите: AlphaProof може да помогне при проверката на математически текстове, откриването на грешки и дори при разработването на нови теоретични идеи.