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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Рассмотрев представленные выше методы, можно сказать, что подход с использованием решателей действительно помогает 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 Подход на основе подсказок: перевод, рассуждение и проверка через LLM

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 _____________________________________________________________________________

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