ИИ и формализмы

[sab123]

"Transformers Can Do Arithmetic with the Right Embeddings"
https://neurips.cc/virtual/2024/poster/94565

LLMов научили арифметике, как я понимаю, через специальное кодирование чисел. Это интересный трюк, поскольку у обычных ЛЛМов даже счет не получается, и да у людей научиться арифмерике занимает годы. Так что интересно с точки зрения понимания, как оно работает.

Но одновременно у меня возникает вопрос (который, как оказалось, авторам этой бумаги в голову не пришел): накойхер их учить арифмерике, если у них есть под боком компьютер, который может посчитать все то же самое легко и эффективно? Гораздо более продуктивным занятием было ты научить ЛЛМы пользоваться калькулятором. В простейшем варианте, добавить поспроцессинг к выводу ЛЛМа, который выцепит и выполнит вычислительные инструкции, и научить ЛЛМ генерить эти инструкции. Ну вот например, недавно народ активно рассуждал про "посчитать буквы r в слове strawberry". Это задание можно поделить на две части: (1) выцепить буквы r, (2) посчитать их. ИИ мог бы генерить что-то типа

$(wc r r r)

и получить на выходе 3. Ну и то же самое с любой арифметикой.

Интересно, какие возражения такая идея вызывает у учоных: "но ведь разрешать выполнение питонного кода из вывода - небезопасно". То, что можно сделать не Питон, а любой свой безопасный язык, им просто в голову не приходит. На лицо еще один признак большого разрыва между Машинными Учоными и Компьюторными Учоными.

А вот еще интересен такой момент: я спрашивал в разных местах, и у всех генерация машинного кода искусственным интеллектом просиходит совершенно от балды этого ИИ. Но ведь машинный код - формальный язык. Грамматика и семантика его известна. Ничего не мешает генерировать сразу согласно грамматике - проверять каждую следующую лексему на соответствие грамматике, и если соответстие не найдено, то ее отбрасывать и выбирать другую, следующую по весу. Может полученный код и не будет правильно работать, но как минимум всегда будет соответствовать грамматике, и с небольшими дополнительными проверками - компилироваться. В одном из мест я видел примеры кода, сгенерированного моделями различной сложности, с качеством, растущим со сложностью модели. Но простая формальная проверка должна поднять качество кода, сгенерированного даже простыми моделями.

Comments

[sobriquet9]

Смысл не в том, чтоб научить LLM совершать арифметические операции. Это умеет делать даже механический арифмометр.

Смысл в том, чтобы LLM научилась этому самостоятельно. В этом преимущество нового поколения reasoning моделей вроде DeepSeek r1. У них умение мыслить логически появилось само по себе, в результате тренировки, а не было заранее запрограммировано человеками.

При разговоре с r1 видно, как оно думает, можно отследить логическую цепочку мыслей. Даже когда оно ошибается, эти ошибки не такие, как раньше, где просто слова брались явно от балды. Может сказать "я не знаю", может зациклиться в рассуждениях и не найти ответа, как человек.

[lev]

пусть считают по аксиомам Пеано

[chapai]

еще надо смотреть, есть ли у LLM теже проблемы с разрядностью вещественными и накоплением ошибки. Во всяких матбиблиотеках довольно мучительно решали. Возможно вот таким фокусом обошли.

[paserbyp]

"Гораздо более продуктивным занятием было ты научить ЛЛМы пользоваться калькулятором."

Калькулятор это приложение и его надо сначала запрограммировать, а пользоваться калькулятором, который поставляется с ОС не совсем корректно, только если это система не написана сама ИИ.

накойхер их учить арифмерике

[rotbar]

Вопрос, например, правильный.

[selik]

Проблема как раз в том, что ЛЛМ пытается мыслить логически, а математика нелогична.

Сделать отдельно калькулятор – просто. Но совместить с логическим мышлением не получается.

Почему так. Арифметика существует несколько тысячелетий, но у неё никогда не было логически непротиворечивых правил. Это упущение попытались устранить лет 150 назад и напоролись на теоремы Гёделя о противоречивости и неполноте.

Пример 1. Делить можно на любое число за исключением нуля. Это нарушение закона исключённого третьего. В логике не существует утверждений вида «все без исключения… за исключением…», «любой… кроме…». А ещё есть проблемы с единицей.

Пример 2. Матан опирается на утверждение, что на дифференциально малом участке дуга тождественна прямой. Это прямое нарушение закона тождества.

В общем совместить логику и математику даже у людей не получается. В подавляющем большинстве случаев люди этого не замечают, потому что логикой не владеют. А вот в ЛЛМ проблема проявилась во всей красе.

Как встроить калькулятор в LLM

[dennisgorelik]

> В простейшем варианте, добавить поспроцессинг к выводу ЛЛМа

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