ainews
ИИ впервые проверил самое сложное математическое доказательство: теорема о простых числах и будущее безопасного кода
Команда Axiom Math автоматически верифицировала доказательство «теоремы 246» — важнейшего результата о простых числах. Это первый случай полной AI-проверки столь сложного доказательства. Главное: технология готовится проверять AI-код, на котором скоро будет работать весь мир.
Потому что AI уже пишет код, который управляет деньгами, данными и инфраструктурой. Технология формальной верификации может сделать этот код безопасным — или хотя бы показать, где он точно небезопасен.
Что произошло
Команда Axiom Math с помощью системы AxiomProver автоматически верифицировала доказательство теоремы о простых числах, известной как «теорема 246». Это самое сложное математическое доказательство, проверенное ИИ на сегодня.
Теорема утверждает: существует бесконечно много простых чисел, которые отличаются друг от друга ровно на 246. Звучит абстрактно, но это максимум, до которого математики дошли в попытках доказать гипотезу о простых числах-близнецах (разница в 2) — задачу, нерешённую с XIX века. Теорему доказали Джеймс Мейнард и Теренс Тао в рамках коллаборации Polymath8b.
Формальная верификация — это когда компьютер проверяет машиночитаемую версию доказательства. Не абсолютная гарантия (недавно показали, что баг в методе может пропустить фальшивое доказательство), но близко к ней.
Axiom Math не просто проверила одно доказательство. Команда построила библиотеку результатов о разрывах между простыми числами — переиспользуемую основу для будущих задач. Теорема 246 — флагманский результат этой библиотеки.
Основатель компании Кен Оно видит главную цель не в математике, а в проверке AI-кода: «Мир скоро будет работать на коде, который никто не читал». Если свойства кода можно перевести в математические утверждения, технология AxiomProver сможет их верифицировать — и сделать AI-код безопасным.
Автор: Никита Громов · Источник: spectrum.ieee.org
Разработчикам. Автоматическая верификация доказательств открывает путь к формальной проверке AI-сгенерированного кода: можно математически доказывать, что алгоритм всегда завершается или выдаёт корректный результат. Это критично для безопасности систем, где AI пишет код для инфраструктуры, финансов или защиты данных.
Бизнесу. Компании, использующие AI-генерацию кода (Copilot, Cursor, внутренние ассистенты), получают инструмент для проверки на баги и уязвимости. Это снижает риски и повышает доверие к автоматизации. Особенно актуально в финтехе, кибербезопасности и критичной инфраструктуре.
Инвесторам. Формальная верификация AI-кода — растущая ниша на пересечении математики, безопасности и DevOps. Axiom Math показывает работоспособность подхода. Секторы роста: верификация для AI-кода, безопасность критичных систем, инструменты для compliance в регулируемых отраслях (финансы, здравоохранение).
- Создать SaaS для формальной верификации AI-кода: API, которое проверяет корректность функций, написанных LLM, до деплоя в прод
- Интегрировать верификацию в IDE и CI/CD: плагин для VSCode/GitHub Actions, который автоматически проверяет AI-сгенерированный код на математическую корректность
- Консалтинг по внедрению формальной верификации для финтеха и здравоохранения: помочь компаниям соответствовать регуляторным требованиям
- Построить библиотеки доказательств для популярных алгоритмов и паттернов кода, продавать доступ к ним разработчикам и компаниям
- Развивать инструменты для автоматического перевода свойств кода в математические утверждения — ключевое узкое место технологии
- Формальная верификация не даёт 100% гарантии — недавно показали, что баг в методе может пропустить ложное доказательство
- Технология пока работает только для узкого класса задач; масштабирование на весь AI-код — сложная и нерешённая проблема
- Высокая вычислительная сложность: проверка сложных доказательств требует значительных ресурсов, неясно, насколько это масштабируется на миллионы строк кода
- Хайп вокруг AI-безопасности может переоценить реальную готовность технологии к массовому применению
Это важнее, чем кажется на первый взгляд. Формальная верификация математических доказательств — не самоцель. Axiom Math открыто говорит: цель — проверять AI-код, который уже пишет половину нового софта и скоро будет писать 90%. И это реальная проблема: AI-генерация кода растёт быстрее, чем наша способность его проверять.
Но пока это далеко не серебряная пуля. Верификация требует перевести свойства кода в математические утверждения — нетривиальная задача. Работает на простых алгоритмах, но как масштабировать на реальные системы с миллионами строк — неясно. И баги в самих методах верификации никто не отменял. Всё это значит, что до массового применения ещё далеко, но направление правильное. Следите за Axiom Math и конкурентами: кто первый сделает это usable для реального кода — тот заберёт рынок.
Комментарии