Комментарии 56
Впечатляющее достижение, что тут говорить - формализовать теорему Ферма не каждый день увидишь. Но я, как человек, который сам запускал проекты на нейросетях, сразу задаюсь вопросом: какая реальная ценность за этим стоит? И сколько стоили эти 1000 агентов, работающих 30 часов? Пока это похоже на дорогую демонстрацию возможностей, а не на инструмент с понятной юнит-экономикой или реальным спросом на рынке. Мне всегда интересно, как такая мощь конвертируется в окупаемость.
Это наука. Часто дорого и не факт, что пригодится.
Если брать Великую Теорию Ферма, то она бесполезная для практике. Но ради нее было придумано хороших технологий и тому подобное.
Теорема красивая значимая и поэтому на ней довольно логично проводить вещи.
Если наладить процесс, то можно те же заработки применить на другие задачи, с практической выгодой. Ну пример, малая теорема Ферма основа криптографии.
Эвристической ценности хотелось бы... а тут предлагают очередной Монте-Карло. Практическая польза, конечно, есть, но съеденным чижиком отдает.
Конкретно это - не наука, это поддержание информационного фона и нагон хайпа перед IPO, как раз ради того чтобы потенциальные лохи инвесторы думали как вы, а не как гражданин которому вы отвечаете.
Так сказать, фрейминг мышления - думайте о классных демках, "прорывах" и невероятных будущих перспективах, а не о том сколько это стоит, что за продукт вам продают, какие гарантии его функционирования вы получаете и как вообще этот продукт может быть вам полезен, если он вообще вам полезен.
Как только ранние инвестора выведут деньги после IPO вся эта карусель "открытий", "взломов" и прочих чудес немедленно прекратится.
Это наука. Часто дорого и не факт, что пригодится.
А что тут может пригодиться? Само доказательство и так должно быть полностью формализовано (иначе это и не доказательство). Его просто на служебный язык перенесли...
Как это "что может пригодиться"? В математике постоянно так происходит, что то, что сейчас кажется бесполезным, потом находит применение, как и в науке в целом. Тут идет отработка перевода неформализованных математических описаний в формализованное Lean описание, как я понимаю. Процесс нетривиальный. Все эти наработки могут быть использованы в других доказательствах, расширяя покрытие, созодавая новые библиотеки. Полагаете, это не нужно?
Это не математика! Это прикладное программирование. И какая тут "наработка"? Чего? Дали промт и получили формализацию?
Само доказательство и так должно быть полностью формализовано (иначе это и не доказательство)
Это не так. Математическое доказательство пишется для людей, на обычном нестрогом языке со ссылками на что-то, что многим очевидно, на прошлые доказательства со множеством допущений, логических переходов. Для проверки нужно множество математиков и определённый консенсус между ними. Подразумеваемые понятия тоже не определены формально так, чтобы автоматически следовало доказательство. Проверять доказательства могут годами. Для этого на Lean постепенно всё и переводят, но ручной процесс был очень медленным, и никакие системы кроме LLM не могли распознавать неформальный язык и всякие ссылки на прошлое знание. Lean описывает строгие программы, хотя даже в нём могут быть ошибки или ошибки перевода.
И какая тут "наработка"? Чего? Дали промт и получили формализацию?
Почитайте хоть про Lean, его библиотеки, сложность формализации и почему за годы его существования не так много на него переведено было. Чем больше в Lean библиотек, чем больше областей математики покрыто, тем проще доказывать новые вещи. Нейросетям тоже будет проще обучаться логике и формализованным доказательствам на Lean программах, чем на человеческих текстах. Рано или поздно просто на него перейдут, думаю, не мучая сообщество утомительной перепроверкой.
Кроме того, тут пример согласованной работы роя агентов. Они там сами создали PostreSQL таблицы для координации доказательства. Такое и для других научных исследований будет полезно.
Математическое доказательство пишется для людей
Я никак в толк не возьму - в чём разница?
на обычном нестрогом языке со ссылками на что-то, что многим очевидно
Это так работать не должно)) Это даже на Хабре не работает - "ну это очевидно". Есть строгая аксиоматика и есть следствия из неё. Да, это может быть долго - но а как иначе? Нейросетевую формализацию тоже надо проверять будет!
Подразумеваемые понятия тоже не определены формально так, чтобы автоматически следовало доказательство
А должны быть определены. Или как - "ну тут имеется в виду что-то типа такого..."? А автоматическое доказательство вообще не обязано следовать из этого.
Для этого на Lean постепенно всё и переводят
Ну т.е. вот тот самый "определённый консенсус множества математиков"?
Рано или поздно просто на него перейдут, думаю, не мучая сообщество утомительной перепроверкой.
Вот спасибо! Последняя сфера где хотелось бы видеть нейросети))
Кроме того, тут пример согласованной работы роя агентов.
Вообще не ново.
Последняя сфера где хотелось бы видеть нейросети))
почему?
и да, вам не хочется видеть, а другим хочется. что делать?
почему?
Потому что работа со строжайшей формальной логикой идёт через "вероятностную систему" - странно, что подобное тут приходится разжёвывать...
и да, вам не хочется видеть, а другим хочется. что делать?
Ничего. Работайте ;)
Ну, вот если честно даже не знаю как вести дискуссию. Я был тоже далёк от темы, я не математик. Но я поизучал вопрос, что такое Lean, для чего он нужен, чем сейчас заняты ведущие математики для которых он основной рабочий инструмент. Не хочу делать умный вид и всё это пересказывать, когда любой может разобраться самостоятельно. Но вы почему-то считаете себя спецом в математике, хотя явно таковым не являетесь и пишете как должно быть, а как не должно быть.
Ну, вот если честно даже не знаю как вести дискуссию.
Конструктивно. По тезисам. Которые я явно выписываю. Без перехода на личности. Не пробовали? ;)
Не хочу делать умный вид и всё это пересказывать, когда любой может разобраться самостоятельно.
И не делайте. И домыслы свои можно при себе оставить ;)
Но вы почему-то считаете себя спецом в математике, хотя явно таковым не являетесь и пишете как должно быть, а как не должно быть.
Ну вроде давно на Хабре. Это по вашему аргументация? Апелляция к ad hominem? Зачем тогда эта новость вообще тут, если её должны обсуждать только математики с соответствующим профилем???
А главное, зачем вы её тогда обсуждаете, если
Я был тоже далёк от темы, я не математик.
Что по сути дискуссии вы хотели сказать, кроме "явно таковым не являетесь"?
UPD: Пьер Ферма, к слову, тоже не был "профессиональным математиком". Ваш критерий отсекает автора теоремы, которую вы обсуждаете))
Формализация чего-либо в системе интерактивных доказательств, это задача на стыке математики и программирования. Одной из целей является развитие и улучшение самих систем интерактивных доказательств теорем.
Попытка формализации в Lean, это одновременно проверка пригодности Lean для анализа данной математической проблемы. И если формализовать не получается, то всегда возникает вопрос - в чем причина? Это ошибка математика, или ошибка программиста, или ограничение самой системы? Если формализовать математическую проблему не удается, то это может означать что сама система Lean требует изменений и дополнений.
Так что вопрос здесь не “зачем подтверждать конкретно теорему Ферма”, а более общий - “зачем нужны системы интерактивных доказательств теорем”, и какие у них перспективы практического применения? Приведет ли их развитие к созданию универсальной электронной системы, которая заменит всех математиков?
Так что вопрос здесь не “зачем подтверждать конкретно теорему Ферма”
Именно в этом. Потому что вопрос тут - "что такого может доказательство ВТФ, чего не может любое другое доказательство?".
Проверили? Работает? Отлично. Как дальше будем это использовать? Проверять на следующей? Плюс неплохо бы проверить саму корректность формализации, а не кивать автоматически "нейросеть смогла".
Одной из целей является развитие и улучшение самих систем интерактивных доказательств теорем.
Звучит, как по мне, довольно обтекаемо и пафосно. Скорее "демонстрация возможностей нейросетей". Потому что не сегодня-завтра, эту прослойку в виде "системы интерактивного доказательства" возьмут и выкинут за ненадобностью))
ЛЛМ как раз может стать перспективным дополнением к системе интерактивных доказательств теорем. Для преобразования текстового доказательства в код. Для подробного комментирования формул и кода. Для графического представления.
прослойку в виде “системы интерактивного доказательства” возьмут и выкинут за ненадобностью
Тоже вариант эволюции. Но сначала модели должны научится “мыслить” на уровне строгих алгоритмов. Вернее должна быть связка “ЛЛМ-модель + алгоритмическая модель”. В нынешние ЛЛМ-модели строгое алгоритмическое ядро не встраивается, из-за самого принципа обучения.
Для преобразования текстового доказательства в код.
Проверять её кто будет? Потому что сами же пишете:
Но сначала модели должны научится “мыслить” на уровне строгих алгоритмов. Вернее должна быть связка “ЛЛМ-модель + алгоритмическая модель”. В нынешние ЛЛМ-модели строгое алгоритмическое ядро не встраивается, из-за самого принципа обучения.
Вы тут реально не замечаете противоречия?))
Ключевое слово - эволюция. Нынешние модели это переходные формы. Следующим шагом, вероятно, будут связки специализированных моделей.
Или будет дефицит быстродействующей памяти и как следствие - ничего не будет... Или будет тотальная коммерциализация всей этой сферы и под "неприкладную математику" никто не даст финансирования...
Не кажется ли вам преждевременным проектировать космодром для варп-звездолётов? Потому что прогресс может вырулить и так, что в Lean попросту отпадёт нужда (например его заменит более широкопрофильный "логический сопроцессор")... Или вскроются какие-то принципиальные ограничения для активно исследуемых областей математики (например необходимость оперировать не классической логикой)... А вы уже вбухали столько ресурсов в эту систему...
Да какая там наука? 29 тыс промежуточных теорем. Ни один математик никогда не разберется. Люди доказывают да, дольше, но адаптированно под людей с возможностью понимания и контроля
В 1993 году Эндрю Уайлс представил доказательство, очень под людей адаптированное. Люди несколько месяцев разбирались, нашли ошибку в одном из ключевых рассуждений. Уайлс еще 2 года сидел и исправлял, но только совместно с Тейлором довёл до конца. С Lean, при условии корректного прописывания и отсутствия ошибок в самом Lean, что отдельно можно тестировать, доказательство - компиляция программы.
Ещё вот нашёл пример интересный - гипотеза Кеплера. Для проверки назначили 12 рецензентов. Они работали четыре года, но так и не смогли полностью удостовериться в корректности доказательства. Их итоговая оценка: примерно 99% уверенности, что доказательство верно.
А есть доказательства, которые вообще никто не способен охватить целиком. Классификация конечных простых групп. Её первоначальное доказательство занимает порядка 10-15 тысяч страниц, распределённых примерно по 500 статьям более чем 100 математиков. В доказательстве обнаруживались пробелы, некоторые результаты были недостаточно подробно опубликованы, и десятилетиями шла работа по приведению всего материала в связную и проверяемую форму.
Так что, дойдя до определённого уровня сложности, математика неизбежно переходит к более строгой формализации и чем больше переведут на Lean, тем это будет проще и быстрее.
С Lean, при условии корректного прописывания и отсутствия ошибок в самом Lean, что отдельно можно тестировать, доказательство - компиляция программы.
Ну т.е. двойную работу сделать - вначале написать доказательство, а потом всю матчасть перевести в формальный язык Lean... И на каждом этапе запустить колоссальную по трудоёмкости операцию верификации...
Их итоговая оценка: примерно 99% уверенности, что доказательство верно.
А Lean как тут поможет? Спотыкаются ведь не на построении классической логики, а на какой-нибудь неоднозначности. Которую Lean в принципе устранить не может...
Её первоначальное доказательство занимает порядка 10-15 тысяч страниц, распределённых примерно по 500 статьям более чем 100 математиков.
Вот тут да - как агрегатор огромной по объёму матчасти, может сильно помочь. Но это же не специализация Lean. Он же для проверки, а не для разработки... Плюс снова - всё это вначале надо туда внести...
Так что, дойдя до определённого уровня сложности, математика неизбежно переходит к более строгой формализации.
Нет. Для этого вам мета-язык понадобится, а не машинный код.
UPD: Я понял как эта связка (Lean + нейросети) в идеале должна работать - нейросеть генерирует доказательство, а Lean проверяет. И вот тут это может быть чрезвычайно эффективно - можно закрыть огромный пул имеющихся нерешенных задач.
Ну т.е. двойную работу сделать - вначале написать доказательство, а потом всю матчасть перевести в формальный язык Lean... И на каждом этапе запустить колоссальную по трудоёмкости операцию верификации...
увы, да. но зато на выходе имеем почти полную уверенность в том, что доказательство верное.
А Lean как тут поможет? Спотыкаются ведь не на построении классической логики, а на какой-нибудь неоднозначности. Которую Lean в принципе устранить не может...
так формализация подсвечивает эти неоднозначности. смогли перенести доказательство в lean — неоднозначностей в нём не осталось (для простоты пока не учитываем возможные баги в самом lean)
UPD: Я понял как эта связка (Lean + нейросети) в идеале должна работать - нейросеть генерирует доказательство, а Lean проверяет
и так оно тоже часто используется.
но lean изначально использовался для формализации и проверки сгенерированных кожаными мешками доказательств. появление нейросетей позволяет скинуть на них нудную работу по переводу доказательства на язык lean. не понимаю, что тут может не нравиться
так формализация подсвечивает эти неоднозначности. смогли перенести доказательство в lean — неоднозначностей в нём не осталось (для простоты пока не учитываем возможные баги в самом lean)
Код на lean может доказывать не то, что написано в доказательстве, а какое-то совершенно другое утверждение. Как понимаю, именно это подразумевалось под "неоднозначностью".
Код на lean может доказывать не то, что написано в доказательстве, а какое-то совершенно другое утверждение. Как понимаю, именно это подразумевалось под "неоднозначностью".
Я реально в шоке от того, что вот этот тезис приходится разжёвывать уже несколько комментариев... Ещё и минусами злобно спамят... Как будто есть какая-то волшебная кнопка "строго формализуй приведённое доказательство без необходимости проверки корректности этой процедуры формализации"
Как будто есть какая-то волшебная кнопка "строго формализуй приведённое доказательство без необходимости проверки корректности этой процедуры формализации"
так новость про то, что нашлась такая волшебная кнопка, fable сам формализовал доказательство теоремы в lean;
а зачем нужна проверка корректности формализации? весь смысл записи доказательства в lean в том, что возможна автоматическа проверка корректности этого доказательства. от нас требуется лишь убедиться, что формулировка условия перенесена корректно.
Объясните - с чем именно вы спорите? Потому что уже сколько комментариев я (и не один) пытаюсь донести суть, а вы снова мимо...
так новость про то, что нашлась такая волшебная кнопка, fable сам формализовал доказательство теоремы в lean;
Кто проверил корректность этой формализации? Что именно в итоге этой формализации доказывается (само формализованное доказательство безусловно при этом может быть корректным)?
а зачем нужна проверка корректности формализации?
Чтобы удостовериться, что формализованное доказательство решает именно ту же задачу (включая весь пул подзадач определённых внутри), что и оригинальное.
от нас требуется лишь убедиться, что формулировка условия перенесена корректно.
Малость какая)) 1000 агентов 30 часов формализовывали, а тут стоит "лишь убедиться". И формулировка не условия, а доказательства - это малость разные вещи ;)
смогли перенести доказательство в lean — неоднозначностей в нём не осталось
А если не смогли, то возможно программисту-математику не хватило опыта, или терпения.
К тому же, формализация математической проблемы в системе Lean, это всегда немного эксперимент.
(для простоты пока не учитываем возможные баги в самом lean)
Не только баги, но и ограниченные возможности Lean. Система находится в процессе развития.
Ещё вот нашёл пример интересный - гипотеза Кеплера. Для проверки назначили 12 рецензентов. Они работали четыре года, но так и не смогли полностью удостовериться в корректности доказательства. Их итоговая оценка: примерно 99% уверенности, что доказательство верно
Большое число частных случаев
Мне всегда интересно, как такая мощь конвертируется в окупаемость.
Тысячи людей прочитали новость. В ней сказано, что Fable 5.2 очень умная нейросетка и может даже формализовать теорему Ферма. Круто. Сотня пользователей купит себе токенов или подписок на Fable 5.2, чтобы решать свои более простые задачи, т.е. понесут свои деньги Anthropic.
Инвесторы прочитают эту новость и поймут, что Fable 5.2 очень умная нейросетка и может даже формализовать теорему Ферма. Круто. Позже инвесторы также узнают, что сотня новых пользователей купили себе токенов и подписок на Fable 5.2, а значит Fable пользуется популярностью, поэтому инвесторам следует прикупить немного акций Anthropic, т.е. они понесут свои деньги Anthropic.
Компания Anthropic (разработчик ИИ-помощника Claude) официально подала документы (форму S-1) на первичное публичное размещение акций (IPO) в США. Само размещение и старт торгов предварительно ожидаются в ноябре 2026 года.
Чтобы цена акций была выше, нужно заранее подогреть к ним интерес. А значит будет много позитивных новостей о том, что Claude где-то занял первые места, кому-то очень сильно помог или смог решить важные для человечества задачи. Чем выше хайп, тем выше спрос на акции, тем выше их цена и тем больше иксов смогут сделать ранние инвесторы Anthropic. Так что те, чьи деньги ранее сжигал Anthropic, смогут выйти в хороший плюс и вернуть всё с большими бонусами. А новые покупатели акций Anthropic по факту будут спонсировать новое сжигание денег до того момента, пока Anthropic не выйдет на самоокупаемость и реальную прибыль.
нужно заранее подогреть к ним интерес. А значит будет много позитивных новостей о том, что Claude где-то занял первые места
Все верно. Сейчас решается задача не дать проекту утонуть. Новость об успешной “формализации теоремы Ферма” полезна для рекламы.
Но и при устойчивом финансовом положении Anthropic, подобные новости все равно были бы уместны, ради той же рекламы. И это оправдало бы “формализацию теоремы Ферма”.
И даже при отсутствии нужды в рекламе, “формализация теоремы Ферма” имела бы смысл для исследования возможностей моделей, в рамках развития моделей.
Так что для самих Anthropic “формализация теоремы Ферма” имела бы смысл в любом случае.
И сколько стоили эти 1000 агентов, работающих 30 часов?
примерно нисколько
я думаю, что это эти 30к агенто-часов — малая доля того, что anthropic потратила на внутренние тесты новой версии fable
Собственно все так и есть - это демонстрация возможностей и в этом и смысл этого проекта. Фактически это вложение в рекламу и демонстрация для инвесторов. Но в истории немало примеров как компании развивали науку просто исходя из корыстных целей продемонстрировать себя как технологического лидера. Например в свое время AT&T создала Bell labs и учёные работавшие на деньги корпорации получили 9 нобелевских премий и создали такие штуки как транзистор который фундаментально повлиял на всю электронику и открыли реликтовое излуние. Считал ли AT&T юнит экономику открытий которые возможно сделают ученные в их лабораториях? Или практическое применение и юнит экономику реликтового излучения? Вряд ли - они просто вкладывались в маркетинг и бренд компании.
До гордого номера 5.5 (как остальная линейка) не дотягивает, значит
Конский прайс за задачу
https://artificialanalysis.ai/models/releases/claude-fable-5-2
До 19 ноября входит в недельные лимиты в Claude подписке, идём пробовать!
На полях-то решение поместилось, или как?
Фокус в том, что теорема уже была формализована и какая-то информация об этом (хотя бы об общем путь) была в обушающей выборке.
Claude Fable 5.2 формализовала теорему Ферма за 30 часов
…
Тысяча агентов Claude Fable 5.2 за 30 часов
то есть всё-таки не 30, а 30 000 часов
1) Дикий прайс за задачу, если судить по агрегированным табличкам https://www.gptunnel.ru/ru/blog/claude-fable-5-2
2) В некоторых задачах на уровне опуса или карбона (который еще не вышел, ага)
3) Откатывает на более слабые модельки в случае "чувствительных запросов"
4) Отзывы чела который ее чуть ли не безлимитно тестил тоже не шибко впечатлили
Ощущение, что модель скорее пошла вширь (робототехника и тд) (ну ладно, еще наука), нежели впечатляет каким-то прогрессом в классических задачах
1) Дикий прайс за задачу, если судить по агрегированным табличкам https://www.gptunnel.ru/ru/blog/claude-fable-5-2
Ну скажете тоже - дикий. Вы же не видели их внутренние бухгалтерские документы? Ну вот, и (почти)никто не видел. Так что надо постепенно привыкать, график будет идти вправо и вверх.
Дикий в смысле что нет смысла столько платить за подавляющую часть задач. Дипсик сделает не хуже и на порядки дешевле. И череп измерять не будет в процессе.
ну вот поэтому дарио и ко и борятся с локальным инференсом)) то они хотят определенные правила регулирования отрасли ввести, то страшилки выпускают, как локальные ллм могут перезаражать всё вокруг, + при попытке улучшить локальную нейронку сброс до более простой модели идёт
короче идеальные условия - китай под запретом в гос учреждениях сша , локальные модельки под запретом + другие ограничения)
Вверх и вправо наверное зависит от того, насколько получится задавить всех этих "понаехов" по типу дипсика и квена
Зарегистрируйтесь на Хабре, чтобы оставить комментарий
Claude Fable 5.2 формализовала теорему Ферма за 30 часов