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 Security Service of Ukraine said in a tweet that it was able to effectively target Russian convoys near Kyiv because of messages sent to an official Telegram bot account called "STOP Russian War." The regulator said it had received information that messages containing stock tips and other investment advice with respect to selected listed companies are being widely circulated through websites and social media platforms such as Telegram, Facebook, WhatsApp and Instagram. Despite Telegram's origins, its approach to users' security has privacy advocates worried. "And that set off kind of a battle royale for control of the platform that Durov eventually lost," said Nathalie Maréchal of the Washington advocacy group Ranking Digital Rights. "He has to start being more proactive and to find a real solution to this situation, not stay in standby without interfering. It's a very irresponsible position from the owner of Telegram," she said.
from us


Telegram Metaprogramming
FROM American