Шахматы или Го — это EXPTIME, а всеми любимый сокобан — лишь PSPACE

Шахматы или Го — это EXPTIME, а всеми любимый сокобан — лишь PSPACE. Однако, удивительно, но AI, расправляющийся даже с Го, не может осилить довольно простые для человека головоломки сокобана:

https://ia800300.us.archive.org/26/items/lets-logic-bots-statistics/lets-logic-bots-statistics-2024-apr-19.pdf

Подозрение, что проблема тут примерно такая же, что и с программированием (точнее, с software design): недостаточно просто двигать игрока (CRUD, перекладывать json...), надо ещё и перемещать контейнеры (последующая логика обработки json), что добавляет новые уровни сложности.

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

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

Кроме того, в сокобане нет такого огромного количества предварительно проанализированных партий, на которых можно было бы эффективно обучать AI. В программировании такие данные есть, однако к их качеству ооочень большие вопросы :)

Одно время возлагали надежды на то, что LLM якобы проявляет эффект эмерджентности: обучаясь на данных, особенно, сгенерённых AI, нейронка проявляет нежданные способности, значительно "выше" уровня входных данных. Однако =>

https://habr.com/ru/news/832184/

"использование контента, созданного ИИ, для обучения новых нейросетей грозит коллапсом модели. Сгенерированные данные приводят к необратимым дефектам в новых моделях, и они начинают выдавать бессмыслицу."

=

И по прежнему никакого "понимания" смысла проекта AI не может продемонстрировать. Автономные задачки с хорошо сформулированным заданием они решают неплохо, ну да, могут с литкода задачи щёлкать, ну и что. Больше времени потратишь на объяснение, что надо сделать, и на последующие проверки.

Кстати, хайп по поводу "экспоненциального" развития LLM-ок продолжается, ну будут они быстро генерировать "прикольные" фильмы на любой вкус, а кто это будет смотреть? Интернет забьётся мусором, и всё. А вот хотя бы на рабочем джуниорском уровне в AI-программировании в этом году прогресса вообще не было фактически.

=

Это всё конечно гуру ai/ml понимают, поэтому пытаются скрестить ежа с ужом (и увы, результативно). Для программистов уже реальная опасность:

"AI achieves silver-medal standard solving International Mathematical Olympiad problems"

https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/

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

Gemini переводит задание на функциональный язык Lean с зависимыми типами (который также активно используют как теорем-прувер), и передают его AlphaZero, который уже умеет решать такие формальные задачи. Не знаю, подозрение, что в реальности Lean вряд ли потянет даже небольшой джуниорский проект на тысячу строк (слишком много измерений). Возможно, придумают что-нибудь вроде делегирования из Lean подзадач SMT-солверам (как миддл джунам)...

=

Резюме такое, что использовать AI-ассистанты полезно конечно, но разумно. Я с ними пока работаю в основном как с умным поисковиком, который может пояснить конкретную фичу на примерах, и не более. Генерация достаточно сложного кода в рамках проекта слишком трудоёмка получается суммарно, включая тестирование, интеграцию, баги.

А насчёт сокобана, получается это очень даже неплохой тренажёр для программистов, поэтому рекомендую решать побольше сокобановских задачек =>

https://letslogic.com/

Источник: letslogic.com

Комментарии: