Исследователи из Meta и Нью-Йоркского университета создали предельно упрощённую систему искусственного интеллекта для доказательства математических теорем, которая не уступила или превзошла тщательно спроектированные рабочие процессы доказательства на Lean — и при этом обошлась дешевле.

Система под названием h1 отстаивает простой тезис: в автоматическом доказательстве теорем простота может победить сложность, если модель получает качественную обратную связь.

Минималистичный агентный цикл

Работа выполнена исследовательской командой Meta FAIR совместно с NYU. В статье под названием «h1: A Taste of the Bitter Lesson in Automated Theorem Proving», опубликованной 25 октября 2026 года, исследователи описывают h1 как минималистичный агентный цикл, который соединяет большие языковые модели переднего края с Lean 4 и передаёт им результаты верификатора в реальном времени.

Lean 4 — это открытый интерактивный доказатель, в котором математические рассуждения записываются в виде кода, поэтому каждый шаг проверяет компилятор, а не человек. Такой подход даёт верификатору последнее слово: доказательство засчитывается только после успешной компиляции.

Большинство автоматических доказателей заключают языковую модель в сложную каркасную инфраструктуру, используя заранее заданные рабочие процессы, которые разбивают задачи на части, маршрутизируют подзадачи и координируют множество компонентов. Фреймворк h1 обходится без этой машины и вместо неё опирается на несколько простых механизмов:

• Постоянное редактирование файла, благодаря чему модель работает с файлом доказательства, сохраняющим состояние между шагами
• Немедленная обратная связь компилятора после каждого изменения, поэтому ошибки выявляются сразу
• Рефлексия — использование способности самой языковой модели рассуждать о том, что пошло не так

Согласно статье, производительность h1 обусловлена главным образом эффективным интерфейсом с Lean, а не изощрённой оркестрацией.

Результаты бенчмарков

В исследовании сообщается, что h1 достигла уровня лучших результатов на нескольких бенчмарках формального доказательства теорем. На PutnamBench — бенчмарке, составленном из задач Уильям Лоуэлла Путнамовского конкурса, ежегодного математического соревнования для студентов Северной Америки, — она набрала 670 из 672 с использованием GPT-5.5. В оценке FATE-X h1 получила 90 из 100.

Система также решила восемь открытых задач из коллекции FormalConjectures. Среди них — варианты задач Эрдёша, набора вопросов, названных в честь плодовитого математика Пала Эрдёша. Поскольку такие задачи формулируются на формальном языке Lean, их решение означает получение машинно-проверенных доказательств, а не текстовых рассуждений.

Наиболее прямое сравнение — с AlphaProof Nexus от DeepMind. По решению задач Эрдёша h1 показала долю успешных решений 82,5%, тогда как AlphaProof Nexus — 76%. Разрыв в стоимости оказался больше разрыва в точности: h1 тратила $121 на одно успешное доказательство против $317 у AlphaProof Nexus.

«Горький урок», применённый к математике

Название статьи отсылает к «горькому уроку» — термину, который исследователь ИИ Рич Саттон ввёл в эссе 2019 года для идеи о том, что масштабируемые универсальные методы, опирающиеся на большие вычислительные ресурсы, со временем, как правило, превосходят специализированные, созданные вручную техники.

Это не первая попытка Meta решить данную задачу. Исследование продолжает более ранние работы Meta, включая нейросетевой доказатель теорем HTPS, представленный в 2022 году, и отражает смену подхода. Ранние системы были сосредоточены на построении более умного поиска вокруг модели, тогда как h1 делает акцент на прямом взаимодействии модели с верификатором.

Важен и момент. Результаты h1 зависят от моделей переднего края, таких как GPT-5.5, и высокий результат на PutnamBench был достигнут именно с этой моделью.

Что это значит

Наиболее практическая часть работы — цифры затрат. Снижение стоимости успешного доказательства с $317 до $121 меняет сам набор задач, которые вообще имеет смысл пытаться решать. Когда каждая попытка стоит меньше, команды могут выполнять больше попыток на более сложных или спекулятивных гипотезах. Частью привлекательности является и машинно-проверяемый характер результатов: прогресс в формальном доказательстве привлекает внимание далеко за пределами математики, поскольку интерактивные доказатели используются также для верификации программного и аппаратного обеспечения.

Есть и оговорки. Результаты бенчмарков показывают производительность на конкретных наборах тестов, а PutnamBench близок к насыщению при 670 из 672, поэтому именно то, как системы справляются с коллекциями открытых задач вроде FormalConjectures, станет самой значимой метрикой в дальнейшем. Подход h1 также сильно зависит от лежащей в его основе модели переднего края.

Более широкий вывод статьи состоит в том, что сильная базовая модель в связке с чистой обратной связью от верификатора может значить больше, чем сложная каркасная инфраструктура — ставка, которая на этих бенчмарках себя оправдала.

Источник: CryptoBriefing