Keystone

Движок принятия решений, в котором LLM работает в паре с солвером ограничений

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

Мы сделали его за два дня для трека 3 хакатона AMD Developer Hackathon: ACT II. Главная предметная область — графики смен медсестёр: здесь неправильный ответ обходится дорого, а просто правдоподобный — опасен. Проект распространяется по лицензии MIT и открыт на GitHub.

Почему одна LLM не справится с графиком смен

Встроенная демонстрационная задача охватывает одну неделю для 8 медсестёр и 10 смен — это 80 переменных решения и 97 ограничений, из которых 95 жёсткие. План, который составляет для неё голая LLM, стоит 2 816. Это дешевле, чем 2 936 у Keystone, но только потому, что он нарушает три правила соответствия квалификации. План Keystone доказанно оптимален, а все 95 жёстких ограничений перепроверяются независимо.

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

Ключевые возможности

• Предложить, решить, сертифицировать — LLM только набрасывает модель. Решение принимает CP-SAT, а сертифицирует его верификатор, который никогда не верит собственному отчёту солвера.
• Доказанная невыполнимость — когда плана быть не может, Keystone возвращает минимальный набор конфликтующих правил. Например, если в понедельник утром в реанимации нужны две медсестры, а квалифицированная в штате только одна, он называет ровно эту пару: требование к покрытию смены и требование к квалификации.
• Цикл проверки и исправления — если LLM предлагает некорректную модель, та проверяется и отправляется обратно вместе со списком ошибок; число повторных попыток настраивается.
• Пересчёт по запросу на естественном языке — запрос вроде «добавь вторую медсестру на пятничную вечернюю смену» меняет задачу и заново запускает весь пайплайн. На выходе — новый сертификат и дифф с предыдущим планом.
• Фильтр по области применения — открытые вопросы, в которых нет задачи оптимизации, Keystone отклоняет и подсказывает, как их переформулировать, — вместо того чтобы втискивать их в фиктивную модель.
• Пакет решения — каждый запуск экспортирует один самодостаточный JSON-файл с задачей, моделью, планом, сертификатом, сравнением с базовым планом и объяснением — для того, кто утверждает решение.
• Консоль оператора — веб-интерфейс в одном файле показывает работу пайплайна в реальном времени и выводит график, сертификат и сравнение с планом голой LLM.

Архитектура и технологический стек

Пайплайн

Сервис на FastAPI принимает задачу в виде JSON или загруженного CSV-файла. Асинхронный воркер проводит её через шесть этапов: получение, моделирование, решение, проверка, базовый план и объяснение. Ход выполнения транслируется через Server-Sent Events. Задачи и планы хранятся в SQLite, которую одна переменная окружения меняет на Postgres.

Модель, солвер и верификатор

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

Основное решение считается на нескольких воркерах с фиксированным сидом, поэтому сертифицированные результаты воспроизводимы. Наборы конфликтов берутся из ядер допущений (assumption cores) CP-SAT. Солвер никогда не подменяется заглушкой: офлайн-режим с моками заменяет только LLM, поэтому гарантия сохраняется даже без единого API-ключа.

Маршруты LLM и вычисления на AMD

Gemma предлагает модель через единый OpenAI-совместимый код с тремя маршрутами: Google AI Studio, Fireworks AI или Gemma, развёрнутая через vLLM на AMD Instinct MI300X.

Основная проверка допустимости также реализована на PyTorch — как пакетное умножение матриц в float32, которое выполняется на ROCm. Тесты подтверждают, что она совпадает с CPU-верификатором бит в бит, а на её основе работает поиск по большой окрестности (large-neighborhood search) с отбором кандидатов на GPU для очень больших графиков. Jupyter-ноутбук масштабирует тот же путь «решить, затем сертифицировать» до графика с 10 080 переменными и 31 179 жёсткими ограничениями.

Качество

В репозитории 52 проходящих теста: они покрывают модель, солвер, верификатор, GPU-вычислитель, построители задач для разных предметных областей, пайплайн и REST API. Среди них — регрессионные тесты по итогам ревью, на котором код намеренно пытались сломать: оно выявило коллизию имён переменных, из-за которой сертификат мог получить график с нехваткой персонала. В комплекте — облегчённый Dockerfile и Dockerfile для ROCm.

Что мы сделали

За время хакатона мы выпустили:

• весь бэкенд
• четыре типа задач, которые решаются офлайн: назначение, распределение, отбор и подбор пар
• веб-консоль
• демо-видео с озвучкой
• живое демо, которое работает в режиме моков с настоящими солвером и верификатором

Оговорка — часть продукта. Сертификат доказывает, что план удовлетворяет смоделированным ограничениям, но не что модель учитывает все трудовые правила, поэтому каждый план должен проверить человек.

Смежные работы

Keystone — часть нашей работы по внедрению ИИ и автоматизации. Другие проекты с того же хакатона — RecipeReel, Legible и Testify. Ещё одну систему, где ИИ работает внутри строгих шагов проверки, смотрите в кейсе Opus Magnum.