След като Google DeepMind победи хората във всичко, от Играйте Go to стратегически настолни игри,
сега твърди, че е на ръба да победи най-добрите ученици в света при решаването на математически задачи.

Базираният в Лондон Машинно обучение Компанията обяви на 25 юли, че нейните системи за изкуствен интелект (AI) са решили четири от шестте задачи, дадени на учениците на Международната олимпиада по математика (IMO) през 2024 г. в Бат, Обединеното кралство. AI предостави строги, стъпка по стъпка доказателства, оценени от двама топ математици и постигна резултат от 28/42 - само една точка от територията на златния медал.

„Това очевидно е много значителен напредък“, казва Джоузеф Майерс, математик от Кеймбридж, Обединеното кралство, който заедно с носителя на медал от Фийлдс Тим Гауърс прегледаха решенията и помогнаха за избора на оригиналните задачи за тазгодишната IMO.

DeepMind и други компании се надпреварват в крайна сметка да осигурят на машините доказателства, които имат значение Решете изследователски въпроси по математика. Проблемите, представени на IMO, водещото световно състезание за млади математици, се превърнаха в еталон за напредък към тази цел и се смятат за „голямо предизвикателство“ за машинното обучение, каза компанията.

„Това е първият път, когато AI система е постигнала представяне на ниво медал“, Pushmeet Kohli, вицепрезидент на AI в науката в DeepMind, каза на брифинг за пресата. „Това е важен крайъгълен камък в изграждането на напреднали изследователи на доказателства“, каза Коли.

Разширение

Само преди няколко месеца, през януари, системата DeepMind Постижения на ниво медал на AlphaGeometry постигнато при решаването на един тип IMO проблеми, а именно тези в евклидовата геометрия. Първият AI, който се представи на ниво златен медал на цялостния тест – включително въпроси по алгебра, комбинаторика и теория на числата, обикновено считани за по-предизвикателни от геометрията – ще отговаря на условията за получаване на награда от $5 милиона, наградата на AI ​​Mathematics Olympiad Prize (AIMO). (Наградата има строги критерии като разкриване на изходния код и работа с ограничена изчислителна мощност, което означава, че настоящите усилия на DeepMind няма да отговарят на изискванията.)

В последния си опит изследователите са използвали AlphaGeometry2, за да решат геометричния проблем за по-малко от 20 секунди; AI ​​е подобрена и по-бърза версия на тяхната система за запис, казва компютърният специалист на DeepMind Thang Luong.

За другите видове въпроси екипът разработи изцяло нова система, наречена AlphaProof. AlphaProof реши две задачи по алгебра в състезанието и една по теория на числата, което отне три дни. (Участниците в действителната IMO имат две сесии от по 4,5 часа всяка.) Не успя да реши двата проблема в комбинаториката, друга област на математиката.


Nahaufnahme einer Goldmedaille, gewonnen bei der 63. Internationalen Mathematik-Olympiade von einem rumänischen Teilnehmer.

Изследователите имат смесени резултати, когато отговарят на математически въпроси, използвайки езикови модели – вида системи, които захранват чатботове като ChatGPT. Понякога моделите дават правилния отговор, но не могат да обяснят своите разсъждения рационално, а понякога бълват глупости.

Само миналата седмица екип от изследователи от софтуерните компании Numina и HuggingFace използва езиков модел, за да спечели междинна AMIO „награда за напредък“ въз основа на опростени версии на IMO проблеми. Компаниите направиха целите си системи с отворен код и ги направиха достъпни за изтегляне от други изследователи. Но победителите казахаПриродата, че само езиковите модели вероятно няма да са достатъчни за решаване на по-трудни проблеми.

Само класа

AlphaProof съчетава езиков модел с технология за обучение с подсилване, която използва двигателя „AlphaZero“, който компанията успешно използва за атакуващи игри като Go и някои специфични математически задачи използвани. При обучението с подсилване, невронната мрежа се учи чрез проба и грешка. Това работи добре, когато неговите отговори могат да бъдат оценени с помощта на обективен стандарт. За тази цел AlphaProof беше обучен да чете и пише доказателства на формален език, наречен Lean, който се използва в софтуерния пакет „Proof Assistant“ със същото име, популярен сред математиците. За да направи това, AlphaProof тества дали неговите изходи са правилни, като ги стартира в пакета Lean, което помогна за попълването на някои от стъпките в кода.

Обучението на езиков модел изисква огромно количество данни, но в Lean имаше малко математически доказателства. За да преодолее този проблем, екипът разработи допълнителна мрежа, която се опита да преведе съществуващ запис от милион проблеми, написани на естествен език, но без решения, написани от хора, в Lean, казва Томас Хюбърт, изследовател на DeepMind за машинно обучение, който ръководи разработването на AlphaProof. „Нашият подход беше, можем ли да се научим да доказваме, дори ако първоначално не сме тренирали върху писмени доказателства?“ (Компанията възприе подобен подход към Go, където нейният AI се научи да играе играта, като играеше срещу себе си, а не от начина, по който хората го правят.)

Магически ключове

Много от Lean преводите нямаха смисъл, но достатъчно бяха достатъчно добри, за да доведат AlphaProof до точката, в която може да започне своите цикли на обучение за укрепване. Резултатите са много по-добри от очакваното, каза Гауърс на брифинга за пресата. „Много проблеми в IMO имат това свойство на магически ключ. Проблемът изглежда труден в началото, докато не намерите магически ключ, който го отваря“, каза Гауърс, който работи в Collège de France в Париж.

В някои случаи изглеждаше, че AlphaProof успява да осигури тази допълнителна стъпка на креативност, като предоставя една правилна стъпка от безкрайно голямо възможно решение. Но е необходим допълнителен анализ, за ​​да се определи дали отговорите са по-малко изненадващи, отколкото изглеждат, добави Гауърс. Подобен дискурс се появи след изненадващото "Влак 37", ботът на DeepMinds AlphaGo при него знаменита победа за 2016 г. над най-добрия играч на Go в света направени – повратна точка за AI.

Остава да се види дали техниките могат да бъдат усъвършенствани, за да работят на изследователско ниво в математиката, каза Майърс на брифинга за пресата. „Може ли да се разшири до други видове математика, които може да нямат милиони задачи, върху които да се обучават?“

„Ние сме в момента, в който те могат да доказват не само отворени изследователски проблеми, но и проблеми, които са много предизвикателни за най-добрите млади математици в света“, каза компютърният специалист на DeepMind Дейвид Силвър, който беше водещият изследовател, разработващ AlphaGo в средата на 2010 г.