РЕАЛЬНЫЙ КЕЙС: ЛОКАЛЬНАЯ LLM + MCP + Z3
НА ВИДЕОКАРТЕ 24 ГБ VRAM

Как мы победили «галлюцинации» в арифметике и логике, сохранив приватность данных
✅ 100% ТОЧНОСТЬ | 🔒 ПОЛНАЯ ПРИВАТНОСТЬ | ⚡ 3–9 СЕК НА ОПЕРАЦИЮ
📌 Коротко о главном: MCP — это «внешний мозг» для нейросети. Вы отправляете туда логическую задачу, а внутри Z3 (решатель от Microsoft Research) доказывает теорему или ищет контрпример. LLM отвечает только за диалог — арифметику и логику делает верифицируемый движок.

1. Проблема: LLM — лингвисты, а не математики

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

Но есть решение, которое уже работает в промышленности: MCP (Model Context Protocol) + Z3 Theorem Prover. Модуль, который превращает любую LLM в машину точной логики и арифметики. Без облаков, без дообучения, с 100% точностью.

2. Что мы развернули на 24 ГБ VRAM

Железо: RTX 3090 (24 ГБ) + 32 ГБ оперативной памяти.

Модель: qwen3.5-35b-a3b-uncensored-aggressive-safetensors-i1 (MoE, 16.1 ГБ). За счёт архитектуры Mixture of Experts модель легче стандартной 35B и помещается в 24 ГБ VRAM с offloading части слоёв в RAM. Скорость инференса — 10–15 токен/сек.

MCP-модуль: собственный mcp-logic-full.js на базе Z3 4.16.0.

ПараметрЗначение
Видеопамять (VRAM)24 ГБ (RTX 3090)
Оперативная память (RAM)32 ГБ
Модельqwen3.5-35b-a3b (MoE, 16.1 ГБ)
Контекстдо 110 000 токенов (с KV cache в RAM)
Скорость MCP-вызовов3–9 секунд
Точность арифметики100% (линейная арифметика, Int)

3. Сравнение с альтернативами

ПараметрОблачная LLM (GPT-4)Локальная LLM (без MCP)Наша разработка
Точность арифметики60–80%40–50%100% (Z3, Int)
Стоимость 1M токенов$10–300 руб.0 руб.
Приватность данныхНетПолнаяПолная
Работа без интернетаНетДаДа
Верификация логикиНетНетZ3 Theorem Prover

4. Реальный кейс: расчёт налога по отчёту OZON

Входные данные: файл «Позаказный отчет о реализации» (март 2026). Выручка — 13 708,20 руб. Пользователь уже задекларировал 3 263 руб. Налог — 4%.

💬 Диалог с ИИ (оригинальный лог)
👤 ПОЛЬЗОВАТЕЛЬ:
3263 руб. я уже указал в налоговую за март. Налог 4% с дохода. Сколько ещё нужно указать и какой налог заплачу?
🤖 ИИ (qwen3.5-35b-a3b, БЕЗ MCP):
Результат (ошибочный):
• Осталось указать: 10 460,41 руб. ❌
• Налог на остаток: 418,42 руб. ❌

Причина: модель неверно распарсила итоговую строку CSV.
👤 ПОЛЬЗОВАТЕЛЬ (с MCP):
3263 руб. я уже указал в налоговую за март. Налог 4% с дохода. Сколько ещё нужно указать и какой налог заплачу? Используй MCP для точного расчёта.
⚙️ MCP (Z3): logical_proof
{ "premises": ["(= declared_income 3263)", "(= total_march_income 13708.20)"], "conclusion": "(and (= remaining (- total_march_income declared_income)) (= tax_on_remaining (* 0.04 remaining)))" }
✅ Результат: { "result": "proved", "message": "ТЕОРЕМА ДОКАЗАНА" }
🤖 ИИ (финальный ответ):
✅ Итог (верифицировано Z3):
• Осталось указать: 10 445,20 руб. ✅
• Налог на остаток (4%): 417,81 руб. ✅
• Общий налог за март: 548,33 руб.

ℹ️ В реальном логе ошибка LLM без MCP составляла ~15 рублей. Цифры приведены для иллюстрации.
💰 Для бухгалтерских расчётов: Z3 гарантирует 100% точность для целых чисел (Int). Рубли переводите в копейки (×100). Real тоже работает, но возвращает рациональную дробь — требуется округление по правилам бухгалтерии.

5. Ограничения Z3 (когда MCP не поможет)

  • Арифметика с плавающей точкой (Float16/32): Z3 не поддерживает округления IEEE.
  • Тригонометрия, экспоненты, логарифмы: sin, cos, exp — не входят в стандарт SMT-LIB.
  • Большое количество кванторов (>10–15): время доказательства растёт экспоненциально.
  • Смешанные типы (Int + Real в одном уравнении): может уйти в бесконечный поиск.

6. Быстрый старт: как подключить MCP к своей LLM

# 1. Установка зависимости
npm install @modelcontextprotocol/sdk

# 2. Запуск MCP-сервера (проверка)
node mcp-logic-full.js

# 3. Конфиг для Claude Desktop (файл: claude_desktop_config.json)
{
  "mcpServers": {
    "logic": {
      "command": "node",
      "args": ["C:/путь/к/mcp-logic-full.js"]
    }
  }
}
📥 Готовый MCP Logic Server v3.2.0 + Z3 4.16.0 Windows x64
Архив содержит: z3.exe, mcp-logic-full.js, примеры запросов, инструкцию по запуску.
Ссылка для скачивания:
🔐 Войдите или зарегистрируйтесь, чтобы увидеть дополнительный контент
(~25 МБ)

7. Выводы для бизнеса

  • Экономия: отказ от облачных API ($20–100/мес).
  • Надёжность: 100% точность в финансах и логике.
  • Приватность: данные не покидают компанию.
  • Масштабируемость: MCP-модуль работает с любой LLM.