Кристиан Сегеди

вики
, , , ,
1

Венгро-американский учёный-исследователь, создавший архитектуру Inception, открывший состязательные примеры (adversarial examples) и соизобретатель пакетной нормализации (batch normalization) в Google Brain. Впоследствии переключился на создание математически верифицируемого ИИ с помощью автоформализации.

Профиль
Родился около конца 1970-х, Венгрия
Гражданство Венгро-американское
Текущее место работы Math Inc (основатель); Morph Labs (бывший главный научный сотрудник)
Области исследований Глубокое обучение, компьютерное зрение, проектирование нейроархитектур, состязательное машинное обучение, автоматическое доказательство теорем, автоформализация, формальная верификация
Научный руководитель Йенс Виген (Jens Vygen, требуется подтверждение)
Докторская диссертация Масштабируемое обучение признакам (Scalable feature learning) — прикладная и дискретная математика (Боннский университет, ок. 2005)
X / Twitter @ChrSzegedy
Google Scholar Christian Szegedy

Обзор

Кристиан Сегеди (Christian Szegedy) — венгро-американский исследователь ИИ, наиболее известный тремя вкладами, сделанными за двенадцать лет работы в Google Brain: сверточной архитектурой Inception (GoogLeNet), победившей в ImageNet Large Scale Visual Recognition Challenge в 2014 году; открытием состязательных примеров (adversarial examples), выявивших фундаментальную уязвимость нейронных сетей и положивших начало целому направлению исследований в области безопасности ИИ; и пакетной нормализацией (batch normalization), соизобретённой с Сергеем Иоффе (Sergey Ioffe), ставшей одним из самых универсально применяемых методов обучения в глубоком обучении. С 2016 года Сегеди почти полностью переключил своё внимание на формальные математические рассуждения — утверждая, что верифицируемые машиной доказательства представляют собой единственный принципиальный путь к надёжному ИИ — и постепенно перешёл от отраслевых исследований к созданию компаний вокруг этой идеи. Он стал сооснователем xAI вместе с Илоном Маском (Elon Musk) в 2023 году, занимал пост главного научного сотрудника в Morph Labs, а в настоящее время возглавляет Math Inc, где его основным инструментом является система формального доказательства Gauss.

Ранние годы и образование

Сегеди вырос в Венгрии, учился в Fazekas Mihály fővárosi gyakorló gimnázium в Будапеште — одной из самых престижных математических и естественнонаучных средних школ Венгрии, где учились несколько лауреатов Филдсовской премии. Он окончил бакалавриат в Университете Лоранда Этвёша (Eötvös Loránd University, ELTE) в Будапеште, после чего переехал в Германию для проведения докторских исследований в Научно-исследовательском институте дискретной математики Боннского университета (Rheinische Friedrich-Wilhelms-Universität Bonn), где получил степень PhD в области прикладной и дискретной математики. Его докторская работа была сосредоточена на комбинаторных алгоритмах оптимизации для проектирования СБИС-чипов — в частности, на математических методах для временну́го синтеза и размещения, задачи на стыке теории графов и инженерии. Он работал научным ассистентом в институте с 1998 по 2005 год.

Карьера

Cadence Design Systems — Cadence Research Labs, Беркли (2005–2010)

После получения докторской степени Сегеди присоединился к Cadence Research Labs в Беркли, Калифорния, в качестве научного сотрудника. Он продолжал заниматься математической оптимизацией для автоматизации проектирования электроники (EDA), разрабатывая алгоритмы для трассировки и синтеза СБИС. Этот период дал ему обширный опыт применения строгих математических методов к масштабным инженерным задачам — подход, который впоследствии сформировал его подход как к проектированию нейроархитектур, так и к формальной верификации.

Google Brain — от инженера-программиста до штатного научного сотрудника (2010–2023)

Сегеди пришёл в Google в 2010 году, первоначально как инженер-программист, затем перейдя на исследовательские должности, достигнув статуса штатного научного сотрудника (Staff Research Scientist) к 2015 году. За более чем двенадцать лет он внёс вклад в трёх различных исследовательских фазах.

Компьютерное зрение и состязательные примеры (2012–2015). Первым крупным вкладом Сегеди в Google стало открытие, описанное в статье «Интригующие свойства нейронных сетей» („Intriguing Properties of Neural Networks“, 2013, ICLR 2014), что нейронные сети имеют неочевидные уязвимости: незаметные глазу возмущения входного изображения могут вызвать уверенную ошибочную классификацию, и эти возмущения переносятся между архитектурами, обученными на разных данных. Статья назвала такие входные данные «состязательными примерами» (adversarial examples) и впервые систематически продемонстрировала их существование, открыв область состязательного машинного обучения. Параллельно он руководил разработкой GoogLeNet (архитектура Inception v1) — глубокой свёрточной сети на основе стекируемых «модулей Inception», обрабатывающих несколько размеров рецептивных полей параллельно, что резко уменьшало количество параметров при повышении точности. GoogLeNet с большим отрывом выиграла соревнования ILSVRC 2014 по классификации и обнаружению, представив архитектурный принцип факторизованных свёрток, который повлиял на проектирование глубоких сетей на долгие годы.

Пакетная нормализация и итерации Inception (2015–2017). В сотрудничестве с Сергеем Иоффе Сегеди соизобрёл пакетную нормализацию (batch normalization, ICML 2015) — метод, нормализующий активации в мини-пакете во время обучения для уменьшения того, что они назвали «внутренним ковариатным сдвигом». Пакетная нормализация стабилизировала и резко ускорила обучение, позволила использовать более высокие скорости обучения, действовала как лёгкий регуляризатор и стала практически универсальной в глубоком обучении уже через несколько месяцев после публикации. Затем он выпустил Inception-v3 („Rethinking the Inception Architecture“, CVPR 2016) и Inception-v4 / Inception-ResNet („Inception-v4, Inception-ResNet and the Impact of Residual Connections on Learning“, AAAI 2017), которые интегрировали остаточные связи в структуру Inception. Он также внёс вклад в SSD (Single Shot MultiBox Detector, ECCV 2016) — влиятельную систему реального времени для обнаружения объектов.

Автоматическое доказательство теорем и автоформализация (2016–2023). С 2016 года Сегеди переориентировался на применение нейронных сетей в формальной математике. Статья DeepMath (NeurIPS 2016), написанная в соавторстве с командой Google Brain, была первой демонстрацией того, что большие нейронные сети могут выполнять выбор посылок (premise selection) для автоматических доказательств теорем в масштабе — обязательное условие для работы с реальными математическими библиотеками. В позиционной статье 2020 года Сегеди ввёл и формально предложил термин «автоформализация» (autoformalization) — процесс автоматического перевода естественно-языковой математики в машинно-верифицируемые формальные спецификации — как долгосрочную исследовательскую программу. Статья на NeurIPS 2022 с Юхаем Ву (Yuhuai Wu) и коллегами показала, что большие языковые модели уже могут автоформализовать значительную часть задач олимпиадной математики в Isabelle/HOL, установив новый бенчмарк на MiniF2F.

xAI — сооснователь (2023)

В марте 2023 года Сегеди был назван среди основателей компании xAI, Илона Маска, вместе с Игорем Бабушкиным (Igor Babuschkin), Юхаем Ву, Кайлом Косичем (Kyle Kosic) и другими. Его основным фокусом в xAI были рассуждения и формальные методы, что соответствовало направлению исследований, установленному им в Google. Он покинул компанию в 2024 году, до её наиболее заметных публичных запусков продуктов.

Morph Labs — главный научный сотрудник (2024)

После ухода из xAI Сегеди стал главным научным сотрудником Morph Labs, продукто-исследовательской лаборатории в Сан-Франциско, создающей автономных программных инженерных агентов. Эта роль была переходной; он ушёл, чтобы основать собственную компанию, сосредоточенную на формальной математике.

Math Inc (Math Incorporated) — основатель (2025–настоящее время)

Сегеди основал Math Inc для создания инфраструктуры верифицированных рассуждений ИИ в масштабе. Флагманская система компании, Gauss, предназначена для генерации машинно-проверяемых математических доказательств и, по сообщениям, примерно за две недели сгенерировала доказательство, которое, по оценкам экспертов-людей, заняло бы год. Он также основал отдельную компанию в Венгрии, занимающуюся образованием с использованием ИИ, движимый желанием принести инструменты обучения с ИИ в контексты, где такие ресурсы исторически были дефицитны. Сегеди публично отстаивает тезис о том, что именно автоформализация — а не поведенческое согласование (alignment) — является правильной основой для надёжного ИИ: если все рассуждения ИИ могут быть выражены в виде машинно-проверяемых формальных доказательств, вопрос о том, является ли система «безопасной», становится математической задачей верификации, а не эмпирической.

Ключевые вклады

  • Состязательные примеры („Intriguing Properties of Neural Networks“, ICLR 2014) — Первое систематическое открытие и описание состязательных входных данных: минимальные, незаметные для человека возмущения, которые вызывают уверенно неверные предсказания нейронной сети и, что критично, переносятся между архитектурами. Статья основала подобласть состязательного машинного обучения, породив тысячи последующих работ как по атакам, так и по защите.

  • GoogLeNet / Архитектура Inception (CVPR 2015) — „Going Deeper with Convolutions“. Представлен модуль Inception, применяющий свёртки с несколькими размерами фильтров параллельно и объединяющий их выходы, что позволяет создавать гораздо более глубокие сети со значительно меньшим количеством параметров. GoogLeNet выиграла ILSVRC 2014, имея примерно в 12 раз меньше параметров, чем AlexNet, при повышении точности; принципы проектирования архитектуры повлияли на последующие семейства, включая Inception-v2–v4, и повлияли на EfficientNet.

  • Пакетная нормализация (ICML 2015) — „Batch Normalization: Accelerating Deep Network Training by Reducing Internal Covariate Shift“ совместно с Сергеем Иоффе. Продемонстрировала, что нормализация активаций слоёв по мини-пакетам обучения позволяет обучаться в 14 раз быстрее до эквивалентной точности, обеспечивает более высокие скорости обучения и неявную регуляризацию. Стала одним из самых универсальных методов в глубоком обучении, появившись практически во всех основных архитектурах после 2015 года.

  • DeepMath (NeurIPS 2016) — „DeepMath — Deep Sequence Models for Premise Selection“. Первое масштабное демонстрирование того, что глубокие нейронные сети могут эффективно помогать автоматическим средствам доказательства теорем, выбирая релевантные леммы из больших математических библиотек — ключевое узкое место в автоматическом поиске доказательств. Установило жизнеспособность формальной математики с помощью машинного обучения.

  • Inception-v3 / v4 и Inception-ResNet (CVPR 2016, AAAI 2017) — Продолжение систематической разработки семейства Inception с введением факторизованных свёрток, сглаживания меток (label smoothing) и интеграции с остаточными связями, создав архитектуры, остававшиеся современными базовыми линиями в течение нескольких лет.

  • Автоформализация (предложена в 2020; NeurIPS 2022) — Предложена и названа исследовательская программа автоформализации: использование ИИ для автоматического перевода естественно-языковой математики на формальные языки доказательств, такие как Lean, Isabelle или Coq. Статья на NeurIPS 2022 (совместно с Юхаем Ву и др.) продемонстрировала, что большие языковые модели могут корректно формализовать 25,3% олимпиадных задач в Isabelle/HOL, установив большие языковые модели как практические инструменты для этой задачи и улучшив бенчмарк доказательства теорем MiniF2F с 29,6% до 35,2%.

Награды и признание

  • Победитель ILSVRC 2014 — GoogLeNet выиграла как трек классификации, так и трек обнаружения в ImageNet Large Scale Visual Recognition Challenge 2014, самом популярном на тот момент бенчмарке компьютерного зрения.
  • Наследие состязательных примеров — Статья „Intriguing Properties“ и её непосредственное продолжение („Explaining and Harnessing Adversarial Examples“, ICLR 2015, с Яном Гудфеллоу (Ian Goodfellow) и Джонатаном Шленсом (Jonathon Shlens)) входят в число наиболее цитируемых работ по безопасности и робастности ИИ; состязательное машинное обучение теперь является крупной подобластью.
  • Прогноз о золотой медали Международной математической олимпиады (de facto подтверждён, 2025) — Сегеди сделал публичный прогноз, что ИИ достигнет уровня золотой медали на Международной математической олимпиаде к 2026 году; модель Gemini от Google DeepMind достигла этого стандарта на IMO 2025, в целом подтвердив временные рамки.

Ключевые связи

  • Сергей Иоффе (Sergey Ioffe) — Самый близкий исследовательский коллаборатор в Google Brain; соизобретатель пакетной нормализации и соавтор статей по Inception-v4 и Inception-ResNet. Работа Иоффе и Сегеди породила две статьи, изменившие практику обучения глубокому обучению.
  • Ян Гудфеллоу (Ian Goodfellow) — Соавтор статьи «Explaining and Harnessing Adversarial Examples» (ICLR 2015), сопутствующей работы, давшей теоретическое объяснение уязвимости, открытой Сегеди; тогда Гудфеллоу был научным сотрудником Google Brain.
  • Юхай (Тони) Ву (Yuhuai (Tony) Wu) — Давний соавтор исследований по формальным математическим рассуждениям в Google Research; соавтор статьи по автоформализации 2022 года и сооснователь xAI вместе с Сегеди.
  • Илон Маск (Elon Musk) — Сооснователь xAI в 2023 году; компания объединила команду с общими амбициями в области крупномасштабного ИИ для рассуждений.
  • Йенс Виген (Jens Vygen) — Научный руководитель в Научно-исследовательском институте дискретной математики Боннского университета в годы докторантуры Сегеди; традиции комбинаторной оптимизации этой группы сформировали математически строгий подход Сегеди к проектированию алгоритмов.
  • Франсуа Шолле (François Chollet) — Публичный собеседник по срокам возможностей ИИ; у них есть текущее публичное пари о сроках достижения сверхчеловеческого математического ИИ, причём Сегеди придерживается оптимистичного краткосрочного взгляда.
  • Винсент Ванхуке (Vincent Vanhoucke) — Коллега по Google Brain и соавтор нескольких статей по Inception.

Личный стиль

Исследовательский стиль Сегеди определяется приверженностью математической строгости, которая сохранялась в трёх совершенно разных технических областях: дискретная оптимизация для проектирования чипов, систематические исследования архитектур и регуляризации в глубоком обучении и теперь формальная верификация рассуждений ИИ. Он подходит к проблемам, ища принципиальные, механистические объяснения — работа с состязательными примерами характерна: вместо того чтобы рассматривать хрупкость как досадную помеху, он отнёсся к ней как к явлению, требующему формального объяснения. Его нынешний тезис о том, что автоформализация является основополагающей технологией для безопасного сверхинтеллекта, является прямым продолжением этой склонности: если рассуждения ИИ не могут быть выражены как машинно-проверяемое доказательство, им нельзя доверять, независимо от того, насколько впечатляющими они кажутся. Он говорит о долгосрочной траектории математики и ИИ с необычной конкретностью, делая фальсифицируемые публичные прогнозы с конкретными временными рамками, и основал компании как в США, так и в Венгрии, чтобы действовать в соответствии с этими убеждениями, а не просто публиковать о них.

Ссылки