Google DeepMind выпустило исследование, которое буквально ломает мозг каждому математику. AlphaProof, система, которая решила задачи международной олимпиады по математике на серебро, стала делать это полностью сама, без костылей! К слову, больше таких новостей есть в KLSTR!
Ни единой галлюцинации, только сухой расчет!
AlphaProof это вообще не тот ChatGPT, который галлюцинирует с утра до вечера и выдаёт чушь за истину. Совершенно другой зверь. Система работает внутри Lean - это такой строгий язык проверки теорем, где каждый шаг доказательства автоматически проверяет компьютер. Каждый отдельный шаг! Никаких ошибок. Никаких галлюцинаций! Ни одного правдоподобного бреда!
А еще прикольнее не обучали на интернете, как обычные нейросети. DeepMind взяла миллион математических задач, перевела в формальный язык, выжала 80 миллионов уникальных утверждений. Потом запустила то, что называется подкрепляющимся обучением.
А что же произошло на олимпиаде-то?
На IMO эта штука решила три задачи из пяти. Включая самую адскую задачу. Ту, над которой только пять человек из 600 участников не поломали голову! Это нестандартные задачи, которые люди специально придумали, чтобы ловить машины. И система получила 28 баллов из 42 и взяла серебро. Впервые в истории ИИ вообще медаль получает.
Но тут же есть множество гигантских подвохов:
- Вся эта система в сотню раз медленнее черепахи! Для сложных задач ей нужно было 2-3 дня. Это нереально долго. И второе система вообще не понимает задачи, которые ей не показывали. Комбинаторика? Фиаско полное! Люди решают комбинаторные задачи потому что видят закономерность, видят структуру. AlphaProof просто... не видит. Исследователи это честно признали: алгебра работает супер, теория чисел средне, а вот комбинаторика — полная беда.
- Нужно переводить задачи вручную в формальный язык. Да, система может это делать сама, но требует времени и подготовки. Обычный человек прочитает задачу на простом русском и решит. AlphaProof нужна формализация.
Гений математики Тимоти Гауэрс такого от ИИ не ожидал
Знаете, что написал Тимоти Гауэрс, один из самых крутых математиков, живущих прямо сейчас? Он лично проверял доказательства AlphaProof. Его отзыв:
Я мог узнать знакомые подходы, но некоторые идеи просто выходят за границы того, что я считал возможным для ИИ в этом году.
Скорее всего математики начнут использовать разработку для проверки рутинных шагов больших доказательств, освобождая себя для творчества. Преподаватели получат инструмент для автоматической верификации задач.