Новый ИИ-фреймворк систематически находит и проверяет крупные математические гипотезы
Научный препринт, опубликованный на arXiv, описывает новый подход к автоматическому поиску крупных математических гипотез. Авторы использовали большие языковые модели и формальную верификацию, чтобы систематизировать процесс, который раньше зависел от интуиции экспертов.
Крупные математические проблемы, такие как гипотеза Римана, до сих пор требуют глубокого понимания и творческого подхода. Единой методики для порождения и проверки подобных утверждений не существовало, что ограничивало возможности автоматизации в этой области.
Предложенный конвейер состоит из трёх этапов. На первом этапе выполняется поиск областей на основе локальных математических данных. Второй этап включает рефлексивную валидацию по критериям фундаментальности, новизны и потенциальной значимости. На третьем этапе утверждения формально проверяются в системе Lean 4 и библиотеке Mathlib.
Цель — выявление задач с высоким математическим вкусом. Под этим понимаются проблемы, доказательство которых может перестроить язык целой области и оказать долгосрочную помощь в математических исследованиях.
В экспериментах на двадцати кандидатах система показала устойчивый переход от естественного языка к формальным проверкам. Все двадцать кандидатов прошли парсинг и проверку типов в Lean, ни один не был напрямую поглощён существующими тактиками, ни один не отклонён автоматически, а явных дубликатов или близких аналогов не обнаружено.
По мнению авторов, такой подход может стать шагом к созданию ИИ-помощников для математиков, способных генерировать новые гипотезы и проверять их формально. Однако речь идёт о препринте, и окончательная значимость найденных утверждений ещё требует подтверждения.
