Добрый день, это моя первая статья на Хабре, прошу не судить строго.

Я хочу рассказать вам немного о моём исследовании и то как стоит честно относиться к LLM моделям, так как вы скорее всего знаете, что такое LLM модель не будем терять времени на её определение давайте перейдём к сути моей работы: LLM не дают гарантии правильности ответа особенно операций с большим количеством шагов и формальным рассуждением, даже когда ответ правдоподобный или оказывается верный. (Вы же все видели дисклеймер ChatGPT can make mistakes.Check important info)

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

Но так как мы живём в мире где мы внедряем системы LLM повсюду появляется закономерный вопрос как же верифицировать LLM и тут у инженеров есть готовый по их мнению инструментарий, который массово внедряется:

• RAG (Создание баз знаний)

• fine-tuning (до-обучение моделей)

• Человеческий контроль (Human control)

• Более мощные LLM с большим количеством параметров (на 120b, на 200b и так далее)

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

Моя идея состоит, что у нас есть математическая теория доказательств, а также можно сделать сертификацию входящего сообщения, то есть давайте создадим

• Сообщение, которое должно быть в установленном формате

• Создадим минимальное ядро для верификации данных в моём случае послужило ядро верификации на основе Hilbert system из теории доказательств.

Пример моего сообщения из certificate.schema :

В чём же сам модуля верификации:

• JSON декодируется с DisallowUnknownFields(), то есть лишние поля мы сразу запрещаем (только в том виде, котором мы собираемся общаться)

• Затем проводим верификацию сообщения (проверяем структуру сообщения)

  • есть у него поля заявленные в сертификате (proof_id, goal, context, steps)

  • версия сертификата соответствует(certificate_version == «1.0.0»)

  • и другие параметры, которые вы можете посмотреть в функции

• После верификации если она пройдена:

  • соединяем с нашей базой правил

  • проверяем синтаксис

  • парсим goal, assumptions и каждую формулу шага

  • проходим шаги по порядку и валидируем их как assupmtion(предпосылка), axio(аксиома) или modus_ponens(правило вывода)

  • в конце проверяем, что последняя выведенная формула равна параметру goal во входящем сообщении

Какие ограничения я наложил на систему:

Мы пользуемся очень маленьким языком:

• переменные

• отрицания !

• импликация → (если..., то...)

• скобки

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

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

Мы написали этот инструмент верификации, но что же дальше.

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

Вот полная архитектура моей модели верификации LLM:

задача → prompt → LLM → candidate certificate → Hilbert verifier → accept/reject

Генерацией кандидатов у меня занимались модели (через ollama (пришлось взять plus пакета сообщений оказалось не очень много да и даже gpt-oss:20b нагружает не слабо видеокарту и медленно достаточно работает)):

• deepseek-v3.1:cloud:

• glm-5:cloud

• gpt-oss:120b-cloud

• gpt-oss:20b-cloud

Основные результаты исследования:

Давайте явно рассмотрим пример успешного и не успешного ответа:

cases‑V2E01

Нам нужно доказать «R → S», имея в предпосылка «R → S» для нас это достаточно просто это тождественно равные понятия от модели LLM мы ждём, что она не придумает новую математику, а корректно оформит её в виде сертификата.

Задача V2E01: «R→S»

Вот пример успешного созданного кандидат:

{
  // Начало объекта сертификата доказательства.

  "certificate_version": "1.0.0",
  // Версия формата сертификата.
  // Должна совпадать с поддерживаемой схемой сертификатов.

  "proof_id": "V2E01",
  // Идентификатор доказательства/кейса.
  // Должен совпадать с ID тестового примера или benchmark-case.

  "goal": "R -> S",
  // Целевая формула, которую сертификат должен вывести.
  // Финальный проверенный результат должен совпасть именно с этой формулой.

  "context": {
    // Метаданные о том, в каком формализме и для какого benchmark-а выдан сертификат.

    "domain": "hilbert-benchmark-v1",
    // Идентификатор домена/набора задач.
    // Используется для проверки, что сертификат относится к ожидаемому benchmark-контексту.

    "rule_pack": "classical-hilbert-v1",
    // Набор правил вывода.
    // Здесь: классическая гильбертовская система.

    "syntax": "hilbert-prop-ascii-v1",
    // Идентификатор синтаксиса формул.
    // Здесь ожидается ASCII-нотация пропозициональной логики.

    "generator": "llm-benchmark-v1"
    // Источник/тип генератора сертификата.
    // Это метка происхождения, а не сам шаг вывода.
  },
  // Конец блока context.

  "assumptions": [
    "R -> S"
  ],
  // Верхнеуровневый список допущений.
  // На них потом ссылаются шаги вида "assumption".
  // Здесь допущение одно: "R -> S".

  "steps": [
    // Список шагов доказательства.
    // Шаги проверяются по порядку; первый шаг имеет номер 1.

    {
      "kind": "assumption",
      // Тип шага.
      // "assumption" означает: этот шаг не выводит новую формулу,
      // а берет одну из формул из массива assumptions.

      "assumption_ref": 1,
      // Ссылка на элемент в массиве assumptions.
      // ВАЖНО: индекс здесь 1-based, не 0-based.
      // То есть 1 означает assumptions[0].

      "formula": "R -> S"
      // Формула, заявленная на этом шаге.
      // Для шага kind="assumption" она обязательна
      // и должна совпадать с формулой из assumptions по указанному assumption_ref.
    }
    // Единственный шаг доказательства:
    // "берем первое допущение, а это и есть R -> S".
  ]
  // Конец списка шагов.
}

вот пример не успешно созданного кандидат:

{
  "certificate_version": "1.0.0",
  "proof_id": "cases-V2E01",
  "goal": "R -> S",
  "context": {
    "domain": "hilbert-benchmark-v1",
    "rule_pack": "classical-hilbert-v1",
    "syntax": "hilbert-prop-ascii-v1",
    "generator": "llm-benchmark-v1"
  },
  "assumptions": [
    "R -> S"
  ],
  "steps": [
    {
      "kind": "assumption",
      "assumption_ref": 1
    }
  ]
}

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

V2E01 — entailed / assumption_import / easy

— Goal: R -> S

— Assumptions: R -> S

— Comment: Import a single assumption directly

Почему же так: всего не хватает «formula»: «R -> S», значит надо поменять promt, отчасти вы будете правы, но этот пример сам по себе не доказывает, что модель не способна решить такие задачи при другом promt или другой оболочке. Он показывает, что даже в простом случае модель может не превратить уже данное истинное утверждение в правильный формальный сертификат внутри нашего протокола.

Код я писал на Go, так как только изучаю мне помогал с этим Codex, мною проверена сама логика верификации + также выборочно проверены raw/result в artifacts, также буду очень благодарен если вы тоже посмотрите данный репозиторий и указали мне на ошибки или поможете в развитии кодовой базы для создания такого ядра верификации и исследовании других моделей и их пороги знаний.

Что доказано, а что нет:

Исследование показывает:

• LLM может выдать корректный сертификат, но делает это не стабильно

• Ядро верификации не даёт пройти некорректным кандидатам

• В узких классах задач это даёт рабочую границу доверия

Что исследование не показывает:

• Что LLM «Вообще не умеют рассуждать»

• Что ядро верификации уже готово для любого вида бизнес процессов

• Что RAG/fine-tuning бесполезны

• Что мои логические кейсы покрывают все реальные кейсы.

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

Идея проста: не доверять свободному тексту модели, если его нельзя проверить. Если LLM действительно смогла построить правильный вывод, это должно проявиться в виде сертификата, который проходит строгую верификацию. Если не смогла, система должна сказать не «похоже верно», а «сертификат отклонён».

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

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

Также хочу отметить научную статью Neural Theorem Proving for Verification Conditions: A Real-World Benchmark научное сообщество стремится к верификации логического рассуждения LLM моделей используя автоматические системы математических доказательств(Lean, Rocq, Isabelle) для того, чтобы верифицировать логические последовательности.

Я пришёл к тем же выводам о проблемах LLM моделей, которые получены в результате их исследования прошу посмотреть разделы данного исследования: "5.1 Results" и "5.2 Error Analysis of NTP models". (вот бы я ещё раньше бы нашёл, а не после первых промежуточных исследований, которые заняли 5 дней)

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

Открытый Github для более подробного изучения и результатов моего исследования

Открытый Github исследования, также полезно посмотреть вам

Нужно ещё многое сделать:

• полноценно внедрить Lean для исследовательских задач, кстати кто не видел посмотрите это правда интересная программа особенно для математиков.

• Добавить, чтобы провайдером была не только ollama, но и можно было подключать через llm.c модель, так как не все модели есть в ollama.

• Провести исследования на других моделях.

• Расширить языковую модель ядра верификации.

• Добавить новые гипотезы для исследования, тогда можно будет точнее определять границу доверия к моделям.

Ссылки на литературные источники:

Neural Theorem Proving for Verification Conditions: A Real-World Benchmark

Trustworthy Reasoning: Evaluating and Enhancing Factual Accuracy in LLM Intermediate Thought Processes

Why Language Models Hallucinate

AA-Omniscience: Evaluating Cross-Domain Knowledge Reliability in Large Language Models

Emerging Risks of AI-to-AI Interactions in Health Care: Lessons From Moltbook

Ссылка на информационный источник