Невероятно, это имяГауссНовый ИИ-агент (Гаусса) чувствует себя немного сумасшедшим. Потому что он использует толькотри неделивремя, дело сделаноТеренс Таои математическая задача Алекса Конторовича по формализации теоремы о простых числах (PNT) в Lean.
Знаете, после того как Тао Чжэсюань и Конторович предложили эту задачу в январе 2024 года, они потратили много времени.18 месяцев(июль этого года) достигнут лишь поэтапный прогресс.
Так каково же происхождение этого Гаусса?
За этим стоит компания под названиемМатематикаКомпания AI, по имеющимся данным, Gauss является первой, кто помогает ведущим математикам в формальной проверкеавтоматическая формализация(автоформализация)Агент:
Под формализацией здесь понимается преобразование математического содержания, написанного людьми, в машиночитаемый, проверяемый, строгий и однозначный формальный язык с последующим использованием компьютеров для проверки его правильности.
Причина, по которой Тао Чжэсюань и Алекс Конторович до сих пор добились лишь поэтапного прогресса, заключается в том, что проблема застряла в ключевой проблеме комплексного анализа.
Будучи кремниевой жизнью, этот Гаусс характеризуется способностью работать без перерыва, что значительно снижает рабочую нагрузку, которую в прошлом могли выполнять только ведущие формальные эксперты; в то же время Гаусс также формализовал ключевые недостающие результаты комплексного анализа, упомянутого выше.
Вот почему он может решить математическую задачу, которую Теренс Тао не смог решить за 18 месяцев, за три недели.
Как реализован Гаусс?
В настоящее время Math Company официально не опубликовала конкретный технический отчет.
Но, судя по конечному результату, Гаусс сгенерировал примерно 25 000 строк бережливого кода, содержащего тысячи теорем и определений.
Знаете, формальные доказательства такого масштаба часто занимали многие годы.
Крупнейшие одиночные формальные проекты в истории (часто охватывающие даже 10 лет) лишь на порядок превышают этот размер (до 500 000 строк кода).
Для сравнения, стандартная математическая библиотека Lean Mathlib содержит около 2 миллионов строк кода и 350 000 теорем, но на ее создание ушло более 600 участников и 8 лет.
Чтобы поддержать работу Gauss, команда также сотрудничала с Morph Labs для разработки инфраструктуры среды Trinity.
Потому что для запуска Gauss в таком большом масштабе потребуются тысячи одновременно работающих агентов, и каждый агент имеет свою собственную экономичную операционную среду, которая будет потреблять несколько терабайт кластерной памяти, что делает эту задачу чрезвычайно сложной системной инженерией.
Команда математиков также заявила:
Gauss значительно сократит время, необходимое для выполнения крупных математических проектов.
Поскольку алгоритмы продолжают совершенствоваться, мы планируем увеличить общий объем формального кода в 100–1000 раз в течение следующих 12 месяцев.
Это станет тренировочной площадкой для новых парадигм – в сторону «проверяемого сверхинтеллекта» и «универсальных машинных математиков».
И только сейчас,Теренс ТаоЯ объяснил некоторые вопросы, связанные с формализацией Мастодонта (далее — заявление Тао Чжэсюаня).
Проекты любой сложности, как правило, имеют явно сформулированные цели и неявные неявные цели. Например, заявленной целью проекта формализации бережливого производства может быть получение формального доказательства некоторого математического утверждения…; научитесь использовать различные инструменты для совместной работы и назначать задачи; органично обнаружить более тонкую структуру доказательств
В прошлом часто не было необходимости формулировать эти неявные цели, поскольку существовала сильная эмпирическая корреляция между достижением этих целей и достижением явных целей. В случае формальных проектов практически любые усилия, ориентированные на человека и направленные на достижение явных целей, в конечном итоге естественным образом достигают большинства неявных целей, упомянутых выше. Таким образом, явные цели фактически становятся жизнеспособной альтернативой более широким практическим целям.
Однако ситуация меняется с появлением мощных инструментов искусственного интеллекта, которые используют совершенно иные подходы, чем люди. Эти инструменты могут быть направлены на решение явной цели без необходимости достижения всех неявных целей, которые могли бы быть достигнуты одновременно, если бы задачу выполняла команда людей. Фактически, природа алгоритмов оптимизации ИИ предполагает, что они могут даже достичь высокой производительности при достижении явных целей за счет всех неявных целей. (См. Закон Гудхарта: «Когда мера становится целью, она перестает быть хорошей мерой».)
Учитывая все более широкое использование этих инструментов, мне кажется, что организаторам проекта теперь необходимо приложить больше усилий, чтобы четко сформулировать все цели проекта, а не только номинальные. В некоторых случаях эти цели могут быть изначально даже не очевидны для самих организаторов и могут потребовать некоторого обсуждения среди участников. Внешние стороны, заинтересованные в тестировании таких проектов с помощью своих инструментов искусственного интеллекта, должны заранее координировать свои действия с организаторами на случай, если они упустят одну или несколько ключевых неявных целей, которые их инструменты не смогут оптимизировать.
Основатель — автор премии ICML’25 Time Test Award
Стоит отметить, что у босса компании Math тоже есть некоторая сила.
Потому что он является одним из авторов статьи, получившей награду ICML Time Test Award на конференции по искусственному интеллекту в этом году.Кристиан Сегеди.
Эта статья представляет собой пакетную нормализацию (Batch Normalization, называемую BatchNorm), предложенную им и другим автором Сергеем Лоффе в 2015 году.
Сегодня эту статью процитировали более 60 000 раз. Это важный прорыв в истории развития глубокого обучения, который значительно способствовал обучению и применению глубоких нейронных сетей.
Можно сказать, что это одна из ключевых технологий, которая позволяет глубокому обучению перейти от небольших экспериментов к масштабной практичности и надежности.
Конечно, хотя пользователи сети воскликнули «Удивительно» после прочтения Гаусса, они также призвали чиновника как можно скорее опубликовать статью.
Что касается более подробного технического содержания, мы можем взглянуть~