Автоматизация научного метода
Исследователь Ян Пасторек представил проект AutoGraphForge — вычислительный конвейер, который полностью автоматизирует цикл «гипотеза — опровержение — формализация — доказательство» в теории графов. Система работает итерационно: генератор Graffiti3 предлагает утверждения на основе небольшого набора данных, которые затем проверяются на новизну и истинность.
Масштаб данных и фильтрация
Ключевой этап — проверка гипотез на огромном наборе данных. Система использует фильтр новизны из 559 классических отношений и тестирует кандидаты на выборке из 348 000 графов. В датасет входят полные инварианты House of Graphs, полный перебор связных графов до 9 вершин, а также экстремальные семейства (сильно регулярные, минимальные Рамсея, графы Кэли и др.).
Результаты работы на HPC
После нескольких раундов работы на кластере высокопроизводительных вычислений (HPC) система отобрала 6 522 гипотезы, которые выдержали проверку на опровержение и прошли фильтр новизны. Среди них оказались нетривиальные связи между числом аннигиляции и числом реберного покрытия для двудольных и регулярных графов, которые автор подтвердил ручным доказательством.
| Компонент системы | Характеристики и параметры |
|---|---|
| Генератор гипотез | Graffiti3 (итеративный, на основе инвариантов) |
| 559 отношений, проверка через линейное программирование | |
| Базовый датасет | ~348 000 графов (House of Graphs, census до 9 вершин, экстремальные семейства) |
| Нейросетевые доказатели | DeepSeek-Prover-V2-671B (vLLM) и OProver-32B (специализированный для Lean) |
| Формальная верификация | Lean 4, mathlib4, kernel-verified proofs |
Интеграция с Lean 4
Завершающий этап конвейера — автоматическая формализация. Каждая выжившая гипотеза переводится в скелет утверждения на языке Lean 4. Доказательства генерируются двумя нейросетями — DeepSeek-Prover-V2-671B и OProver-32B — и проходят строгую ядровую проверку (kernel verification) против зафиксированной версии библиотеки mathlib4. Это обеспечивает математическую строгость результатов, полученных ИИ.
Источник: arXiv cs.AI ↗