OpenAI доказала гипотезу о Navier-Stokes за 17 часов — раньше на это ушли бы годы
The part of Navier-Stokes no one is talking about
OpenAI объявила о доказательстве давней проблемы уравнений Navier-Stokes и одновременно с человекочитаемым доказательством выложила формальное доказательство на Lean 4. Если раньше формализация одной страницы учебника занимала около 40 часов, то проверка 166-страничной статьи в Lean заняла у OpenAI всего 17 часов. Это снижение трудозатрат на четыре порядка делает формальную верификацию реальной не только для математики, но и для безопасности, смарт-контрактов и критичных алгоритмов.
Я не решаюсь использовать слово «революционный», но снижение стоимости чего угодно на четыре порядка — это революция.
- stabbles
Забавно осознавать, что Lean, судя по всему, настолько медленный, что для проверки доказательства Великой теоремы Ферма он работает всего на один порядок быстрее, чем агенты могли бы сгенерировать код на Lean (15 часов проверки с 230 ГБ оперативной памяти против 11 дней на генерацию).
Насколько вообще можно оптимизировать Lean? Он должен быть достаточно простым для аудита — означает ли это, что нельзя использовать непрозрачные оптимизации, чтобы ускорить его работу?
- parhamn
Они оценили затраты на агентов в $40 млн (это был большой флот агентов). Если использовать цифру из поста, то для человеческого случая получается ближе к ~880 000 часов × $150/час = $132 миллиона. Всё равно потрясающее достижение, но не совсем «четыре порядка». Сравнение, очевидно, бессмысленно, потому что скоординировать 1 миллион часов интеллектуального труда — это, мягко говоря, непросто.
Очень захватывающие и неопределённые времена!
- boshalfoshal
Кажется, люди обсуждают всё что угодно, кроме собственно результатов этого конкретного анонса.
Всё ещё поразительно, что какая-либо обобщённая компьютерная программа способна решить задачу такого масштаба, и мы наблюдали это в реальном времени. Мне было бы интересно узнать, может ли новая модель также делать более прямые доказательства/индуктивные доказательства.
- pkal
ИМХО, правило «сорок часов на страницу» устарело и является скорее следствием нехватки автоматизации доказательств в 2005 году. Насколько я понимаю Lean, это одна из тех вещей, над улучшением которых они приложили много усилий, делая механизацию доказательств более приемлемой для математически настроенных людей, а не только для логиков.
- lordnacho
Откуда вы знаете, что он формализует именно то, что вы думаете? Если в вашем Lean 4 есть баг, разве вы не докажете что-то другое, не то, что имели в виду?
- 3m4r
Не обязательно применительно к решению OpenAI для Навье-Стокса, но что произойдёт, если и когда ИИ действительно, как кажется, решит чрезвычайно сложную задачу, но люди не смогут независимо проверить решение, потому что для понимания доказательства/аргумента требуется интеллект, которого у проверяющих биологически нет, или ресурсы, чтобы позволить себе использовать автоматизированные инструменты?
Мы уже видели свидетельства в дикой природе, как агенты пытаются обойти выполнение реальной работы в бенчмаркинге (то есть просто украсть ключ с ответами) из-за кажущейся экономии от читерства для получения результатов. Что произойдёт, если или когда у нас больше не будет возможности фактически обнаружить либо читерство ИИ, либо просто неверный ответ? Что произойдёт, если будет долгоиграющая атака социальной инженерии (вроде попытки захвата XZ) на что-то вышестоящее от ключевого инструмента (или его зависимостей) для формальной верификации, и у нас не будет доверенной вычислительной базы?
Что было бы дешевле и более прямым путём, особенно в долгосрочной перспективе? Тем, кто пытается построить несокрушимый замок, нужно защищать тысячи потенциальных брешей; атакующему достаточно найти лишь одну.
- zem
Не хочу умалять признательность автора за недавно ставшие доступными формальные доказательства, но люди говорили об экономии усилий на формализацию дольше, чем об ИИ, выполняющем сами доказательства!
- aabhay
Формализация доказательств в Lean стала значительно проще по сравнению с формализациями, доступными в 2005 году. А mathlib в Lean проделал большую часть базовой работы, так что у вас уже встроены аксиомы и необходимые леммы. Вы можете мыслить в терминах стандартных абстракций, которые очень похожи на точные обозначения из учебника для бакалавриата.
Тем не менее, я никоим образом не пытаюсь принизить, насколько невероятным достижением является формализация алгоритма, выигравшего премию тысячелетия, на Lean. Просто взгляните на код, который опубликовал OpenAI. Это как энциклопедия различных концепций гидродинамики.