Розв’язання кожної задачі в одному з найскладніших тестів з математики зазвичай коштує десятки тисяч доларів. NEAR AI зробив це за $111.
6 вересня 2026 року співзасновник NEAR Protocol Олександр Скіданов оголосив, що відкритий агент Lean проекту вирішив усі 672 завдання бенчмарку PutnamBench, який складається з завдань з математичної олімпіади імені Вільяма Лоуелла Патнема. Загальна вартість: 111 доларів США. Другий найдешевший відомий результат коштував у 250 разів більше.
Що таке PutnamBench і чому це має значення
Змагання Патнем — найпрестижніший підготовчий математичний конкурс у Північній Америці. Набрати нуль балів — не незвичайно, навіть серед блискавичних студентів. Екзамен створений, щоб зламати вас.
PutnamBench, представлений у 2024 році, продовжує цю традицію складності, перетворюючи її на формальну тестову сукупність для AI-доказових систем. Бенчмарк містить 672 задачі, закодовані в Lean 4 — мові допоміжного засобу доведення, яка вимагає, щоб математичні аргументи були записані з машинно-перевіряємою точністю. Доведення, що є логічно невдалою, відхиляється одразу, без часткового зарахування.
До результатів NEAR AI агенти, що намагалися пройти PutnamBench, часто потребували тисяч викликів висновку на кожну задачу. Витрати на обчислення швидко зростали, і повні прогони тестового набору коштували від 10 000 до 25 000 доларів США для лідируючих систем.
Агент NEAR AI завершив усі 672 завдання за 111 доларів.
Чому розрив у вартості — це справжня історія
За ціною від 10 000 до 25 000 доларів США за повний цикл лише невелика кількість організацій могли собі дозволити ітерувати, експериментувати та покращувати свої конвеєри доведення теорем. За ціною в $111 цей розрахунок повністю змінюється.
Швидкий прогрес у результатах PutnamBench між 2025 та 2026 роками вже забезпечувався агентними робочими процесами, які поєднують великі мовні моделі з двигуном перевірки доведень Lean. Підхід NEAR AI розширює цю модель, додаючи рівень ефективності, якого спільнота бенчмарку раніше не бачила.
NEAR AI позиціонує це досягнення в межах ширшої інфраструктурної ідеї, заснованої на тому, що вона називає IronClaw — фреймворку, спрямованому на конфіденційність та перевіряємість ШІ. Здатність до формальної верифікації прямо відповідає цьому підходу: якщо ви можете довести, що математичний аргумент є правильним на рівні машини, ви отримуєте основу для систем ШІ, вихідні дані яких можна незалежно аудитувати, а не довіряти їм на віру.
Рішення NEAR Protocol зробити Lean-агент відкритим джерелом підсилює його значущість. Власні інструменти, які забезпечують перевагу у витратах у 250 разів, зазвичай залишаються власністю. Відкриття джерельного коду агента означає, що методологія доступна для перевірки, розширення та використання будь-ким.