Keystone

LLM va cheklovlar solverini birlashtirgan qaror mexanizmi

Keystone — operatsion rejalashtirish uchun sertifikatlangan qaror mexanizmi: xodimlar jadvalini tuzish, vazifalarni biriktirish, resurslarni taqsimlash, tanlash va moslashtirish. Jamoa qarorni ma’lumotlar jadvallari, oddiy tildagi qoidalar va maqsad ko‘rinishida tasvirlaydi, masalan: «avval mehnat xarajatini kamaytir, keyin smena bo‘yicha istaklarni hisobga ol». Keystone esa reja qaytaradi va unga har bir qat’iy qoidaga rioya qilingani hamda rejaning optimal ekanini isbotlovchi sertifikat ilova qiladi. Agar to‘g‘ri reja umuman mavjud bo‘lmasa, buning isbotini qaytaradi.

Biz uni AMD Developer Hackathon: ACT II’ning 3-yo‘nalishi (Track 3) uchun ikki kunda qurdik. Asosiy namunaviy soha — hamshiralar smenasini rejalashtirish: bu yerda xato javob qimmatga tushadi, shunchaki ishonarli ko‘ringan javob esa xavfli. Loyiha MIT litsenziyasi ostida va GitHub’da ochiq.

Nega faqat LLM xodimlar jadvalini tuza olmaydi

To‘plamdagi namunaviy masala 8 hamshiraning 10 ta smena bo‘yicha bir haftalik jadvalini qamrab oladi: bu 80 ta qaror o‘zgaruvchisi va 97 ta cheklov, ulardan 95 tasi qat’iy. Faqat LLM tuzgan rejaning narxi 2 816. Bu narxi 2 936 bo‘lgan Keystone rejasidan arzonroq, lekin faqat malakaga moslik bo‘yicha uchta qoidani buzgani uchun. Keystone rejasining optimalligi isbotlangan va barcha 95 ta qat’iy cheklov mustaqil ravishda qayta tekshirilgan.

Bu taqqoslash har bir ishga tushirishga o‘rnatilgan. Bazaviy reja ham Keystone rejasi o‘tadigan o‘sha verifikatordan o‘tadi, shuning uchun uning buzilishlari shunchaki da’vo qilinmaydi — ko‘rsatib beriladi.

Asosiy imkoniyatlar

• Taklif qil, qaror qil, sertifikatla — LLM faqat model qoralamasini tuzadi. Qarorni CP-SAT qabul qiladi, uni esa solverning o‘z hisobotiga hech qachon ishonmaydigan verifikator sertifikatlaydi.
• Yechim yo‘qligining isboti — reja umuman bo‘lishi mumkin bo‘lmasa, Keystone bir-biriga zid qoidalarning minimal to‘plamini qaytaradi. Masalan, dushanba ertalab ICU’ga ikkita hamshira talab qilinsa-yu, shtatda malakali hamshira bitta bo‘lsa, aynan shu qamrov va malaka juftligini ko‘rsatadi.
• Tekshirish va tuzatish sikli — LLM noto‘g‘ri tuzilgan model taklif qilsa, model tekshiriladi va xatolar bilan birga qaytarib yuboriladi; urinishlar sonini sozlash mumkin.
• Tabiiy tilda qayta yechish — «juma kechki smenasiga ikkinchi hamshira qo‘sh» kabi so‘rov masalani o‘zgartiradi va butun konveyerni qayta ishga tushiradi. Natijada yangi sertifikat hamda oldingi rejaga nisbatan farqlar (diff) qaytadi.
• Qamrov filtri — optimallashtirish masalasi bo‘lmagan ochiq savollar soxta modelga zo‘rlab tiqilmaydi: ular rad etiladi va savolni qanday qayta qo‘yish bo‘yicha taklif beriladi.
• Qaror paketi — har bir ishga tushirish masala, model, reja, sertifikat, bazaviy taqqoslash va izohni o‘z ichiga olgan bitta mustaqil JSON faylni eksport qiladi — rejani tasdiqlaydigan odam uchun.
• Operator konsoli — bitta fayldan iborat veb-interfeys konveyerni jonli oqimda ko‘rsatadi hamda jadval, sertifikat va faqat LLM rejasi bilan taqqoslashni chiqaradi.

Arxitektura va texnologiyalar

Konveyer

FastAPI servisi masalani JSON yoki CSV fayl ko‘rinishida qabul qiladi. Asinxron worker uni olti bosqichdan o‘tkazadi: qabul qilindi, modellashtirish, yechish, tekshirish, bazaviy reja va izohlash. Jarayon holati Server-Sent Events orqali jonli uzatiladi. Vazifalar va rejalar SQLite’da saqlanadi, uni bitta muhit o‘zgaruvchisi bilan Postgres’ga almashtirish mumkin.

Model, solver va verifikator

Oraliq model chegaralangan o‘zgaruvchilar ustidagi chiziqli butun sonli cheklovlardan foydalanadi. Ya’ni u to‘g‘ridan-to‘g‘ri CP-SAT cheklovlar solveriga tushadi va suzuvchi nuqtali taxminiy chegaralarsiz, aniq butun sonlar bilan qayta tekshirilishi mumkin. Yumshoq istaklar vaznli jarimalarga aylanadi.

Asosiy yechish bir nechta worker va qat’iy belgilangan seed bilan ishlaydi, shuning uchun sertifikatlangan natijalarni aynan takrorlash mumkin. Ziddiyatli to‘plamlar CP-SAT’ning taxminlar yadrolaridan (assumption cores) olinadi. Solver hech qachon soxta (mock) bilan almashtirilmaydi: oflayn mock rejimida faqat LLM soxta javob bilan almashtiriladi, shuning uchun kafolat birorta ham API kalitisiz saqlanib qoladi.

LLM yo‘nalishlari va AMD hisoblash quvvati

Gemma modelni OpenAI bilan mos keladigan yagona kod yo‘li orqali taklif qiladi, bu yo‘lning uchta varianti bor: Google AI Studio, Fireworks AI yoki AMD Instinct MI300X’da vLLM orqali ishga tushirilgan Gemma.

Asosiy bajarilish tekshiruvi PyTorch’da ham ROCm’da ishlaydigan paketli float32 matritsa ko‘paytmasi sifatida amalga oshirilgan. Testlar uning natijasi CPU verifikatorinikiga bitma-bit mos kelishini tasdiqlaydi; u juda katta jadvallar uchun GPU’da saralanadigan katta qo‘shnilik qidiruvini (large-neighborhood search) boshqaradi. Bitta notebook xuddi shu «avval yech, keyin sertifikatla» yo‘lini 10 080 o‘zgaruvchi va 31 179 qat’iy cheklovdan iborat jadvalgacha kengaytiradi.

Sifat

Repozitoriyda model, solver, verifikator, GPU baholovchisi, turli sohalar uchun quruvchilar, konveyer va REST API’ni qamrab olgan 52 ta muvaffaqiyatli test bor. Ular orasida adversarial ko‘rib chiqishdan kelib chiqqan regressiya testlari ham bor: o‘sha ko‘rib chiqish o‘zgaruvchi nomlari to‘qnashuvini aniqlagan, bu xato esa xodim yetishmaydigan jadvalni sertifikatlab yuborishi mumkin edi. Yengil (slim) va ROCm uchun Dockerfile’lar ham qo‘shilgan.

Nimani topshirdik

Xakaton davomida quyidagilarni ishga tushirdik:

• to‘liq backend
• oflayn yechiladigan to‘rtta masala shakli: biriktirish, taqsimlash, tanlash va moslashtirish
• veb-konsol
• ovozli izohli demo video
• haqiqiy solver va verifikator bilan mock rejimida ishlaydigan jonli demo

Ogohlantirish mahsulotning o‘zida bor. Sertifikat rejaning modellashtirilgan cheklovlarga mos kelishini isbotlaydi, lekin model barcha mehnat qoidalarini qamrab olganini isbotlamaydi — shuning uchun har bir rejani inson ko‘rib chiqishi kerak.

Tegishli ishlar

Keystone — sun’iy intellekt integratsiyasi va avtomatlashtirish bo‘yicha ishlarimizdan biri. Xuddi shu xakatonda qurilgan boshqa loyihalar: RecipeReel, Legible va Testify. Sun’iy intellekt qat’iy tekshiruv bosqichlari ichida ishlaydigan yana bir tizimni ko‘rish uchun Opus Magnum loyihasiga qarang.