Если Астра находит математический результат в научной литературе, то она его не примет без проверки. Независимо насколько авторитетны автор или издание.
Текст 5.6 Sol о том как Астра решала НС уравнения.
Цитата:
Как искусственный интеллект решает математические задачи исследовательского уровня
Одним из примеров применения искусственного интеллекта в современной математике стало исследование проблемы существования и гладкости решений уравнений Навье — Стокса. Для получения результата использовалась многоагентная система OpenAI. Группа, достигшая результата, насчитывала порядка 10 000 одновременно работающих агентов.
Как был организован исследовательский процесс?
На первом этапе агенты получили различные формулировки задачи. Одни группы пытались доказать глобальную регулярность решений, другие искали контрпример. Агенты имели доступ к сохранённым интернет-материалам и могли выполнять программный код.
На втором этапе группы независимо исследовали различные математические подходы. Некоторые направления оказывались бесперспективными, другие приводили к новым промежуточным результатам и вспомогательным утверждениям.
На третьем этапе исследователи использовали Codex для объединения наиболее перспективных идей, полученных разными группами. Таким образом, даже попытка, не приведшая к окончательному решению, могла оказаться полезной для другой исследовательской группы.
После запуска первых агентов система получила предложенное решение. Затем GPT-6 Astra использовалась для формализации доказательства в Lean и его машинной проверки.
Принципиальное отличие такого подхода от обычного интернет-поиска заключается в том, что модель не ограничивается воспроизведением уже известных результатов. Она может использовать существующие теоремы, выводить новые вспомогательные утверждения, исследовать следствия различных гипотез и строить последовательность рассуждений, ведущую к доказательству.
Однако главная трудность заключается не в формулировании новых гипотез или лемм, а в строгом обосновании каждой из них. Увеличение вычислительных ресурсов, параллельная работа тысяч агентов и длительный перебор математических подходов расширяют возможности исследования, но сами по себе не гарантируют правильности полученного результата.
Как в таком случае система защищается от недостоверной информации из Интернета?
Здесь необходимо различать достоверность используемых источников и математическую корректность доказательства.
Если модель обнаружила ошибочное утверждение в научной статье или учебнике, авторитет автора и репутация издания не делают это утверждение истинным. Более того, одна и та же ошибка может многократно воспроизводиться в разных публикациях. Поэтому сопоставление источников полезно, но не заменяет самостоятельной математической проверки.
Существенную роль в обеспечении строгости играет формальная верификация доказательств, в частности с использованием Lean.
Предположим, модель использовала лемму L для доказательства теоремы T. Если лемма ошибочна, то получить корректное формальное доказательство на её основе невозможно, пока сама лемма не будет строго обоснована либо не появятся дополнительные предпосылки.
Однако существует важная оговорка. Ложную или недоказанную лемму можно объявить аксиомой. Тогда Lean сможет проверить правильность логического вывода из этой аксиомы, но не её истинность. Поэтому успешная формальная проверка требует также анализа использованных аксиом и зависимостей.
Кроме того, необходимо удостовериться, что формализованное утверждение в точности соответствует исходной математической задаче. Иначе система может безупречно доказать формально корректную теорему, которая отличается от той, которую исследователь намеревался доказать.
Таким образом, формальная верификация существенно повышает надёжность математических результатов, но не отменяет необходимости независимой проверки исходных предпосылок и соответствия формализации поставленной задаче
Показательно, что даже опубликованный результат OpenAI по уравнениям Навье — Стокса остаётся предметом научного рассмотрения. Наличие аналитического доказательства и его формализации в Lean ещё не равнозначно окончательному признанию результата математическим сообществом.
Публичные материалы OpenAI позволяют достаточно подробно проследить организацию многоагентного исследования и процедуру проверки полученного доказательства. Однако из них не следует, что Astra автоматически применяет универсальный и безошибочный механизм оценки достоверности каждого интернет-источника, использованного в исследовании.
Поэтому необходимо различать две способности искусственного интеллекта: открывать новые математические результаты и гарантировать корректность всех утверждений, на которых эти результаты основаны.
Значительные достижения в первой области уже продемонстрированы. Вторая по-прежнему требует строгой математической аргументации, независимой проверки и, когда это возможно, формальной верификации.
Именно сочетание творческих возможностей искусственного интеллекта с математической строгостью позволяет рассматривать подобные системы не просто как инструменты поиска информации, а как средства проведения самостоятельных исследований.
Поэтому, собственно, ИИ и врет, потому что его обучали на интернете. Кстати, современные молодые человеки в этом смысле не многим лучше. Именно по этой причине (не только, но в т.ч.).
