Как-то раз мы со студентами-переводчиками по ИТ задались вопросом:

А реально ли LLM «думает»? Или она просто, подобно школьнику, подгоняет объяснения под ответ в конце учебника, не имея ни малейшего понятия о том, правилен ли этот ответ или логичны ли ее рассуждения?

Поиски ответов на этот вопрос привели нас к статье-исследованию "Empowering LLMs with Logical Reasoning: A Comprehensive Survey", адаптированный перевод которой мы и предоставляем вашему вниманию. Над переводом мы работали вместе с коллегой – Губановой Екатериной.

Статья представляет собой большой обзор подходов к тому, как сделать языковые модели не просто «говорящими машинами», а системами, которые умеют думать, делать выводы и находить логические связи, «не натягивая сову на глобус».

Введение

Этот обзор посвящен способности больших языковых моделей (LLM) рассуждать логически – а точнее тому, как систематизировать современное состояние исследований: с какими логическими задачами модели справляются плохо и какие методы помогают улучшить их способности.

Сразу отметим: в этом обзоре не рассматриваются все возможные подходы к развитию LLM – мы сосредоточимся на двух ключевых направлениях, выделенных авторами: логическое решение вопросов и логическая согласованность.

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

1. Трудности LLM с рассуждениями

LLM отлично показали себя в NLP задачах (генерация текста, классификация, перевод и т.д.), но у них по-прежнему есть проблемы с логическим рассуждением.

С одной стороны, LLM учатся понимать синтаксис, смысл слов и общие знания о мире через задачи вроде предсказания следующего слова в тексте или заполнения пропусков. Но этого недостаточно, чтобы они умели логически рассуждать – модель может правильно строить предложения и подбирать слова, но не умеет делать выводы на основе фактов. С другой стороны, тексты, на которых обучаются LLM, в основном написаны людьми и редко содержат примеры настоящих логических рассуждений, таких как последовательные выводы или доказательства. То есть модели почти не видят реальных примеров того, как нужно шаг за шагом проверять и связывать факты, чтобы прийти к правильному логическому заключению.

Эти проблемы серьёзно ограничивают применение больших языковых моделей по двум направлениям.

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

1) Проверка истинности утверждения.

Модели нужно определить, верно ли данное утверждение на основе предоставленной информации – ответ может быть «истинно», «ложно» или «неизвестно». Например, даны вводные: “Metals conduct electricity. Insulators do not conduct electricity. If something is made of iron, then it is metal. Nails are made of iron.” (Металлы проводят электричество. Изоляторы не проводят электричество. Если что-то сделано из железа, значит это металл. Гвозди сделаны из железа).

Логический вопрос, заданный LLM: “Nails cannot conduct electricity. Is the following statement true, false, or unknown?” (Гвозди не проводят электричество. Истинно, ложно или неизвестно?).

Чтобы дать правильный ответ, модель должна проследить цепочку рассуждений: nails → made or iron → metal → conduct electricity (гвозди → сделаны из железа → металл → проводят электричество).

Таким образом, утверждение “Nails cannot conduct electricity” (Гвозди не проводят электричество) оказывается ложным.

2) Выбор правильного варианта из нескольких предложенных.

В этом случае модели нужно выбрать такой вариант ответа, который удовлетворяет всем данным условиям и вводным. Например, при нескольких возможных ответах модель должна проверить каждый и убедиться, что он не противоречит фактам и правилам, прежде чем выбрать правильный.

На удивление, модель LLaMA 13B (одна из больших языковых моделей компании Meta, специально обученная понимать и генерировать текст) правильно отвечает только на 33,63% вопросов из набора FOLIO – специального датасета с логическими задачами, где требуется проверять факты и делать выводы. Для этого модели сначала показывают 8 примеров правильных ответов, чтобы она поняла, как решать задачу, а затем задают новый вопрос. Для сравнения, если бы модель просто угадывала ответы между вариантами «истинно», «ложно» и «неизвестно», точность была бы почти такой же – 33,33%.

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

Во-вторых, LLM также склонны давать противоречивые ответы на разные вопросы, что рассматривается как нарушение логической согласованности. Формы логической согласованности могут быть разными. Например, LLaMa-2 70B отвечает положительно и на вопрос “Is an albatross an organism?” (Является ли альбатрос организмом?), и на вопрос “Is an albatross not an organism?” (Альбатрос не является организмом?), что нарушает согласованность отрицания (см. пункт 3 для формального определения). Вспомним также пример с сорокой в современной модели вопросов и ответов Macaw, где сорока – птица, птицы имеют крылья, но сорока, в итоге, оказалась бескрылой.

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

В этой статье мы рассматриваем обе проблемы вместе. Они напрямую связаны между собой и одинаково важны для развития логических способностей моделей. Для их решения уже предложено немало подходов: одни направлены на повышение точности ответов на логические вопросы, другие – на обеспечение согласованности. В последние годы эти направления вызывают особый интерес, и в своей работе мы подробно проанализировали самые современные методы и представили их классификацию (см. рис. 1).

В частности, для логического решения вопросов найденные нами методы делятся на три категории:

1. основанные на решателях (Solver-based) – переводят задачи из естественного языка в символическую форму и решают их с помощью внешних логических решателей;

2. основанные на подсказках (Prompt-based) – либо явно выстраивают цепочку логических рассуждений при ответе, либо переводят текст в символическую форму с помощью тщательно подобранных подсказок, после чего используют LLM для более глубокого рассуждения;

3. основанные на методах предобучения и дообучения (Pretrain and fine-tuning methods) – учитывая нехватку в корпусах высококачественных примеров рассуждений (например, многошаговых выводов или доказательств), данные подходы предлагают дообучать LLM на расширенных выборках, где явно представлены рассуждения и пошаговые доказательства.

Для логической согласованности мы формализовали наиболее распространённые её типы, а также их комбинации:

1. согласованность по импликации (Implication Consistency),

2. согласованность по отрицанию (Negation Consistency),

3. согласованность по транзитивности (Transitivity Consistency),

4. согласованность по фактичности (Factuality Consistency).

2. Логическое решение вопросов

Для проверки того, как LLM решают логические задачи, мы создали разные тестовые наборы (benchmarks). Эти наборы показывают, умеет ли модель делать правильные выводы, не запутывается ли в противоречиях и насколько точно решает логические задачки.

2.1 Подход с использованием решателей: перевод через LLM и решение через внешние инструменты

Идея подхода с решателями, довольно проста: сначала задача на естественном языке превращается в формулы на символическом языке, а потом решается внешним логическим решателем. В целом процесс делится на три шага (см. рис. 2).

1. LLM переводит текстовую задачу в символическую форму (это может быть язык логического программирования (LP), логика первого порядка (FOL), задачи удовлетворения ограничений (CSP) или проверки, можно ли сделать выражение истинным (SAT) – такая запись понятна внешнему решателю);

2. решатель делает свою работу и выдаёт ответ;

3. LLM переводит этот ответ обратно в привычный язык, чтобы получился финальный результат.

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

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

Так, например, существует метод Faithful Chain-of-Thought (Faithful CoT). Его цель – сделать рассуждения модели прозрачными, показывая реальные промежуточные шаги, которые она использует для ответа. Faithful CoT переводит задачу в цепочку символических рассуждений, а затем эти рассуждения можно проверить через внешние решатели (например, Python, Datalog или PDDL) (см. рис. 4).

С помощью этого метода можно получить более надёжные ответы, потому что модель не просто выдаёт результат, а демонстрирует ход мыслей. Однако у него есть ограничения: сложные нелинейные задачи могут быть слишком тяжёлыми для формальных инструментов, а даже небольшие ошибки при формализации цепочки рассуждений могут привести к неправильному результату.

В отличие от Faithful CoT, методы SatLM (см. рис. 5) и LINC (см. рис. 6) используют более универсальный подход: они сначала переводят текст задачи в общие логические формулы, а затем решают их с помощью специальных алгоритмов.

LogicLM идёт ещё дальше: сразу преобразует задачу в несколько формальных систем (например, линейное программирование, логика первого порядка, задачи с ограничениями и логические проверки), чтобы максимально точно уловить смысл текста (см. рис. 7). Однако при этом часто теряются тонкие логические нюансы, скрытые в естественных предложениях – как результат, модель не справляется (см. рис. 8).

Метод CLOVER пытается это исправить: сначала строится структура логических зависимостей внутри предложения, а потом переводятся его части поэтапно, чтобы сохранить смысл (см. рис. 8).

Рассмотрев представленные выше методы, можно сказать, что подход с использованием решателей действительно помогает LLM справляться с логическими задачами, но имеет свои недостатки:

Преобразование текста в формальные формулы часто теряет важную информацию. Например, утверждение: “When a person reads a book, that person gains knowledge. Harry read Walden. Whether this inference is correct: Harry gains knowledge.” (Когда человек читает книгу, он получает знания. Гарри прочитал «Уолден». Верно ли, что Гарри получил знания?) может привести к неопределённому ответу, потому что символический перевод не учитывает, что Гарри – человек и что «Уолден» – книга. Для человека это очевидно, а модель этого не видит.

Даже маленькая ошибка при переводе может полностью испортить результат. У некоторых моделей, например GPT-3.5, бывают проблемы с правильной расстановкой скобок и другими деталями формул.

И, наконец, чем сложнее задача, тем больше растёт пространство поиска решений. Иногда существующие решатели могут работать неделями или даже месяцами, прежде чем найти ответ.

2.2 Подход на основе подсказок: перевод, рассуждение и проверка через LLM

Другой большой класс методов основан не на внешних решателях, а на правильном использовании промптов. Идея здесь такая: если мы правильно сформулируем задание для модели, то она сможет сама рассуждать более логично и давать более точные ответы.

В этом подходе методы обычно делят на два больших направления.

1) Модель прямо в процессе ответа «расписывает» свои рассуждения.

То есть вместо того, чтобы сразу сказать «да» или «нет», она сначала объясняет, как пришла к этому выводу. Такой приём называется Chain-of-Thoughts (CoT). Примерно, как если бы студент решал задачу по математике и показывал все промежуточные шаги (см. рис. 9). На основе CoT появились более сложные варианты.

Например, Tree-of-Thoughts (ToT) позволяет модели рассмотреть несколько возможных цепочек рассуждений и выбрать ту, которая выглядит наиболее убедительной.

В свою очередь, Graph-of-Thoughts (GoT) превращает рассуждения в целый граф, где разные куски знаний соединяются узлами и рёбрами. Это похоже на то, как человек держит в голове целую «карту мыслей», а не просто одну прямую линию (см. рис. 9).

Есть и более формализованные попытки – например, Diagram-of-Thoughts (DoT). Здесь рассуждения строятся в виде направленного ациклического графа (DAG) (см. рис.  10), где узлы – это высказывания, уточнения, проверки и даже критические замечания, а стрелки между ними показывают логику связей. То есть DoT не просто показывает связи между идеями, как GoT, а превращает рассуждения в формальную структуру, которую можно системно анализировать и проверять (см. рис. 11).

Иногда исследователи выделяют ещё один метод – разбить сложный вопрос на несколько простых и решать их по шагам. Так, Cumulative Reasoning (CR), дословно «совокупное рассуждение» предлагает подключать к процессу сразу три разных модели: одна – предлагает гипотезы, другая – проверяет, а третья – подводит итог. Такой коллективный способ работает надёжнее, чем если бы модель рассуждала в одиночку (см. рис. 12).

2) Сначала задачу переводим с естественного языка в более строгий символический язык (например, в логические формулы), а потом уже просим модель рассуждать в этих терминах. Здесь всё держится на том, что грамотно подобранный промпт помогает LLM «понять», как перейти от текста к символам.

Например, метод Symbolic Chain-of-Thoughts (SymbCoT) работает так: модель переводит задачу в логические выражения, затем шаг за шагом применяет правила вывода (вроде классического: «если А → В и А, то В»), и только потом проверяет всю цепочку (см. рис. 13).

Другой подход – Logic-of-Thoughts (LoT), где для начала задействуются алгоритмы на Python, которые делают строгие логические выводы, а затем результаты снова подаются модели в виде текста. В итоге получается комбинированный процесс: вычислительная строгость + языковая гибкость (см. рис. 14).

Ещё один интересный вариант – LLM-Driven Neuro-Symbolic Approach (LINA), где используется гипотетико-дедуктивный метод (сначала строится гипотеза, потом проверяются её следствия). Чтобы повысить надёжность, итоговый ответ выбирается «голосованием большинства» (см. рис. 14).

У методов этого подхода есть явные плюсы. Главное – это прозрачность: можно посмотреть на рассуждения модели и понять, как она пришла к выводу. Также интерпретируемость: шаги можно проверить и при желании указать на ошибки. Но есть и минусы.

Во-первых, LLM всё равно склонны к «галлюцинациям» – они могут вставить в рассуждения лишние факты или перепутать причинно-следственные связи.

Во-вторых, такие методы требуют колоссальных вычислительных ресурсов. Чтобы решить даже одну задачу, модель должна пройти десятки или сотни шагов рассуждений, а каждый шаг – это отдельный вызов модели. В итоге затраты быстро становятся огромными.

2.3 Подход предварительного обучения и дообучения

Ограниченные способности LLM к рассуждениям во многом объясняются тем, что в корпусах, на которых они обучаются, очень мало качественных примеров строгих логических выводов. Большинство текстов, написанных людьми, содержат скорее «размышления вслух», чем пошаговые доказательства или строгую дедукцию. Поэтому неудивительно, что модель умеет строить грамотные предложения, но не всегда способна рассуждать как логик.

Интуитивно решение кажется простым: если мы хотим, чтобы модель умела доказывать, её надо учить на примерах доказательств. То есть добавлять в обучение тексты, где явно расписаны логические шаги: от исходных фактов → к промежуточным выводам → к окончательному результату. Такой материал может заметно улучшить внутренние способности модели к логическому мышлению.

Для этого используют предобучение и дообучение на логических задачах. Разница между ними в том, откуда берётся обратная связь.

Внутренняя обратная связь опирается на саму модель: она анализирует свои же ответы и уточняет их, используя внутренние параметры.

Внешняя обратная связь приходит от людей, других моделей или внешних инструментов (например, логических решателей).

Есть разные примеры таких методов. Например, метод интерактивного согласования логики на основе дедукции, известный как Deductive Iterative Logic Alignment (DiLA) работает так: модель сначала предлагает своё решение, а затем оно многократно уточняется с учётом ограничений логики первого порядка. Проверку корректности выполняет SAT-решатель, и модель обновляет ответ до тех пор, пока не будут выполнены все логические условия (см. рис. 15).

Другой метод – Logic-Driven Contrastive Learning. Его идея в том, чтобы натренировать модель лучше «схватывать» логическую информацию, заставляя её отличать правильные рассуждения от неправильных.

Например, даём LLM задачу: «Все птицы умеют летать. Пингвин – птица. Умеет ли пингвин летать?»

Варианты рассуждений модели: «Да, пингвин – птица, значит летает» (неправильно). «Нет, пингвин – птица, но пингвины не умеют летать» (правильно).

Модель таким образом учится отличать и постепенно начинает отдавать предпочтение правильной логике. То есть она не просто получает ответ, а учится понимать, почему рассуждение верное, а другое – нет.

Метод Abstract Meaning Representation – Logic-Driven Augmentation (AMR-LDA) работает в три этапа. Сначала обычный текст превращается в структурированную схему смысловых связей (граф AMR) (см. рис. 16). Затем над этим графом выполняются логические преобразования, чтобы создать новые варианты рассуждений. Наконец, граф снова переводят в текст. Так получается дополнительный тренировочный материал, где явно показаны разные варианты логической обработки информации.

Для большей прозрачности и объяснимости предложен метод Logical Inference Process Training (LOGIPT). Это метод логически ориентированного пошагового обучения, который не просто дообучает модель, а фактически встраивает в неё процесс рассуждения с помощью внешнего решателя Pyke, позволяя модели самой воспроизводить и объяснять шаги рассуждений (см. рис. 17).

Метод Algorithmic Logic Training (ALT), строит специальный синтетический корпус на основе логических принципов. В нём каждое задание сначала формируется логическим алгоритмом (см. рис. 18) (как цепочка строгих выводов), а потом переводится в естественный язык. Такой материал используется для обучения модели тому, как шаг за шагом сделать вывод из фактов.

Очень похожую идею использует LogicAsker. Здесь исследователи выделили базовый набор логических навыков (например, умение работать с высказываниями или предикатами), а потом с помощью LLM сгенерировали для каждого навыка собственные примеры на естественном языке. Далее эти задания использовались для проверки слабых мест модели и создания новых обучающих данных, чтобы подтянуть проблемные зоны (см. рис. 19).

Наконец, LogicLLM пошёл по пути полной автоматизации: он предлагает полностью самосупервизируемую схему, где сама модель создаёт и проверяет логические примеры без ручной разметки. Это снижает затраты и позволяет генерировать очень большие тренировочные наборы.

В целом методы предобучения и дообучения показывают, что, если мы систематически «кормим» модели примерами рассуждений, они начинают заметно лучше справляться с логическими задачами. Однако такие подходы требуют больших объёмов специально подготовленных данных и продуманной организации обучения.

2.4 Проверка логического рассуждения LLM

В целом, задача на логическое рассуждение содержит описание на естественном языке, в котором формулируется набор высказываний или ограничений, связанных с определёнными объектами, а также вопрос о этих объектах. Цель состоит в том, чтобы, исходя из предоставленной информации, вывести правильный ответ.

Такие пары «вопрос-ответ» обычно делят на два основных типа:

1.    Вопросы со свободной формой ответа

Здесь задача модели – определить, можно ли логически вывести ответ на данный вопрос или утверждение из предоставленной информации. Ответ обычно выражается как «истинно», «ложно» или «неизвестно».

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

Существует несколько типичных наборов данных для обучения и тестирования моделей на такого рода задачах:

• Proofwriter – для проверки цепочек рассуждений и доказательств;

• FOLIO – с логическими задачами, где требуется проверять факты и делать выводы;

• Ruletaker – задачи с логическими правилами и выводами.

2.    Вопросы с выбором из нескольких вариантов

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

Такие задачи формулируются с использованием Constraint Satisfaction Problem (CSP), дословно «задачи удовлетворения ограничений» или булевой SAT-формулировки. Простыми словами, это задачи, где нужно найти значения для переменных так, чтобы все условия (ограничения) выполнялись одновременно (в случае CSP), и задачи, где нужно проверить, можно ли сделать логическое выражение истинным, подбирая значения «истинно» или «ложно» для переменных.

Среди типичных наборов данных:

• ReClor – набор логических задач, где нужно выбрать правильный вариант ответа;

• LogiQA – вопросы на проверку логического понимания текста и аргументации;

• AR-LSAT – задачи, направленные на тренировку логического вывода и анализа аргументов.

 _____________________________________________________________________________

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

Продолжение следует.