Исследователи разработали систему искусственного интеллекта AlphaProof Nexus, которая самостоятельно ищет формальные доказательства математических утверждений. Во время испытаний она решила девять задач Эрдеша и доказала 44 гипотезы из Онлайн-энциклопедии целочисленных последовательностей. Две задачи Эрдеша оставались нерешенными более 50 лет.
Система использует несколько ИИ-агентов, которые предлагают варианты доказательств и дорабатывают их с учетом обратной связи. Для проверки рассуждений применяется Lean — язык программирования и среда формальной верификации, позволяющая автоматически проверять логическую корректность каждого шага.
Такая проверка особенно важна для больших языковых моделей. Они способны решать сложные математические задачи, но иногда допускают незаметные логические ошибки или используют несуществующие утверждения. Если доказательство записано на языке Lean, система может проверить его формальную корректность, а не просто оценить, насколько убедительно оно выглядит.
В ходе экспериментов AlphaProof Nexus решила девять из 353 проверенных открытых задач Эрдеша. Кроме того, она доказала 44 из 492 гипотез, отобранных из Онлайн-энциклопедии целочисленных последовательностей — базы данных, содержащей сведения о числовых последовательностях и связанных с ними математических закономерностях.
Исследователи также применили систему к задачам из нескольких областей науки, включая алгебраическую геометрию, оптимизацию, квантовую оптику и теорию графов.
В более сложной конфигурации агенты координируют работу с помощью эволюционного алгоритма, который помогает отбирать и улучшать перспективные варианты доказательств. В систему также встроена возможность использовать AlphaProof — специализированный инструмент для доказательства теорем.
Авторы исследования считают, что формальный поиск доказательств может расширить возможности применения ИИ в математических исследованиях. Даже если система не находит окончательного решения, ее попытки могут помочь ученым обнаружить новые направления поиска. Система может стать вспомогательным инструментом для математиков, помогая искать и проверять доказательства сложных задач.
Читайте также:
Математики не доверяют доказательствам ИИ — нейросети научились обходить компьютерную проверку
GPT-6 Astra расшифровала письмо времен Наполеона, которое не могли прочитать 217 лет