ИИ-система AutoGraphForge автоматически открыла тысячи новых математических гипотез
Международная группа разработчиков представила AutoGraphForge — вычислительную систему, способную автоматически открывать новые теоремы в теории графов. Проект, описанный в препринте на arXiv, объединяет генерацию гипотез, поиск контрпримеров и формальную проверку доказательств.
Система работает циклически: генератор Graffiti3 предлагает гипотезы на основе таблицы из нескольких сотен графов с вычисленными инвариантами. Таблица пополняется только контрпримерами к собственным гипотезам. Каждая новая гипотеза проходит через фильтр новизны, включающий 559 известных соотношений, проверяемых с помощью линейного программирования.
Выжившие кандидаты тестируются на обширной базе данных около 348 тысяч графов. В выборку вошли полный экспорт инвариантов House of Graphs, исчерпывающая перепись всех связных графов с числом вершин до девяти, а также экстремальные семейства: сильно регулярные графы, графы Рамсея, графы Кэли, клетки и другие модели.
В ходе нескольких раундов на кластере HPC система сгенерировала 6522 гипотез, которые пережили опровергающий датасет, фильтр новизны и все проверки активного поиска контрпримеров. Среди них обнаружены нетривиальные соотношения между числом аннигиляции и рёберным покрытием для двудольных и регулярных графов — эти утверждения впоследствии доказали вручную.
Следующий этап — автоматическая формализация. Каждая выжившая гипотеза транслируется в синтаксическую заготовку утверждения на языке Lean 4. Проверка корректности выполняется независимым ядром доказательств. На этом этапе задействованы две нейросети: DeepSeek-Prover-V2-671B, запущенная через vLLM, и специализированная для Lean модель OProver-32B.
Пайплайн полностью реализован и проходит первоначальные проверки работоспособности. Сейчас полный цикл выполняется на кластере. По словам авторов, проект демонстрирует потенциал автоматизации математических исследований, где ИИ не только строит догадки, но и доводит их до формально проверяемых доказательств.
