Материал подготовлен автоматически по первоисточникам: ссылки на них — в конце статьи.
Ján Pastorek разработал AutoGraphForge — систему для генерации, опровержения и формализации гипотез в теории графов, описанную в препринте, не проходившем рецензирования. По замерам автора, после нескольких раундов проверки осталось 6 522 гипотезы, но их выживание ещё не означает доказанности. Работа важна командам, которые проектируют автоматические исследовательские системы и должны отделять генерацию идей от проверяемого результата.
Что сделали
AutoGraphForge начинает с небольшой таблицы графов и вычисленных для них инвариантов — числовых характеристик вроде числа независимости или хроматического числа. Graffiti3 строит по этой таблице возможные неравенства и условия, после чего фильтр из 559 известных и выводимых соотношений отсеивает повторные результаты.
Оставшиеся гипотезы система проверяет на заранее собранном наборе графов и передаёт алгоритмам активного поиска контрпримеров. Найденный контрпример добавляется в исходную таблицу, поэтому следующий раунд генерации учитывает прежнюю ошибку. Выжившие утверждения детерминированно переводятся в каркас на Lean 4; нейронные доказатели могут предложить доказательство, но принять его способен только независимый проверяющий модуль Lean.
Среди результатов автор вручную доказал пару соотношений между аннигиляционным числом и числом рёберного покрытия для двудольных и регулярных графов. Это показывает, что цикл способен выдавать содержательные утверждения, хотя автор не считает их глубокими новыми теоремами.
Что это значит
Практический результат работы — архитектурный шаблон: генератор предлагает варианты, база известных фактов убирает повторы, поиск контрпримеров обновляет входные данные, а формальная система становится последней границей доверия. Такой подход снижает риск принять правдоподобный вывод модели за проверенное утверждение и применим не только к математике, но и к системам, где результат можно проверить формальными правилами.
Ограничения. Авторы проверяли гипотезы на конечном наборе из 348 207 графов, содержащем до 59 точно вычисленных инвариантов, поэтому отсутствие контрпримера не доказывает утверждение для всех графов. Этап доказательства прошёл только начальные проверки и ещё не оценивался контролируемо на выживших гипотезах. В работе также нет сопоставления с другими генераторами и доказателями по доле действительно новых, нетривиальных и автоматически доказанных результатов; замкнутый цикл пока остаётся целью проекта.
Источники
Иллюстрация: рисунок из статьи «AutoGraphForge: Towards Automated Graph Theory Discovery», J\'an Pastorek, CC BY 4.0
Похоже на вашу задачу?
Расскажите, что собираете. За полчаса разложим на этапы и назовём сроки — это бесплатно и ни к чему не обязывает.
