sab123: (Default)
SB ([personal profile] sab123) wrote2025-02-16 04:05 pm

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

"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. Ну и то же самое с любой арифметикой.

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

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

[personal profile] selik 2025-02-18 04:48 am (UTC)(link)
Не знаю такого доказательства у Гёделя. Он доказал, что любая сложная формальная система либо противоречива, либо неполна. А вот логика Аристотеля построена на аксиомах. Они по определению истинны, ни от чего не зависят, не доказываются и не ставятся под сомнение.

Я и не говорил, что математика не работает. На матане вся физика держится. Я говорю, что математика нелогична, как и физика. Сила науки проявляется в ее способности предсказывать будущее, а не в том, насколько она логична. Но здесь речь об ЛЛМ. Как ему совместить логику и математику?

sobriquet9: (Default)

[personal profile] sobriquet9 2025-02-18 12:42 pm (UTC)(link)

Неполнота в данном контексте именно это и означает.