Самый известный в мире русский инженер в ИИ занялся формальной верификацией алгоритмов на DeepSeek

Илья Полосухин входит в число «8 отцов-основателей GPT» как соавтор эпохальной статьи «Attention Is All You Need», с которой и началась ИИ-революция на трансформерах. Он не гражданин России — Илья родился в Харькове, но его успехи не связаны с качеством украинского образования: он ещё студентом попал в американскую компанию из Сан-Диего, которая и дала ему знания и практику в ИИ.

Илья сделал агента на DeepSeek, который смог пройти все 672 задачи PutnamBench.

https://github.com/nearai/putnambench-deepseek

PutnamBench — это бенчмарк для проверки способности ИИ строго доказывать сложные математические утверждения. Он собран из задач престижной североамериканской студенческой олимпиады William Lowell Putnam Mathematical Competition, переведённых из обычного текста в формальные языки доказательств: Lean 4, Isabelle и Coq.

Это не доказательство отсутствия ошибок любого алгоритма, а только тех алгоритмов, которые допускают строгую логическую проверку по смыслу. Это довольно новый тренд, и за ним важно следить, т.к. разработка в нём не имеет вообще классического тестирования и багфикса. Вместо этого доказывается дедукцией модели, что алгоритм — «само совершенство» и ошибок не может быть в принципе.

Я сейчас занимаюсь этой же тематикой в новой версии своего фреймворка GRACE, но не на жёстких математических условиях проверок, а на семантических. Это не даёт гарантию 100% безошибочности, как у Ильи, но накрывает почти все реальные бизнес-приложения, где математические гипотезы не сформулировать, т.к. они в принципе не формулируются классическими аналитическими методами матлогики.

Тем не менее, разные варианты формальных проверок корректности алгоритмов — определённо тренд и новая техника. Показательно, что Илья ещё доказал высокие способности последних версий DeepSeek в таком анализе. Вам не требуется Astra или Fable — даже DeepSeek V4.1 Flash достаточно мощен, если вы умеете правильно ставить ему задачу.

Илья в интервью отметил, что DeepSeek дешевле в 100-200 раз американских фронтиров, но вполне делает, что нужно. Также Илья указывает, что часто строгие проверки нужны для систем безопасности, а Claude или ChatGPT с высокой вероятностью вам откажут в анализе, т.к. не могут понять вы хакер или эксперт по безопасности.

Телеграм: t.me/ainewsline

Источник: t.me

Комментарии: