Forwarded from Machinelearning
Суть задачи простая: есть
n точек на плоскости. Нужно понять, сколько пар точек могут находиться ровно на расстоянии 1 друг от друга.Долгое время считалось, что почти оптимальный ответ дают конструкции, похожие на квадратную решётку. Модель OpenAI показала, что это неверно.
Она построила бесконечное семейство конфигураций, где таких пар получается заметно больше, чем ожидалось. То есть была опровергнута не мелкая техническая деталь, а известная гипотеза, вокруг которой десятилетиями строились оценки.
Модель связала задачу о точках на плоскости с алгебраической теорией чисел.
В доказательстве используются решётки Минковского (способ превратить числа из алгебраической теории чисел в точки в обычном евклидовом пространстве), элементы нормы один и pro-3 башни числовых полей. Это инструменты из другой части математики, и именно их перенос в геометрию дал результат.
Нога Алон из Принстона отметил, что ответ оказался неожиданным, а применённые методы выглядят элегантно и нетривиально.
При этом доказательство не даёт нового «чисто геометрического» метода, на который многие надеялись. Гипотеза опровергнута, но сама структура задачи стала ещё интереснее.
Задачу сформулировал ИИ, решение сгенерировала внутренняя модель OpenAI, первичная проверка тоже прошла через автоматический ИИ-пайплайн. После этого люди проверили детали, улучшили изложение и довели работу до публикации.
Модель сама нашла неочевидную связь между разными областями математики и получила результат по открытой задаче высокого уровня.
Оригинал: https://openai.com/index/model-disproves-discrete-geometry-conjecture/
@ai_machinelearning_big_data
Please open Telegram to view this post
VIEW IN TELEGRAM
Please open Telegram to view this post
VIEW IN TELEGRAM
❤10👍6🔥2
Гамильтон, о котором не пишут в хайповых СМИ, а без него не было бы ни квантовых компьютеров, ни современного ML
Имя Уильяма Роуэна Гамильтона редко стоит рядом с Ньютоном и Эйнштейном в популярных подборках, но именно его математика стала рабочим языком всей современной физики и значительной части data science. Если вы когда-нибудь обучали нейросеть, моделировали динамическую систему или хотя бы запускали Hamiltonian Monte Carlo в Stan или PyMC, вы пользовались идеями, заложенными Гамильтоном почти двести лет назад.
В начале 1800-х механика жила по законам Ньютона. Они работали, но на практике быстро становились громоздкими: связанные тела, нестандартные системы координат, ограничения на движение. Гамильтон предложил другую оптику. Вместо того чтобы каждый раз расписывать силы, он перешёл к описанию системы через обобщённые координаты и одну ключевую функцию, которую сегодня называют гамильтонианом.
Гамильтониан это полная энергия системы, кинетическая плюс потенциальная. Из него выводятся уравнения движения, которые показывают, как одновременно меняются положение и импульс. Эта формулировка унифицировала механику, оптику и небесную динамику, а главное, оказалась пригодной для гораздо большего, чем рассчёты планет и маятников.
Через сто лет физики обнаружили, что именно гамильтонов формализм идеально ложится на квантовую механику. Уравнение Шрёдингера, на котором стоит вся квантовая физика, выводится напрямую из идей Гамильтона. По сути, любой современный кубит, любой разговор про квантовое превосходство и любая статья по quantum machine learning опирается на гамильтониан как на базовую конструкцию.
Для инженеров и AI-специалистов это не просто красивая историческая справка. Гамильтонова механика стоит за целым семейством инструментов, которые сегодня в продакшене. Hamiltonian Monte Carlo лежит в основе многих современных байесовских фреймворков и активно используется для обучения вероятностных моделей. Hamiltonian Neural Networks учат сеть сохранять физические инварианты, что критично в задачах симуляции и робототехники. Symplectic integrators применяются там, где нужно стабильно прогонять долгие траектории, от молекулярной динамики до обучения с подкреплением.
Главный урок здесь не математический, а методологический. Гамильтон не пытался опровергнуть Ньютона, он переформулировал ту же физику так, чтобы с ней было удобно работать в новых контекстах. Ровно это сегодня делают сильные ML-инженеры, когда берут хорошо известную задачу и переписывают её в терминах, которые лучше ложатся на современное железо и алгоритмы. Гамильтон, по сути, дал нам шаблон: правильная переформулировка важнее новой теории.
Имя Уильяма Роуэна Гамильтона редко стоит рядом с Ньютоном и Эйнштейном в популярных подборках, но именно его математика стала рабочим языком всей современной физики и значительной части data science. Если вы когда-нибудь обучали нейросеть, моделировали динамическую систему или хотя бы запускали Hamiltonian Monte Carlo в Stan или PyMC, вы пользовались идеями, заложенными Гамильтоном почти двести лет назад.
В начале 1800-х механика жила по законам Ньютона. Они работали, но на практике быстро становились громоздкими: связанные тела, нестандартные системы координат, ограничения на движение. Гамильтон предложил другую оптику. Вместо того чтобы каждый раз расписывать силы, он перешёл к описанию системы через обобщённые координаты и одну ключевую функцию, которую сегодня называют гамильтонианом.
Гамильтониан это полная энергия системы, кинетическая плюс потенциальная. Из него выводятся уравнения движения, которые показывают, как одновременно меняются положение и импульс. Эта формулировка унифицировала механику, оптику и небесную динамику, а главное, оказалась пригодной для гораздо большего, чем рассчёты планет и маятников.
Через сто лет физики обнаружили, что именно гамильтонов формализм идеально ложится на квантовую механику. Уравнение Шрёдингера, на котором стоит вся квантовая физика, выводится напрямую из идей Гамильтона. По сути, любой современный кубит, любой разговор про квантовое превосходство и любая статья по quantum machine learning опирается на гамильтониан как на базовую конструкцию.
Для инженеров и AI-специалистов это не просто красивая историческая справка. Гамильтонова механика стоит за целым семейством инструментов, которые сегодня в продакшене. Hamiltonian Monte Carlo лежит в основе многих современных байесовских фреймворков и активно используется для обучения вероятностных моделей. Hamiltonian Neural Networks учат сеть сохранять физические инварианты, что критично в задачах симуляции и робототехники. Symplectic integrators применяются там, где нужно стабильно прогонять долгие траектории, от молекулярной динамики до обучения с подкреплением.
Главный урок здесь не математический, а методологический. Гамильтон не пытался опровергнуть Ньютона, он переформулировал ту же физику так, чтобы с ней было удобно работать в новых контекстах. Ровно это сегодня делают сильные ML-инженеры, когда берут хорошо известную задачу и переписывают её в терминах, которые лучше ложатся на современное железо и алгоритмы. Гамильтон, по сути, дал нам шаблон: правильная переформулировка важнее новой теории.
🔥17❤10✍2🥰1
Гений, который послал на три буквы миллион долларов и Принстон: 7 фактов про Григория Перельмана
В мире, где айтишники прыгают между офферами ради лишних 20 тысяч долларов к зарплате, а топ-исследователи ИИ подписывают контракты с девятью нулями, существует человек, который однажды посмотрел на чек в миллион долларов и сказал: «Мне это не нужно». Григорий Перельман, питерский математик, который доказал то, над чем человечество ломало голову сто лет, а потом просто ушёл из науки. Для тех, кто строит языковые модели, обучает нейросети и спорит про AGI, история Перельмана это полезное напоминание о том, что бывает с людьми, которые ставят чистую идею выше любых KPI и грантов.
Гипотеза Пуанкаре сто лет считалась одной из самых сложных задач в математике. Это одна из семи «задач тысячелетия», за решение которых Институт Клэя в 2000 году объявил награду в миллион долларов за каждую. В 2002 и 2003 годах Перельман выложил на arXiv три препринта, в которых, не претендуя ни на что, аккуратно решил гипотезу. Без громких пресс-релизов, без университетской аффилиации к моменту окончания работы, без раздутых тредов. Просто PDF-ки в открытом доступе.
7 фактов о Григории Перельмане, которые стоит знать каждому айтишнику и исследователю ИИ.
Первое. Он закрыл столетнюю задачу. Перельман доказал гипотезу Пуанкаре, одну из самых известных нерешённых проблем в математике XX века.
Второе. Он отказался от миллиона долларов. Перельман отклонил премию Института Клэя, объяснив это тем, что не хочет быть «выставленным напоказ как зверь в зоопарке».
Третье. Он отказался от Филдсовской премии. В 2006 году он отверг высшую награду в математике, заявив, что не заинтересован в признании.
Четвёртое. Он ушёл из математики. После доказательства гипотезы он покинул академию и пропал из публичного поля.
Пятое. Он переиграл лучшие умы. Его доказательство было настолько глубоким, что научному сообществу понадобилось около четырёх лет, чтобы окончательно его верифицировать.
Шестое. Он отказал топовым университетам. Принстон, Стэнфорд и другие пытались его пригласить, но он отверг все предложения.
Седьмое. Он живёт в почти полной изоляции. По имеющимся данным, он живёт в небольшой квартире в Санкт-Петербурге с матерью и избегает медиа и публичности.
https://uproger.com/genij-kotoryj-poslal-na-tri-bukvy-million-dollarov-7-faktov-pro-perelmana/
В мире, где айтишники прыгают между офферами ради лишних 20 тысяч долларов к зарплате, а топ-исследователи ИИ подписывают контракты с девятью нулями, существует человек, который однажды посмотрел на чек в миллион долларов и сказал: «Мне это не нужно». Григорий Перельман, питерский математик, который доказал то, над чем человечество ломало голову сто лет, а потом просто ушёл из науки. Для тех, кто строит языковые модели, обучает нейросети и спорит про AGI, история Перельмана это полезное напоминание о том, что бывает с людьми, которые ставят чистую идею выше любых KPI и грантов.
Гипотеза Пуанкаре сто лет считалась одной из самых сложных задач в математике. Это одна из семи «задач тысячелетия», за решение которых Институт Клэя в 2000 году объявил награду в миллион долларов за каждую. В 2002 и 2003 годах Перельман выложил на arXiv три препринта, в которых, не претендуя ни на что, аккуратно решил гипотезу. Без громких пресс-релизов, без университетской аффилиации к моменту окончания работы, без раздутых тредов. Просто PDF-ки в открытом доступе.
7 фактов о Григории Перельмане, которые стоит знать каждому айтишнику и исследователю ИИ.
Первое. Он закрыл столетнюю задачу. Перельман доказал гипотезу Пуанкаре, одну из самых известных нерешённых проблем в математике XX века.
Второе. Он отказался от миллиона долларов. Перельман отклонил премию Института Клэя, объяснив это тем, что не хочет быть «выставленным напоказ как зверь в зоопарке».
Третье. Он отказался от Филдсовской премии. В 2006 году он отверг высшую награду в математике, заявив, что не заинтересован в признании.
Четвёртое. Он ушёл из математики. После доказательства гипотезы он покинул академию и пропал из публичного поля.
Пятое. Он переиграл лучшие умы. Его доказательство было настолько глубоким, что научному сообществу понадобилось около четырёх лет, чтобы окончательно его верифицировать.
Шестое. Он отказал топовым университетам. Принстон, Стэнфорд и другие пытались его пригласить, но он отверг все предложения.
Седьмое. Он живёт в почти полной изоляции. По имеющимся данным, он живёт в небольшой квартире в Санкт-Петербурге с матерью и избегает медиа и публичности.
https://uproger.com/genij-kotoryj-poslal-na-tri-bukvy-million-dollarov-7-faktov-pro-perelmana/
❤18🤯5💩2
Forwarded from Machinelearning
🔥 AlphaProof Nexus: формальные доказательства начинают превращаться в инженерный пайплайн
Google DeepMind показали AlphaProof Nexus - систему, которая автономно закрыла 9 открытых задач Эрдёша, часть из которых висела десятилетиями. По оценке авторов, стоимость решения одной задачи составила всего несколько сотен долларов.
Кроме этого, система доказала 44 открытые гипотезы из OEIS, закрыла 15-летний вопрос в алгебраической геометрии и нашла новый алгоритмический параметр в оптимизационной теории, который раньше не был описан людьми.
Модель генерирует идеи и фрагменты доказательств, а Lean проверяет каждый логический шаг через компилятор. Если доказательство некорректно, оно просто не проходит проверку. Не нужен рецензент, который вручную ищет дыру в рассуждении.
Базовый агент, который просто чередует генерацию LLM и обратную связь от компилятора, смог повторить все 9 успешных решений задач Эрдёша. Более сложная версия с эволюционным поиском и reinforcement learning дала заметный выигрыш только на самых тяжёлых случаях.
Чем сильнее становятся foundation models, тем чаще простые циклы «сгенерировал - проверил - исправил» начинают догонять специализированные архитектуры.
Отличие от неформального подхода к математическим доказательствам принципиальное. Модель часто придумывала несуществующие леммы, ссылалась на «известные результаты» и пыталась спрятать сложность задачи в вспомогательное утверждение. В обычном текстовом доказательстве такие ошибки легко пропустить. Lean отсекает их сразу.
Ещё один неожиданный эффект: агент находил неточности в формализациях уже существующих математических утверждений. То есть он работал не только как решатель, но и как диагностический инструмент для самой постановки задачи.
Успехи пока сосредоточены там, где библиотека Lean уже достаточно зрелая: комбинаторика, теория чисел, оптимизация. Задачи, где нужно строить большой пласт новой теории, всё ещё далеко не закрыты. И большинство задач Эрдёша система не решила.
Та же схема подходит для кодигша, спецификаций, верификации протоколов, компиляторов, криптографии.
Формальная проверка отсекает галлюцинации.
Модель может придумать лемму или сослаться на несуществующий результат, но Lean это не пропустит.
https://arxiv.org/html/2605.22763v1
@ai_machinelearning_big_data
Google DeepMind показали AlphaProof Nexus - систему, которая автономно закрыла 9 открытых задач Эрдёша, часть из которых висела десятилетиями. По оценке авторов, стоимость решения одной задачи составила всего несколько сотен долларов.
Кроме этого, система доказала 44 открытые гипотезы из OEIS, закрыла 15-летний вопрос в алгебраической геометрии и нашла новый алгоритмический параметр в оптимизационной теории, который раньше не был описан людьми.
Модель генерирует идеи и фрагменты доказательств, а Lean проверяет каждый логический шаг через компилятор. Если доказательство некорректно, оно просто не проходит проверку. Не нужен рецензент, который вручную ищет дыру в рассуждении.
Базовый агент, который просто чередует генерацию LLM и обратную связь от компилятора, смог повторить все 9 успешных решений задач Эрдёша. Более сложная версия с эволюционным поиском и reinforcement learning дала заметный выигрыш только на самых тяжёлых случаях.
Чем сильнее становятся foundation models, тем чаще простые циклы «сгенерировал - проверил - исправил» начинают догонять специализированные архитектуры.
Отличие от неформального подхода к математическим доказательствам принципиальное. Модель часто придумывала несуществующие леммы, ссылалась на «известные результаты» и пыталась спрятать сложность задачи в вспомогательное утверждение. В обычном текстовом доказательстве такие ошибки легко пропустить. Lean отсекает их сразу.
Ещё один неожиданный эффект: агент находил неточности в формализациях уже существующих математических утверждений. То есть он работал не только как решатель, но и как диагностический инструмент для самой постановки задачи.
Успехи пока сосредоточены там, где библиотека Lean уже достаточно зрелая: комбинаторика, теория чисел, оптимизация. Задачи, где нужно строить большой пласт новой теории, всё ещё далеко не закрыты. И большинство задач Эрдёша система не решила.
Та же схема подходит для кодигша, спецификаций, верификации протоколов, компиляторов, криптографии.
Формальная проверка отсекает галлюцинации.
Модель может придумать лемму или сослаться на несуществующий результат, но Lean это не пропустит.
https://arxiv.org/html/2605.22763v1
@ai_machinelearning_big_data
🔥5❤3👍3
NVIDIA официально опубликовала Skills, которые они используют для своих ИИ-агентов.
Прямо сейчас у них есть Skills для:
→ автоматического анализа и суммирования видео
→ создания голосовых агентов в реальном времени
→ обучения и улучшения LLM
→ ускорения моделей, чтобы они работали намного быстрее
→ систем RAG, подключенных к документам и данным
→ агентов, работающих в изолированных безопасных средах
→ оптимизации логистики и маршрутизации с помощью GPU
→ программирования и вычислений на CUDA
Некоторые из самых интересных:
• TensorRT-LLM → экстремальное ускорение LLM
• NeMo-RL → продвинутое обучение агентов
• Video Search → автоматический поиск и суммирование видео
Кроме того, они совместимы с:
→ Claude Code
→ OpenAI Codex
→ Cursor
https://github.com/NVIDIA/skills
Прямо сейчас у них есть Skills для:
→ автоматического анализа и суммирования видео
→ создания голосовых агентов в реальном времени
→ обучения и улучшения LLM
→ ускорения моделей, чтобы они работали намного быстрее
→ систем RAG, подключенных к документам и данным
→ агентов, работающих в изолированных безопасных средах
→ оптимизации логистики и маршрутизации с помощью GPU
→ программирования и вычислений на CUDA
Некоторые из самых интересных:
• TensorRT-LLM → экстремальное ускорение LLM
• NeMo-RL → продвинутое обучение агентов
• Video Search → автоматический поиск и суммирование видео
Кроме того, они совместимы с:
→ Claude Code
→ OpenAI Codex
→ Cursor
https://github.com/NVIDIA/skills
🔥6👍1🥰1