Telegram Group & Telegram Channel
Вкратце о математиках, информатиках и маркетинге

ChatGPT выпустил новую модель, o1, построенную на принципе рекурсивного порождения текстов: модель буквально ведёт сама с собой "внутренний диалог", "думает вслух", пытаясь в итоге получить рациональное построение.

Как и во все предыдущие разы, достигнутый успех, мягко говоря, ограниченный. Забавная и в чём-то правдоподобная модель мышления способна выдать рассуждение на общие вопросы, но сыпется на самых простых задачках из, к примеру, абстрактной алгебры.

Подобное положение вещей укрепляет уже в общем-то устоявшееся впечатление, что большие лингвистические модели это больше о болтовне на свободные темы, чем о решении реальных задач.

С чем смириться, конечно, невозможно.

Для подтягивания роботам математики необходимо (хоть и недостаточно) набрать "математического материала". Буквально следует иметь некое промежуточное формальное представление, не допускающее лишних вольностей и галлюцинаций, в которое можно конвертировать запрос пользователя (математическую задачу, формулировку теоремы и т.п.), и из которого потом снова перевести результат на естественный язык. (Такую работу ИИ как специфического "универсального переводчика" вкратце обсуждали ранее.)

Как на основе подобного формального представления довести качество работы бота до приемлемого уровня (ведь в аналогичной задаче — написание программного кода — ещё и близко об этом говорить не приходится) как-нибудь в будущем разберутся.

Сейчас — нужен сырой материал для обучения.

В таком контексте второе дыхание получают proof assistants — "помощники в доказательстве", такие как Lean.

И на сцену выходят агрессивные проповедники (см. предыдущий пост-введение) с практически буквально следующими лозунгами: деды приватизировали математику, да и вообще люди совершают ошибки, формализуем все теории в Lean!

Целевая аудитория: пассионарные undergraduate students (бакалавры). Ну оно и понятно по слову "деды" в риторике (сам Кевин практически подросток, до 60 ещё два года).

Работа по рутинной формализации всяких давно известных вещей скучная, тупая, безблагодатная и в целом в контексте обучения отдельно взятого математика неоднозначная. А ведь нельзя же просто взять денег у Microsoft на честное развитие проекта, нацеленного на совершенствование ИИ... а кстати, почему нельзя?

Агрессивная риторика, впрочем, неизбежно порождает агрессивных фанбоев. Ну знаете, есть пользователи Apple и есть пользователи Apple. В таком же смысле есть пользователи Lean и есть пользователи Lean :)

По неофициальному мнению некоторых профессионалов в области систем формальных доказательств из числа наших подписчиков, началась вся текущая волна беззастенчивой рекламы с того, что... американцам в более зрелых проектах-аналогах не понравилось название... потому что Coq оно по произношению означает... ну, вы знаете, то самое. Не захотели переименовываться по-хорошему, сейчас значит организуем переезд по-плохому! :)

#mathematics #programming



group-telegram.com/metaprogramming/366
Create:
Last Update:

Вкратце о математиках, информатиках и маркетинге

ChatGPT выпустил новую модель, o1, построенную на принципе рекурсивного порождения текстов: модель буквально ведёт сама с собой "внутренний диалог", "думает вслух", пытаясь в итоге получить рациональное построение.

Как и во все предыдущие разы, достигнутый успех, мягко говоря, ограниченный. Забавная и в чём-то правдоподобная модель мышления способна выдать рассуждение на общие вопросы, но сыпется на самых простых задачках из, к примеру, абстрактной алгебры.

Подобное положение вещей укрепляет уже в общем-то устоявшееся впечатление, что большие лингвистические модели это больше о болтовне на свободные темы, чем о решении реальных задач.

С чем смириться, конечно, невозможно.

Для подтягивания роботам математики необходимо (хоть и недостаточно) набрать "математического материала". Буквально следует иметь некое промежуточное формальное представление, не допускающее лишних вольностей и галлюцинаций, в которое можно конвертировать запрос пользователя (математическую задачу, формулировку теоремы и т.п.), и из которого потом снова перевести результат на естественный язык. (Такую работу ИИ как специфического "универсального переводчика" вкратце обсуждали ранее.)

Как на основе подобного формального представления довести качество работы бота до приемлемого уровня (ведь в аналогичной задаче — написание программного кода — ещё и близко об этом говорить не приходится) как-нибудь в будущем разберутся.

Сейчас — нужен сырой материал для обучения.

В таком контексте второе дыхание получают proof assistants — "помощники в доказательстве", такие как Lean.

И на сцену выходят агрессивные проповедники (см. предыдущий пост-введение) с практически буквально следующими лозунгами: деды приватизировали математику, да и вообще люди совершают ошибки, формализуем все теории в Lean!

Целевая аудитория: пассионарные undergraduate students (бакалавры). Ну оно и понятно по слову "деды" в риторике (сам Кевин практически подросток, до 60 ещё два года).

Работа по рутинной формализации всяких давно известных вещей скучная, тупая, безблагодатная и в целом в контексте обучения отдельно взятого математика неоднозначная. А ведь нельзя же просто взять денег у Microsoft на честное развитие проекта, нацеленного на совершенствование ИИ... а кстати, почему нельзя?

Агрессивная риторика, впрочем, неизбежно порождает агрессивных фанбоев. Ну знаете, есть пользователи Apple и есть пользователи Apple. В таком же смысле есть пользователи Lean и есть пользователи Lean :)

По неофициальному мнению некоторых профессионалов в области систем формальных доказательств из числа наших подписчиков, началась вся текущая волна беззастенчивой рекламы с того, что... американцам в более зрелых проектах-аналогах не понравилось название... потому что Coq оно по произношению означает... ну, вы знаете, то самое. Не захотели переименовываться по-хорошему, сейчас значит организуем переезд по-плохому! :)

#mathematics #programming

BY Metaprogramming


Warning: Undefined variable $i in /var/www/group-telegram/post.php on line 260

Share with your friend now:
group-telegram.com/metaprogramming/366

View MORE
Open in Telegram


Telegram | DID YOU KNOW?

Date: |

The original Telegram channel has expanded into a web of accounts for different locations, including specific pages made for individual Russian cities. There's also an English-language website, which states it is owned by the people who run the Telegram channels. At the start of 2018, the company attempted to launch an Initial Coin Offering (ICO) which would enable it to enable payments (and earn the cash that comes from doing so). The initial signals were promising, especially given Telegram’s user base is already fairly crypto-savvy. It raised an initial tranche of cash – worth more than a billion dollars – to help develop the coin before opening sales to the public. Unfortunately, third-party sales of coins bought in those initial fundraising rounds raised the ire of the SEC, which brought the hammer down on the whole operation. In 2020, officials ordered Telegram to pay a fine of $18.5 million and hand back much of the cash that it had raised. "The inflation fire was already hot and now with war-driven inflation added to the mix, it will grow even hotter, setting off a scramble by the world’s central banks to pull back their stimulus earlier than expected," Chris Rupkey, chief economist at FWDBONDS, wrote in an email. "A spike in inflation rates has preceded economic recessions historically and this time prices have soared to levels that once again pose a threat to growth." "We as Ukrainians believe that the truth is on our side, whether it's truth that you're proclaiming about the war and everything else, why would you want to hide it?," he said. Friday’s performance was part of a larger shift. For the week, the Dow, S&P 500 and Nasdaq fell 2%, 2.9%, and 3.5%, respectively.
from us


Telegram Metaprogramming
FROM American