Все о блокчейн/мозге/space/WEB 3.0 в России и мире

Команда Google DeepMind решила 9 проблем Эрдёша с ИИ-агентом Они это сделали с помощью AlphaProof Nexus - фреймворка для автоматического поиска формальных математических доказательств с помощью LLM в связке с верификатором Lean 4. Недавно мы писали про формальную верификацию здесь. Надо отметить разницу с работами OpenAI, которые тоже говорят о решении задач Эрдёша. Кроме Google все пишут решения на естественном языке, которые требуют экспертной проверки. А Google использует верификацию автоматическую Lean, где каждый шаг автоматически верифицируется компилятором. Отметим, что ранее Google запустили коллекцию нерешенных математических задач на Lean. В итоге из 353 открытых задач Эрдёша AlphaProof Nexus автономно решила 9, включая 2 задачи, открытые с 1970 года. И все это обошлось в несколько сотен $ за задачу. Отдельно про Nexus читайте тут. Google DeepMind построили и сравнили 4 конфигурации: 1. Базовый агент - набор независимых подагентов, которые в цикле. 2. Базовый + AlphaProof к базовому добавляется возможность вызывать AlphaProof как инструмент для закрытия отдельных подцелей. 3. Базовый + эволюция - ИИ-агенты работают с общей базой набросков, ранжируют их по Elo через LLM-критика (Gemini Flash), используют алгоритм P-UCB для выбора перспективных направлений. 4. Полная система - комбинация всего: AlphaProof + эволюция + Elo-рейтинги. Авторы говорят, что базовый агент решил все 9 задач Эрдёша, хотя изначально они запускали полную систему именно потому, что простые агенты плохо работали на соревновательных бенчмарках. Это означает, что по мере роста базовых способностей LLM сложные архитектуры теряют преимущество на средних задачах. Полная система остаётся лучше только на самых сложных, там она в 2-5 раз дешевле по стоимости успешного доказательства.