Протокол NEAR обнародовал планы по применению формальной верификации с поддержкой ИИ к своему протоколу и основным смарт-контрактам после сообщения о решении 672 математических задач при стоимости модели на момент подачи в $111,85.
Краткое содержание
- NEAR планирует применить формальную верификацию с поддержкой ИИ к своему протоколу и основным смарт-контрактам.
- NEAR AI сообщила о решении 672 задач PutnamBench при стоимости модели на момент подачи в $111,85.
- Производственная верификация требует точных моделей программного обеспечения, определённых требований и доказательств, охватывающих развёрнутую реализацию.
- Формальная верификация дополняет тестирование и обзоры кода, при этом гарантии ограничены указанными свойствами и допущениями.
Протокол NEAR заявил в объявлении от 16 октября, что его исследование направлено на снижение специализированных трудозатрат и вычислительных расходов, связанных с доказательством того, что программное обеспечение следует определённым правилам.
Планируемое применение охватывает протокол сети и основные контракты, а также инструменты для разработчиков экосистемы. NEAR охарактеризовал производственную верификацию как цель, тогда как его завершённая эталонная работа касается автоматизированной генерации математических доказательств.
NEAR планирует перенести генерацию доказательств в производственное программное обеспечение
Согласно объявлению NEAR, применение исследования к работающему программному обеспечению включает три этапа. Разработчики должны представить программу математически, определить свойства, которым она должна удовлетворять, и построить доказательства того, что эти свойства выполняются.
Недавние результаты эталонных испытаний NEAR AI демонстрируют прогресс на третьем этапе. В объявлении говорится, что производственная работа по-прежнему требует точных моделей поведения программного обеспечения и чёткой связи между доказательствами и реализацией, на которую полагаются пользователи.
В своём объяснении NEAR отличает доказательство, охватывающее конкретное правило учёта, от гарантии того, что всё приложение безопасно. Контракт может сохранять балансы при переводах, но при этом требовать отдельного доказательства того, что инициировать их могут только авторизованные аккаунты.
Соучредитель NEAR Илля Полосухин связал это исследование с рисками, связанными с программным обеспечением, генерируемым ИИ, и инструментами, которые помогают злоумышленникам выявлять уязвимости.
«Будущее ИИ и кода, генерируемого ИИ, захватывающе — но только после того, как мы достигнем проверяемых и математических гарантий его поведения».
В объявлении воспроизводится заявление из текста Полосухина о безопасности программного обеспечения. NEAR утверждает, что формальная верификация должна дополнять тестирование, обзор кода и практики операционной безопасности.
Результат в $111,85 измеряет математические доказательства
В объявлении NEAR сообщается, что его ИИ-агент решил 672 задачи Lean из PutnamBench — эталонного набора, основанного на студенческом математическом конкурсе Патнэма. Сообщаемая средняя стоимость составила примерно $0,17 за задачу при ценах модели, использованных для подачи.
Публичный репозиторий проекта описывает результат как 670 исходных задач плюс исправленные версии двух задач с дефектными формализациями. NEAR заявляет, что сообщаемые расходы не включают полную стоимость разработки системы и не оценивают цену верификации производственного контракта.
В репозитории команда сообщает, что воспроизведение того же использования по более поздним указанным ценам DeepSeek в непиковые часы стоило бы $331. Их методология включает неудачные попытки, хотя авторы выделяют отдельный параллельный эксперимент с использованием Kimi, который они исключили из учёта затрат.
В репозитории описываются проверки на незавершённые доказательства и изменения в математическом утверждении, которое доказывается. Сообщается, что самый длительный запуск длился более трёх дней.
Наряду с PutnamBench, NEAR сообщает, что её команда заняла первое место по общему числу решённых задач в таблице лидеров формализации Lean Eval v1. В объявлении уточняется, что это показатель рейтинга, что отличает его от первых решений и уникальных решений.
По словам NEAR, математические бенчмарки проверяют способность, необходимую для верификации программного обеспечения, поскольку разработчики переводят требования к программному обеспечению в математические утверждения. Компания отделяет эти результаты от работы по доказательству свойств развёрнутого кода.
Формальные доказательства зависят от правил, которые выбирают разработчики
В примере с переводом от NEAR обычный тест проверяет выбранную транзакцию, например перемещение пяти токенов между двумя счетами. Доказательство может установить, что каждый успешный перевод, охватываемый математической моделью, сохраняет совокупный баланс счетов.
В объявлении объясняется, что разработчики сначала выбирают требование, выражают соответствующее поведение программного обеспечения математически и передают предложенное доказательство проверяющему. Полученная гарантия зависит от используемых определений и допущений.
Подход NEAR использует Lean — открытый язык программирования и помощник доказательств. ИИ-агент может предложить доказательство, запустить Lean, изучить его обратную связь и пересмотреть попытку, в то время как ядро Lean проверяет, следует ли доказательство его логическим правилам.
Неудачная попытка не обязательно указывает на дефект программного обеспечения, по словам NEAR. Требование может быть неверным, реализация может его нарушать, или агент может не найти корректное доказательство.
Формальная верификация уже имеет задокументированные применения в экосистеме NEAR. Оценка Templar от Certora от 30 марта — кредитного протокола, развёрнутого на NEAR, — описывает ручной обзор его контрактов на Rust и формальную спецификацию и верификацию его рыночного контракта. Страница оценки Certora определяет доказанные свойства и обнаруженные проблемы как предметы полного отчёта.
Другие блокчейн-команды также занимались верификацией с помощью ИИ
В мае Aptos Labs описала поддержку формальной верификации с помощью ИИ, включающей динамическую диспетчеризацию в контрактах Move. Согласно освещению объявления, заявленный рабочий процесс использует спецификации, сгенерированные ИИ, с Move Prover.
Соучредитель Ethereum Виталик Бутерин обсуждал аналогичное сочетание инструментов ИИ и машинно-проверяемых доказательств. Как ранее сообщал crypto.news, в его майских комментариях были определены применения по всей дорожной карте Ethereum, включая консенсус, квантово-устойчивую криптографию и системы с нулевым разглашением.
Бутерин предупредил, что доказательство одного уровня не устанавливает, что вся система ведёт себя так, как задумано. Его обсуждение охватывало верификацию от высокоуровневых спецификаций до низкоуровневой реализации.
Отдельное исследование безопасности NEAR касалось квантово-устойчивых подписей. Майское предложение Near One выбрало поддержку подписей FIPS-204, используя стандарт ML-DSA, одобренный Национальным институтом стандартов и технологий США.
В майском предложении описывалась цель для тестовой сети к концу второго квартала 2026 года. Near One заявила, что кошельковое программное обеспечение, аппаратные кошельки, конечные точки и API потребуют скоординированных изменений для поддержки новых схем подписи.
