AML – Telegram

N, ε, Ω, Λ, Q, D

39 views14:29

AlphaProof Nexus — система, где LLM перестаёт быть просто генератором текста и начинает работать как полноценный агент внутри среды с обратной связью

Это важный сдвиг.

Главная проблема обычных LLM — галлюцинации

Для математики это критично: одна ошибка ломает всё доказательство
Но вместо попыток «сделать модель аккуратнее» исследователи изменили сам процесс работы

Теперь у неё есть внешняя система проверки, которая может мгновенно подтвердить или опровергнуть каждый шаг рассуждений

Для этого используется Lean — язык формальных математических доказательств, где каждое утверждение проходит строгую автоматическую верификацию компилятором

Получается такой цикл:
— модель предлагает следующий шаг доказательства
— система проверки валидирует его
— при ошибке агент получает точную обратную связь
— корректирует стратегию
— и продолжает поиск решения

То есть система работает уже не как чат-бот, выдающий ответ за один проход, а как агент, взаимодействующий со средой и постоянно адаптирующий свои действия

Именно это сейчас становится одним из главных направлений развития AML:
не просто “больше нейронных связей”, а появление циклов
генерация → проверка → обратная связь → исправление → новая попытка.

По сути, модель получает нечто похожее на настоящий исследовательский процесс

Результаты при этом очень серьёзные:
— решены 9 открытых задач Эрдёша
— доказаны 44 гипотезы из OEIS
— найден контрпример к одной из гипотез Бена Грина
— продвинут 15-летний спор в алгебраической геометрии

Но, возможно, главный вывод работы даже не в математике

Похоже, что следующий этап развития — это не «ещё более умные чат-боты», а системы, которые умеют:
— долго работать над задачей
— проверять себя
— использовать внешние инструменты
— хранить промежуточное состояние
— и постепенно улучшать собственное решение

Именно это и называют переходом к агентному AML

https://arxiv.org/abs/2605.22763v1?ref=airadar.one

https://github.com/google-deepmind/alphaproof-nexus-results

arXiv.org

Advancing Mathematics Research with AI-Driven Formal Proof Search

Large language models (LLMs) increasingly excel at mathematical reasoning, but their unreliability limits their utility in mathematics research. A mitigation is using LLMs to generate formal...

248 views22:57