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: |

If you initiate a Secret Chat, however, then these communications are end-to-end encrypted and are tied to the device you are using. That means it’s less convenient to access them across multiple platforms, but you are at far less risk of snooping. Back in the day, Secret Chats received some praise from the EFF, but the fact that its standard system isn’t as secure earned it some criticism. If you’re looking for something that is considered more reliable by privacy advocates, then Signal is the EFF’s preferred platform, although that too is not without some caveats. Messages are not fully encrypted by default. That means the company could, in theory, access the content of the messages, or be forced to hand over the data at the request of a government. These administrators had built substantial positions in these scrips prior to the circulation of recommendations and offloaded their positions subsequent to rise in price of these scrips, making significant profits at the expense of unsuspecting investors, Sebi noted. Oh no. There’s a certain degree of myth-making around what exactly went on, so take everything that follows lightly. Telegram was originally launched as a side project by the Durov brothers, with Nikolai handling the coding and Pavel as CEO, while both were at VK. Just days after Russia invaded Ukraine, Durov wrote that Telegram was "increasingly becoming a source of unverified information," and he worried about the app being used to "incite ethnic hatred."
from sg


Telegram Metaprogramming
FROM American