🔑 Keystone

An LLM proposes, an exact solver decides, an independent verifier certifies.

Built for the AMD Developer Hackathon: ACT II — Track 3 (Unicorn) · powered by AMD Instinct MI300X + ROCm + Gemma.

🎬 Watch the narrated demo · ▶ Live demo — infra.tailc95f92.ts.net:8443 — instant, offline, no keys, no signup.

● Live · MIT licensed · 52 tests passing · Docker · MI300X · ROCm · Gemma

---

Ask a chatbot for a staff schedule and it hands you a plausible, cheaper, INFEASIBLE plan. Keystone proves feasibility AND optimality — or proves no plan exists.

Keystone turns a business decision — data tables + natural-language rules + an objective — into a certified plan. Gemma reads the problem and proposes a formal optimization model (an IR); Google OR-Tools CP-SAT solves it to optimality; and an independent verifier re-checks every hard constraint from scratch with exact integer arithmetic and issues a machine-checkable Certificate. On an impossible problem it returns the minimal conflicting constraint set — why no plan exists. The hero domain is verifiable workforce / nurse shift scheduling.

On the bundled fixtures/sample_problem.json ("St. Regis Medical" — a week for 8 nurses across Mon–Fri AM/PM = 10 shifts, 80 decision variables, 97 constraints of which 95 are hard):

	Objective (labor cost)	Status	Hard constraints	Deployable?
Raw-LLM / greedy baseline	2816 (cheaper — it cheats)	❌ INFEASIBLE	3 violations (all skill_match)	No
Keystone	2936	✅ OPTIMAL (proven)	all 95 certified	Yes

That is the wedge: the naive answer is cheaper but not deployable — it staffs ICU shifts with unqualified nurses. Keystone's answer is provably feasible and provably optimal, and the same independent verifier is what exposes the baseline. A chatbot can't hand you that guarantee; a solver + verifier structurally can.

Why it's different (the guarantee)

Gemma PROPOSES  ─►  CP-SAT DECIDES  ─►  INDEPENDENT verifier RE-CHECKS  ─►  Certificate
 (formal model)     (exact optimum)     every hard constraint, exact ints    (feasible + optimal,
                                        — never trusts the solver's word      or minimal conflict)

• The verifier is independent. It re-derives the certificate from the IR + the returned assignment alone, re-evaluating every hard constraint from scratch with exact integer arithmetic. It never takes the solver's word for feasibility — or for optimality.
• INFEASIBLE is a first-class answer. When no schedule can exist, Keystone proves it and returns the minimal conflict set. On fixtures/infeasible_problem.json (two ICU nurses demanded Monday morning, only one ICU-qualified nurse on staff) it returns {coverage:mon_am, skill:mon_am} — the exact pair of rules that cannot both hold.
• The solver is never mocked. MOCK_MODE stubs only the LLM. The exact OR-Tools CP-SAT solve and the independent verification always run for real — deterministic, local, seeded, reproducible.
• Contrast a raw-LLM scheduler: it emits a plan that looks right, is unverifiable, and quietly violates hard constraints. Keystone runs that exact baseline through the same verifier and shows it failing, head-to-head.

Live demo & how to run it (for judges)

▶ Always-on demo: https://infra.tailc95f92.ts.net:8443/ — click it and use it; no signup, no keys.

• How it's hosted (accurate): self-hosted — Docker on a Linux VPS, exposed to the public internet via a Tailscale Funnel (that's why the URL is a *.ts.net address). It runs always-on in MOCK_MODE.
• MOCK_MODE is a feature, not a shortcut: the whole propose → decide → certify pipeline runs offline with zero API keys — and the exact CP-SAT solver + independent verifier still run for real (only the LLM is stubbed). Judges get the full guarantee instantly, on a laptop or the live URL, with nothing to configure.

Run it yourself — two commands, offline, no keys:

pip install -r requirements-dev.txt
MOCK_MODE=true uvicorn app.main:app          # → http://localhost:8000  (console + /docs)

Or one Docker command (the same image the live demo runs):

docker build -t keystone . && docker run --rm -p 8000:8000 keystone   # → :8000, mock mode

Then open the root URL for the Keystone console (submit a problem, watch the pipeline stream, read the certificate + the raw-LLM head-to-head), or POST fixtures/sample_problem.json to the API (see Quickstart). To swap in real Gemma, drop in a .env — see Use of AMD Platforms.

Architecture

Heavy compute on the AMD MI300X (the "Use of AMD Platforms" story); reasoning / model proposal on Gemma. Every stage is a pluggable provider with a mock impl, so the service is always runnable.

POST a Problem (data tables + NL rules + NL objective)
        │
  received   ── parse + validate the problem
        │
  modeling   ── Gemma PROPOSES a formal IR (vars, linear constraints, objective)  ── Gemma (vLLM on MI300X)
        │        validate-and-repair loop (MODEL_MAX_REPAIRS) if the IR is malformed
        │
  solving    ── OR-Tools CP-SAT decides to optimality        ── ortools (CPU) | gpu_lns (MI300X LNS)
        │
  verifying  ── INDEPENDENT verifier re-checks every hard constraint (exact integers) → Certificate
        │
  baseline   ── raw-LLM / greedy plan run through the SAME verifier (the head-to-head wedge)
        │
  explaining ── plain-English rationale for the decision
        │
  done       ── certified Plan + self-contained decision-pack  ── SQLite store · REST + SSE

The GPU-batched constraint evaluator (Keystone's core check, as a float32 matmul), the gpu_lns search that rides on it, and Gemma proposing the model are the AMD-accelerated pieces (see Use of AMD Platforms); the exact CP-SAT solve and the verifier run anywhere, GPU or not.

Quickstart

Zero setup — mock mode runs the whole pipeline offline (no keys, no GPU, no network). The solver and verifier still run for real.

python -m venv .venv && . .venv/bin/activate
pip install -r requirements-dev.txt

# Serve the API in mock mode (the zero-config demo path; also how CI runs):
MOCK_MODE=true uvicorn app.main:app            # → http://localhost:8000  (/docs for interactive)

# In another shell — end-to-end demo (submit → poll → certified plan + decision-pack):
./scripts/demo.sh

Then open http://localhost:8000 for the Keystone console — a black-and-silver operator UI that submits a problem, streams the propose → decide → certify pipeline live, and renders the certified roster, the independent certificate, the raw-LLM head-to-head, and the plain-English "argue with it" command bar. It's a single self-contained file (app/web/index.html) served by the API, so docker run ships it too. The interactive API docs stay at /docs.

Or via the Makefile / Docker:

make dev            # uvicorn with autoreload, mock mode
make test           # pytest (52 tests)
docker compose up   # serves :8000 in mock mode; drop in a .env to switch on real providers

Submit a problem and read the certificate

curl -s -X POST localhost:8000/api/v1/problems \
     -H 'content-type: application/json' \
     --data @fixtures/sample_problem.json         # → 202 {"id": "<job_id>", ...}

# poll GET /api/v1/jobs/<job_id> until status=succeeded, then read the plan:
curl -s localhost:8000/api/v1/plans/<plan_id> | jq

The certified Plan (shape, with the verified sample_problem.json numbers):

{
  "status": "OPTIMAL",
  "objective": 2936,                     // total labor cost — proven minimal
  "certificate": {
    "feasible": true,
    "proven_optimal": true,              // solver proved optimality AND verifier confirms feasibility
    "objective": 2936,                   // recomputed independently from the IR
    "optimality_gap": 0.0,
    "soft_penalty": 10,                  // one nurse's preference was cost-dominated
    "checked_constraints": 95,           // every hard constraint re-verified from scratch
    "violations": [],
    "conflict": []
  },
  "baseline": {                          // raw-LLM / greedy — run through the SAME verifier
    "approach": "raw_llm",
    "feasible": false,                   // INFEASIBLE — not deployable
    "objective": 2816,                   // cheaper, because it cheats
    "violation_count": 3                 // all in the skill_match family
  },
  "schedule": [
    { "shift": "mon_am", "shift_name": "Mon AM", "day": "mon", "staff": ["Casey"], "headcount": 1 }
    // …one row per shift…
  ],
  "explanation": "…plain-English rationale…",
  "conflict": [],                        // populated instead of a schedule on INFEASIBLE
  "stats": { "num_variables": 80, "num_constraints": 97, "num_hard_constraints": 95,
             "solver": "ortools", "modelbuilder": "mock", "device": "cpu" }
}

GET /api/v1/plans/<plan_id>/decision-pack returns the full self-contained export — { problem, ir, plan, certificate, baseline_comparison, explanation, conflict, stats, guarantee, disclaimer } — the shippable artifact you hand to whoever signs off on the roster.

Real Gemma, free, no credit card (Google AI Studio)

Proposing the optimization model from a natural-language problem is a pure-text task, so Gemma being text-only on the Google shim is exactly right — this product uses real Gemma, no multimodal workaround. Get a free key (no card), then:

MODELBUILDER=fireworks \
  FIREWORKS_API_KEY=<your Google AI Studio key> \
  FIREWORKS_BASE_URL=https://generativelanguage.googleapis.com/v1beta/openai/ \
  SYNTH_MODEL=gemma-4-31b-it \
  uvicorn app.main:app

API

Method	Path	Purpose
POST	/api/v1/problems	Submit a decision problem (data tables + NL rules + NL objective) → 202 {id}
POST	/api/v1/problems/upload	Submit a problem as a .json Problem or .csv roster
GET	/api/v1/jobs/{id}	Job status + progress
GET	/api/v1/jobs/{id}/events	Live pipeline progress (SSE)
GET	/api/v1/jobs	List jobs
GET	/api/v1/plans/{id}	The certified Plan (assignment, certificate, baseline, schedule)
GET	/api/v1/plans/{id}/decision-pack	Full self-contained decision bundle (JSON)
POST	/api/v1/plans/{id}/resolve	Re-solve under a modification ({modification_nl, patch?})
GET	/api/v1/plans	List plans (compact cards)
GET	/health, /api/v1/meta	Health + active providers / solver / GPU

Interactive docs at /docs once running.

Providers & configuration

Every var has a safe default; with none set, the app boots in mock mode offline. See .env.example for the full list.

Env var	Values / default	Purpose
MOCK_MODE	false	true ⇒ the LLM stages use their deterministic mock (no GPU/network/keys). The solver + verifier always run for real.
MODELBUILDER	fireworks · amd · mock	Who proposes the IR: Gemma via Fireworks / Google AI Studio shim · Gemma via local vLLM on the MI300X · deterministic mock.
SOLVER	ortools · gpu_lns	ortools = CP-SAT on CPU (runs anywhere) · gpu_lns = MI300X large-neighborhood search. Never mocked.
FIREWORKS_API_KEY / FIREWORKS_BASE_URL / SYNTH_MODEL	— / Fireworks or Google shim / gemma-4-31b-it	OpenAI-compatible Gemma endpoint. Point FIREWORKS_* at Google AI Studio for free Gemma, no card.
AMD_LLM_BASE_URL / AMD_LLM_MODEL / AMD_LLM_API_KEY	http://localhost:8001/v1 / google/gemma-3-27b-it / EMPTY	vLLM-hosted Gemma on the MI300X (MODELBUILDER=amd) — targets the $2k "Best AMD-Hosted Gemma" prize.
SOLVER_TIME_LIMIT_SECONDS / SOLVER_WORKERS / SOLVER_SEED	30 / 8 / 42	CP-SAT tuning. Fixed seed → reproducible, certifiable results.
MODEL_MAX_REPAIRS	2	Retries to repair an invalid Gemma-proposed IR.
MAX_UPLOAD_MB / DATA_DIR / DATABASE_URL	64 / ./data / sqlite:///./data/keystone.db	Upload cap + storage.

The hero domain: shift scheduling

A Problem is a set of workers (skills, weekly-hours cap, hourly cost, unavailability, preferences) and shifts (day, hours, demand, optional required skill), plus natural-language rules and an objective. The model builder compiles those NL rules into these exact constraint families, and the verifier re-checks each one independently:

Family	Meaning
coverage	Every shift is staffed to its demand.
capacity	No worker exceeds their weekly-hours cap.
no_overlap	At most one shift per worker per day.
skill_match	Only qualified workers cover a shift that requires a skill.
availability	A worker marked unavailable for a shift is never assigned it.
min_rest	At least min_rest_hours of rest between consecutive-day shifts.
preference	Soft — honoring a requested shift avoids a weighted penalty.

Objective: minimize total labor cost, then honor preferences (soft, weighted). Bundled fixtures: sample_problem.json (the OPTIMAL hero case), infeasible_problem.json (proves impossibility + names the conflict), and baseline_violation_case.json (a tiny case that isolates the cost-only-heuristic failure mode).

Re-solve. POST /api/v1/plans/{id}/resolve takes a natural-language modification (and/or a structured patch) — "Casey called in sick Wednesday", "add a second nurse to Friday PM" — mutates the problem, re-runs the full pipeline, and returns a fresh certified plan plus a diff against the parent (added/removed assignments, objective delta). Every re-solve is certified from scratch.

Use of AMD Platforms

The AMD Instinct MI300X (192 GB HBM3, ~5.3 TB/s, gfx942) runs Keystone's heaviest step. A runnable, end-to-end demo lives in notebooks/amd_keystone_demo.ipynb — execute it on the MI300X pod to light up the Instinct card (GET /api/v1/meta also reports the live eval device).

• GPU-batched constraint verification — Keystone's core operation, on the MI300X. Checking a schedule against every hard constraint is X @ Aᵀ compared to the demands — a matrix multiply. app/services/solve/gpu_eval.py runs it as a batched float32 matmul (BLAS on CPU, tensor cores on the MI300X), scoring feasibility + cost for hundreds of thousands of candidate schedules per second on the MI300X (a device projection — the notebook prints the measured on-device rate; CPU here runs ~13k–155k/sec). It is bit-exact here — every constraint sum is a small integer well within float32's 2²⁴ range — and the tests assert it agrees with the independent CPU verifier bit-for-bit. This is genuine AMD compute doing the work at the heart of the guarantee, not a wrapper around an API call.
• gpu_lns — GPU-screened large-neighborhood search. Finds an incumbent with CP-SAT, then each round screens a large batch of candidate neighborhoods on the GPU (the evaluator above) and re-optimizes the neighborhood exactly — reporting the real count of GPU-evaluated candidates (lns_candidates). Falls back to CPU-only LNS when torch is absent.
• Gemma proposes the model on the MI300X. Serve Gemma with the rocm/vllm image (vllm serve google/gemma-3-27b-it, OpenAI-compatible) via scripts/serve_amd_gemma.sh, then set MODELBUILDER=amd. On ROCm, torch.cuda.is_available() is True and torch.version.hip is set — the same code path runs on laptop CPU and on the MI300X. This targets the $2k "Best AMD-Hosted Gemma" prize.
• Three Gemma routes, ONE code path. Gemma proposes the IR over an OpenAI-compatible call, so the three ways to run it differ only in base_url / model / key: (1) vLLM-on-MI300X (rocm/vllm, the AMD-hosted route above), (2) Google AI Studio — free real Gemma, no credit card (get a key), and (3) Fireworks AI — the fast, reliable hosted option (itself served on AMD Instinct). Proposing the model is a pure-text task, so text-only Gemma is exactly right here — real Gemma, no multimodal workaround.
• Verification stays independent. Every result — GPU-batched or not — is re-checked by the independent verifier. The GPU accelerates the guarantee; it never replaces it.

Scaling beyond the hackathon

Keystone is a general certified-decision engine, not a one-domain demo — the same compile → solve → verify core already answers assignment · scheduling · allocation · selection · matching · sequencing shapes, and a scope-gate honestly declines what it can't prove instead of fabricating an answer.

• Vertical wedges from one engine. Nurse rostering today; the identical pipeline certifies logistics allocation, portfolio/grant selection, interview and mentor matching, field-service routing — each a regulated back-office decision that needs an auditable proof, not a plausible guess.
• Throughput scales on AMD. The float32-matmul batch evaluator screens hundreds of thousands of candidates/sec on the MI300X (device projection; ~13k–155k/sec on CPU here), and gpu_lns rides it to push large-neighborhood search on very large rosters — the notebook builds a 10,080-variable / 31,179-hard-constraint instance and runs it end-to-end through the same solve-then-independently-certify path (execute it on the MI300X pod for the live solver status + throughput). AMD-hosted Gemma via vLLM removes the LLM as the bottleneck for high propose throughput.
• Ops scale is boring on purpose. Stateless FastAPI + async worker + SSE; SQLite for the demo, swap DATABASE_URL for Postgres to go multi-node; every stage is a pluggable provider with a mock fallback, so the service is always up even when a dependency is down.
• The decision-pack is the product. Each run emits a self-contained, machine-checkable export (problem · ir · plan · certificate · baseline · guarantee) — the artifact a compliance owner, auditor, or ops lead signs off on. That auditability is the moat a chatbot can't cross.

Tests

make test        # or: python -m pytest   (52 tests, all green — no key, no GPU)

52 tests, all green (no API key, no GPU), covering the model builder / IR, the OR-Tools solver, the independent verifier, the GPU-batched evaluator (skipped without torch), the multi-shape domains (assignment · allocation · selection · matching + the scope-gate), the end-to-end mock pipeline, and the REST API — including regression tests for the adversarial-review findings (test_models · test_solver · test_verifier · test_gpu_eval · test_domains · test_pipeline_mock · test_api). The GPU evaluator is asserted to agree with the independent verifier bit-for-bit.

Submission checklist

Required for submission	Where
Public GitHub repo	https://github.com/avinmaster/keystone
README (setup + usage)	this file
Containerized (Dockerfile)	Dockerfile (slim) · Dockerfile.rocm (MI300X) · docker-compose.yml
MIT-licensed	LICENSE
Live Application URL	https://infra.tailc95f92.ts.net:8443/
Demo Application Platform	self-hosted — Docker on a Linux VPS, exposed via a Tailscale Funnel
Use of AMD compute	AMD MI300X notebook notebooks/amd_keystone_demo.ipynb + app/services/solve/gpu_eval.py
Gemma	MODELBUILDER=fireworks|amd — three routes, one code path (see Use of AMD Platforms)
Cover (near-16:9 — crop/pad to 1920×1080) · video (MP4 < 5 min) · slide deck	attached to the lablab form — copy-paste field values in docs/SUBMISSION.md

License

MIT © 2026 Keystone contributors.

Disclaimer

Keystone is illustrative optimization software, not operational or legal advice. Constraints and costs are modeled from the data you provide; the constraint families and sample rosters ship as a starting template. Certificates prove that a plan satisfies the modeled constraints — they do not certify that the model captures your real-world policy, labor law, or safety requirements. Review every plan before operational use.