Компания Google DeepMind представила новый математический фреймворк под названием AlphaProof Nexus. Эта система смогла самостоятельно решить девять открытых задач из списка известного математика Пола Эрдёша. Некоторые из них оставались нерешенными более полувека. Также система доказала 44 гипотезы из Онлайн-энциклопедии целочисленных последовательностей (OEIS) и решила 15-летнюю проблему в алгебраической геометрии. Об этом сообщает Ixbt.com .
Ключевой особенностью системы AlphaProof Nexus является интеграция языковой модели Gemini 3.1 Pro и системы формальной математической проверки Lean. В отличие от обычных LLM-моделей, эта система формирует доказательства не на естественном языке, а пошагово на языке программирования Lean. Каждый шаг автоматически проверяется компилятором. Если возникает ошибка, Lean выдает точное сообщение, и модель делает выводы для следующей попытки. Такой подход предотвращает логические ошибки (галлюцинации) искусственного интеллекта.
По словам исследователей, вычислительные затраты на решение одной задачи составили несколько сотен долларов. Система показала высокие результаты, особенно в таких областях, как комбинаторика, теория чисел и выпуклая оптимизация, где библиотека Mathlib хорошо развита. Тем не менее, из 353 открытых задач Эрдёша на данный момент решено только девять, что говорит о том, что искусственному интеллекту еще предстоит много работы.
Специалисты DeepMind подчеркивают, что AlphaProof Nexus не заменит математиков, а станет новым инструментом для исследований. Все формальные доказательства, представленные системой, были опубликованы на платформе GitHub. Эта работа была проведена на фоне достижений конкурентов, таких как OpenAI, в области математических исследований. Например, ранее OpenAI с помощью своей модели рассуждений опровергла гипотезу Эрдёша о расстояниях.
Читайте «Zamin» в Telegram!
