Аким на 5 часов — AI-симулятор управления городом

Команда BEZBAB · HackAlem AI · задача «Аким на 5 часов».

Веб-симулятор, в котором пользователь с единым бюджетом 100 единиц принимает ровно 5 управленческих решений для 5 районов Астаны (синтетические данные задачи). Система считает Astana Quality of Life Score строго по формулам задания, предлагает 5 оптимальных стратегий, объясняет сильные стороны, риски и последствия каждого сценария и сравнивает его со всеми 694 395 допустимыми наборами. Математика модели и оптимизатора формально проверена в Z3 и Lean 4 + Mathlib.

Работа доступна на HithubPages https://mikhail31415.github.io/BAITC-Hacks-hack-ccf09524-bezbab-result/

Запуск за 1 минуту: нужен только Python 3.8+ и браузер. Установка пакетов, аккаунты и API-ключи не нужны.

git clone https://github.com/BAITC-Hacks/hack-ccf09524-bezbab.git
cd hack-ccf09524-bezbab
python server.py

Откройте http://127.0.0.1:8000.

Содержание

1. Описание решения и назначение
2. Системные требования и зависимости
3. Установка
4. Запуск
5. Параметры окружения
6. Проверка основного сценария
7. Автоматические тесты и формальная проверка
8. Архитектура
9. Используемые технологии
10. Модель расчёта (строго по условию)
11. Как устроен AI
12. Стратегии, страховка от событий, настройки модели
13. Соответствие задаче
14. Сторонние компоненты, данные и AI-инструменты
15. Потенциал развития и ограничения
16. Соответствие README требованиям Положения

1. Описание решения и назначение

Проблема. При развитии города нужно одновременно учитывать транспорт, экологию, социальную инфраструктуру, безопасность и городские сервисы, а ресурсов не хватает на всё. Любое распределение бюджета — это компромисс, и его последствия для разных районов неочевидны.

Пользователь. Городской управленец, аналитик или участник симулятора.

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

• Показывает исходное состояние города: 5 районов × 10 показателей, критические значения, исходный Score = 52.56.
• Предлагает 5 стратегий — наборов из 5 мероприятий с разными приоритетами (максимальный результат, резерв на ЧС, поддержка отстающих, улучшения для всех районов, быстрый эффект), с таблицей сравнения.
• Даёт доработать стратегию или собрать свой набор из 14 мероприятий. Бюджет и правила задачи контролируются автоматически, недопустимые варианты блокируются с объяснением причины.
• Для выбранного сценария: итоговый Score с формулой, AI-аналитик (сильные стороны, риски, последствия для жителей, компромиссы), вклад каждого решения, место среди всех допустимых сценариев, устойчивость, стресс-тест городскими событиями и перераспределение бюджета.
• Страховка от городских событий: резерв под выбранные события закладывается заранее, и стратегии пересчитываются.
• Сравнение команд по коду или ссылке и автогенерация презентации решения (5 слайдов, печать в PDF).

Ценность. Решение показывает не только «сколько баллов», но и почему: какие меры дали прирост, кто из жителей выиграл, где риск и чем оплачен компромисс. Лучшие варианты найдены полным перебором, а не подбором вручную.

2. Системные требования и зависимости

Компонент	Требование	Обязателен	Назначение
ОС	Windows 10/11, macOS, Linux	да	проверено на Windows 10
Python	3.8 или новее, только стандартная библиотека	да	локальный веб-сервер server.py (проверено на 3.10)
Браузер	Chrome / Edge / Яндекс Браузер 100+, Firefox 115+, Safari 16.4+	да	интерфейс: ES-модули, Web Worker, import maps
Интернет	не обязателен	нет	только шрифты Google Fonts; без интернета используется системный шрифт
Git	любой	нет	чтобы клонировать репозиторий (можно скачать ZIP)
Node.js	20+	нет	запуск тестов через node --test (проверено на 24)
anthropic (Python)	актуальная версия, pip install anthropic	нет	LLM-объяснение (нужен ключ Anthropic)
z3-solver (Python)	≥ 4.12, pip install -r verification/requirements.txt	нет	формальная проверка Z3
Lean 4 + Mathlib	elan, Lean v4.33.1, Mathlib v4.33.1 (~5 ГБ)	нет	формальные доказательства

Сборка, npm-пакеты, база данных и Docker не нужны. Вся основная функциональность работает офлайн, без личных аккаунтов, подписок и ключей (п. 5.6.6 Положения).

3. Установка

git clone https://github.com/BAITC-Hacks/hack-ccf09524-bezbab.git
cd hack-ccf09524-bezbab

Больше ничего устанавливать не нужно. Вместо git clone можно скачать ZIP-архив ветки main на GitHub и распаковать его.

Необязательные компоненты:

# LLM-объяснение (иначе объяснения строит аналитик на правилах)
pip install anthropic

# формальная проверка Z3
pip install -r verification/requirements.txt

4. Запуск

Из корня репозитория:

ОС	Команда
Windows	python server.py или py server.py
macOS / Linux	python3 server.py

В консоли появится Откройте http://127.0.0.1:8000. Откройте этот адрес в браузере. Остановить сервер — Ctrl+C.

• Другой порт: python server.py --port 8010, тогда адрес будет http://127.0.0.1:8010.
• Открывать index.html двойным кликом нельзя: браузеры не загружают JavaScript-модули по file://. Сервер нужен именно для этого.
• При первом открытии оптимизатор 0,5–1 с перебирает все наборы в фоне. В правом верхнем углу появится «Проверено 694 395 сценариев · максимум 57.24».

Если что-то пошло не так

Симптом	Решение
python не найден	Windows: py server.py; macOS/Linux: python3 server.py
«Порт 8000 занят»	python server.py --port 8010
Открылся другой или старый интерфейс	На порту 8000 уже работает другой сервер (Windows позволяет двум процессам слушать один порт). Запустите на другом порту: --port 8010
Пустая страница	Откройте через http://127.0.0.1:…, а не как файл; обновите браузер до версии из раздела 2
Остались изменения модели или страховки с прошлого запуска	⚙ → «Вернуть модель ТЗ»; снимите галочки страховки; или очистите данные сайта в браузере

5. Параметры окружения

Для основной функциональности переменные окружения не нужны.

Параметр	Тип	По умолчанию	Назначение
--port	аргумент server.py	8000	порт веб-сервера (слушает только 127.0.0.1)
ANTHROPIC_API_KEY	переменная окружения	не задана	включает LLM-объяснение (нужен пакет anthropic)
ANTHROPIC_AUTH_TOKEN / ANTHROPIC_PROFILE	переменная окружения	не задана	альтернативные способы авторизации SDK Anthropic
AKIM_MODEL	переменная окружения	claude-opus-5	модель Claude для LLM-объяснения

Включить LLM-объяснение:

# Windows (PowerShell)
$env:ANTHROPIC_API_KEY = "ваш-ключ"; python server.py
# macOS / Linux
ANTHROPIC_API_KEY="ваш-ключ" python3 server.py

Без ключа сервер пишет LLM-объяснение: выключено … работает объяснение по правилам, и приложение работает полностью. Ключ хранится только на сервере и не попадает в браузер.

Браузер хранит в localStorage таблицу команд, изменённую модель и отметки страховки. Серверной базы данных нет.

6. Проверка основного сценария

Пошаговый чек-лист, ~5 минут. Все ожидаемые числа проверены на свежем клоне ветки main.

#	Действие	Ожидаемый результат
1	Запустите python server.py, откройте http://127.0.0.1:8000	Справа вверху «Проверено 694 395 сценариев · максимум 57.24». Блок «Город до ваших решений»: исходный Score 52.56, 5 районов, у Нуры красным «Школы и детсады 38» и «Поликлиники 35»
2	Прокрутите до «Выберите стратегию»	5 карточек: Максимальный результат 57.24, Надёжный с резервом 57.09, Поддержка отстающих 55.43, Улучшения для всех районов 55.95, Быстрый эффект 56.05. Ниже таблица сравнения со звёздочками ★
3	Нажмите «Выбрать» на «Максимальный результат»	Раздел результата: 57.24, формула 0.7 × 58.58 + 0.3 × 54.09 (Нура) − 0 = 57.24, «Место среди всех допустимых: 1 из 694 395». Ниже AI-аналитик (объяснение, сильные стороны, риски, последствия для жителей), «Вклад каждого решения» (сумма = +4.68), графики, районы до/после
4	Кнопка «Собрать свой набор ↗» → в тёмной панели «Пример из ТЗ» → «Рассчитать сценарий»	Score 56.54, стоимость 95, место 566 из 694 395. В сильных сторонах: «Сработала синергия «Освещение и камеры…» + «Единая цифровая платформа обращений»»
5	Контроль бюджета: «Изменить состав» → уберите «Единая цифровая платформа обращений» (×)	Расход 81. У «Линия ЛРТ / расширение» кнопки районов заблокированы, подсказка «Не хватает 11 ед. бюджета». При 5 выбранных мерах остальные заблокированы: «Уже выбрано 5 решений — уберите одно»
6	Изменение решений меняет Score: верните платформу обращений, у «Перевод частного сектора на чистое топливо» нажмите «Алматы» вместо «Сарыарка»	Прогноз Score меняется 56.54 → 56.58
7	Закройте конструктор. В «Страховке от городских событий» отметьте «Авария на теплотрассе зимой»	Стратегии пересчитываются: «Максимальный результат» 57.23, «Резерв под страховку: нужно 6 · есть 9» — оптимизатор сам взял «Аварийные бригады ЖКХ», и ликвидация подешевела с 12 до 6 ед. Снимите галочку — снова 57.24
8	В результате сценария, блок «Стресс-тест» → «Перераспределить» у непокрытого события	Варианты перестройки набора (1, 2, … изменения) с Score, ценой мер и ликвидации, кнопка «Применить»
9	Внизу результата: «Сохранить результат», «Сгенерировать презентацию»	Сценарий появляется в таблице команд; открывается 5 слайдов с кнопкой «Печать / PDF»
10	Откройте http://127.0.0.1:8000/tests.html	«16 из 16 тестов пройдено»

Кнопка добавления мероприятий там:

Дополнительно: ⚙ в правом верхнем углу — «Настройки модели» (раздел 12).

7. Автоматические тесты и формальная проверка

Проверка	Команда	Ожидаемый результат	Время
Тесты модели в браузере, без Node.js	http://127.0.0.1:8000/tests.html	16 из 16	~5 с
Те же тесты в Node.js 20+	node --test	pass 16, fail 0	~4 с
Тесты сервера и стража чисел LLM (без ключей и сети)	python -m unittest test_server.py	OK (6 тестов)	< 1 с
Z3, быстрая проверка (глобальный оптимум)	python verification/z3_verify.py --quick	Итог: 19/19 проверок пройдено, код выхода 0	~5 мин
Z3, полная проверка (+ вся граница Парето)	python verification/z3_verify.py	Итог: 37/37 проверок пройдено	~25 мин
Lean 4 + Mathlib	см. ниже	компиляция без ошибок и без sorry	~5 мин + загрузка Mathlib

engine.test.mjs — один и тот же файл для Node и браузера: в tests.html модули node:test, node:assert/strict, node:fs подменяются браузерными заглушками через import map. Тесты сверяют JS-расчёт с verification/expected.json — тем же файлом, который независимо проверяют Z3 и Lean.

Что проверяет Z3 (verification/spec.py — независимая транскрипция условия, verification/z3_verify.py — SMT-модель над точными рациональными числами):

• data.mjs совпадает с условием задачи (14 мер, 5 районов, веса), суммы весов и долей населения равны 1;
• оценки районов совпадают с таблицей ТЗ, базовый Score ровно 52.55768;
• пример из ТЗ, самый дешёвый набор и оптимум допустимы, их Score совпадает в точном расчёте Python, в SMT-модели и в JS;
• минимальная стоимость допустимого набора — 61 (Z3 minimize);
• глобальный оптимум 57.236735 доказан: запрос «существует набор со Score больше» — unsat;
• все 11 точек границы «бюджет → максимальный Score» оптимальны (полный режим);
• независимый перебор в Python даёт те же 694 395 допустимых наборов.

Что доказано в Lean 4 + Mathlib (verification/lean/AkimScore.lean): нормировка весов и долей; базовый Score, Score примера и оптимума — точные равенства в ℚ, проверенные ядром Lean (decide +kernel, не native_decide); пример и оптимум удовлетворяют правилам; оценки районов ∈ [0, 100], Score ≤ 100; монотонность — улучшение любых показателей не снижает Score; эффективность вкладов — сумма маргинальных вкладов по любому порядку и среднее по всем порядкам (значение Шепли) равны приросту Score.

# нужен elan (https://github.com/leanprover/elan); первая загрузка Mathlib ~5 ГБ
cd verification/lean
lake exe cache get
lake env lean AkimScore.lean

8. Архитектура

Клиент-серверное веб-приложение без сборки. Вся модель и оптимизатор работают в браузере. Python-сервер только раздаёт файлы и, если задан ключ, проксирует LLM-объяснение.

flowchart LR
  D[data.mjs<br/>датасет ТЗ, события,<br/>настраиваемая модель] --> E[engine.mjs<br/>Score, правила, Шепли,<br/>Монте-Карло, стресс-тест,<br/>страховка]
  E --> O[optimizer.mjs<br/>точный перебор,<br/>5 стратегий, Парето]
  O --> W[optimizer.worker.mjs<br/>Web Worker]
  E --> X[explain.mjs<br/>AI-аналитик]
  W --> UI[main.mjs + index.html<br/>интерфейс]
  X --> UI
  UI --> ME[model-editor.mjs<br/>настройки модели]
  UI --> C[charts.mjs<br/>SVG-графики]
  UI --> R[report.mjs<br/>презентация]
  UI -- факты --> S[server.py /api/explain<br/>LLM + страж чисел]
  E -. утверждения .-> J[verification/expected.json]
  J --> Z[Z3: z3_verify.py]
  J --> L[Lean 4 + Mathlib]
  J --> T[engine.test.mjs]

Поток данных. data.mjs → engine.mjs считает любой набор решений → optimizer.mjs в Web Worker перебирает все допустимые наборы (с учётом страховки) и возвращает распределение, стратегии и границу Парето → main.mjs рисует стратегии и результат, explain.mjs формирует объяснение из готовых чисел → при наличии ключа server.py переписывает объяснение через LLM, и каждое число сверяется с фактами.

Файл	Назначение
index.html, styles.css	Разметка и стили страницы
main.mjs	Интерфейс: стратегии, страховка, конструктор, результат, команды, запуск оптимизатора
data.mjs	Датасет ТЗ (районы, показатели, веса, 14 мер, синергии, несовместимости), городские события, применение и проверка изменённой модели
engine.mjs	Модель: применение мер, Score, валидатор с причинами, значения Шепли, устойчивость, стресс-тест, стоимость ликвидации и резерв, коды сценариев
optimizer.mjs, optimizer.worker.mjs	Точный перебор, 5 стратегий, граница Парето, ядро лучших решений, лучшая одиночная замена, перераспределение после события
explain.mjs	AI-аналитик (правила) и пакет фактов для LLM
model-editor.mjs	Окно «Настройки модели»: мероприятия, веса, синергии, взаимоисключения, события, формула
charts.mjs, report.mjs	SVG-графики и презентация решения
server.py	Статический сервер без кэша, GET /api/status, POST /api/explain (LLM + страж чисел)
engine.test.mjs, tests.html, tests/	16 тестов модели, оптимизатора, стратегий, страховки и настроек (Node или браузер)
test_server.py	Тесты стража чисел и безопасного отключения LLM
verification/	expected.json (утверждения), spec.py + z3_verify.py (Z3), lean/ (Lean 4 + Mathlib)

9. Используемые технологии

Слой	Технологии
Интерфейс	HTML5, CSS3, JavaScript (ES-модули), Web Worker, SVG. Без фреймворков, без сборки, без npm
Сервер	Python 3, стандартная библиотека (http.server, json, argparse)
Расчёт и оптимизация	Собственный детерминированный движок по формулам ТЗ; точный перебор с отсечениями и инкрементальным пересчётом; значения Шепли; Монте-Карло с фиксированным зерном
AI	Объяснимый аналитик на правилах; необязательно — Claude через официальный SDK anthropic со стражем чисел
Проверка	node:test / браузерный раннер, Python unittest, SMT-решатель Z3, Lean 4 + Mathlib

10. Модель расчёта (строго по условию)

• Показатель после мер: I'_dk = clip(I_dk + Σ эффект × (8 − L)/8 + синергии, 0, 100). Горизонт — 8 кварталов, L — лаг (срок запуска) меры. Районная мера действует в выбранном районе, городская — во всех пяти.
• Синергии («Выделенные полосы» + «Умные светофоры», «Освещение и камеры» + «Платформа обращений», «Чистое топливо» + «Городское озеленение») дают фиксированный бонус в районе первой меры пары, лагом он не масштабируется.
• Несовместимости: автобусные полосы и ЛРТ — везде; парк и школа, чистое топливо и модернизация сетей — в одном районе.
• Оценка района D_d = Σ w_k × I'_dk с весами ТЗ (сумма 1).
• Score = 0.7 × Σ pop_d × D_d + 0.3 × min D_d − N_crit, где N_crit — число пар «район × показатель» строго ниже 40.
• Правила: бюджет 100, ровно 5 решений, без повторов, район только у районных мер, не больше 2 мер из одного направления, несовместимости запрещены. Недопустимый набор не считается, валидатор называет причину.
• Контрольные значения совпадают с условием: база 52.55768; пример из ТЗ 56.54307 (стоимость 95, синергия «Освещение и камеры» + «Платформа обращений»); самый дешёвый набор — 61 ед.

Все эффекты мер кратны 1/8, поэтому расчёт в double точен: сложение и вычитание эффектов при переборе не накапливают погрешность.

Что показывают данные: разброс Score среди допустимых наборов — 52.04–57.24, то есть неудачный выбор может даже ухудшить город. Максимум — 57.24 за 98 ед. Вариант «с резервом» — 57.09 за 86 ед.: он уступает всего 0.15 п., но закрывает все 4 городских события. «Центр семейного здоровья» в Нуре входит в 100% из 2000 лучших наборов.

11. Как устроен AI

Решение построено как нейро-символическая система: числа считает проверяемая модель, объясняет — аналитик и (по желанию) LLM.

1. Детерминированная модель (engine.mjs) считает Score по формулам ТЗ, проверяет правила и выдаёт причины отказа.
2. Оптимизатор (optimizer.mjs, в Web Worker) точно перебирает пространство: C(14,5) наборов мер × до 5⁵ размещений ≈ 1,4 млн вариантов, из них 694 395 допустимых, за ~0,5 с. Отсечения по бюджету, лимиту направления и несовместимостям; эффект меры прибавляется при входе в ветку и вычитается при выходе. Результат — 5 стратегий с разными целями (отличаются минимум двумя решениями), распределение Score, граница Парето, «ядро» лучших решений.
3. Вклад решений — значения Шепли: вклад каждой меры усредняется по всем порядкам добавления, поэтому сумма вкладов в точности равна приросту Score, включая синергии и штрафы.
4. Неопределённость — Монте-Карло: 400 прогонов с эффектами ±20% и вероятностью 25% задержки запуска на квартал; фиксированное зерно даёт всем командам одинаковый результат.
5. Аналитик (explain.mjs) формирует сильные стороны, риски, последствия для жителей и компромиссы только из чисел модели: снятые и оставшиеся критические значения, показатели «на грани», смена слабейшего района, меры с малым вкладом, долгий запуск, побочные эффекты, непокрытые события.
6. LLM-объяснитель (необязательный, server.py): Claude получает JSON с готовыми фактами и пишет связный текст. Страж чисел проверяет каждое число ответа по фактам; при расхождении показывается объяснение аналитика.

12. Стратегии, страховка от событий, настройки модели

5 стратегий. Максимальный результат; Надёжный с резервом (резерв на ликвидацию любого события); Поддержка отстающих (максимум оценки слабейшего района); Улучшения для всех районов (максимум наименьшего прироста); Быстрый эффект (только меры с запуском за 1–2 квартала). У каждой карточки кнопки «Выбрать» и «Изменить состав», под карточками таблица сравнения.

Городские события (синтетическое расширение, на официальный Score не влияют): авария на теплотрассе, смог, всплеск набора в школы, серия ДТП. У события есть район, удар по показателям, стоимость ликвидации и профильные меры. Если профильная мера есть в районе события или действует на весь город, ликвидация дешевле (по умолчанию на 50%), а удар слабее.

• Страховка (до решения): отмеченные события закладываются в резерв, режим «одно событие за 2 года» или «все отмеченные сразу». Резерв считается для каждого набора с учётом профильных мер, и стратегии подбираются заново с условием «стоимость мер + резерв ≤ 100».
• Стресс-тест (после решения): для выбранного набора видно, какие события покрыты резервом и сколько баллов теряется при остальных. «Перераспределить» ищет наборы, на которые хватит денег вместе с ликвидацией, и показывает цену перестройки.

Настройки модели — неприметная кнопка ⚙ в правом верхнем углу:

• вкладки «Мероприятия» (правка и добавление мер), «Веса показателей», «Синергии», «Взаимоисключения», «События» (правка и добавление событий);
• свёрнутый блок «Для опытных: формула итоговой оценки»: веса «средняя / слабейший район», порог и штраф критических значений и штраф за отставание районов − λ × Σ max(0, T − D_d) (при λ = 0 — формула ТЗ);
• правки применяются после проверки; ошибки блокируют применение, предупреждения — нет;
• пока математика отличается от ТЗ, вверху висит плашка с кнопкой «Вернуть модель ТЗ», а упоминания Z3/Lean скрыты. Для защиты используется модель ТЗ.

13. Соответствие задаче

Требование задачи	Где реализовано
Единый бюджет и исходные данные для всех	data.mjs: 100 ед., датасет ТЗ; сверка с условием — verification/z3_verify.py
5 решений по заданным направлениям	5 стратегий по 5 мер (optimizer.mjs → STRATEGY_DEFS) и конструктор из 14 мер; правила ТЗ в engine.mjs → validate
Автоматический контроль бюджета	Недопустимые кнопки заблокированы с причиной; validate() отклоняет набор; тесты и Z3
AI-анализ решений	Аналитик (explain.mjs), оптимизатор, значения Шепли, Монте-Карло, стресс-тест; LLM со стражем чисел
Расчёт Astana Quality of Life Score	engine.mjs → scoreCells, строго по формуле ТЗ; значения доказаны в Lean
Сильные стороны, риски и последствия	Блок «AI-аналитик» и «Главные компромиссы»
Опц.: сравнение команд	Таблица сценариев, импорт по коду или ссылке #s=…, попарное сравнение
Опц.: визуализация изменений районов	Карточки «до → после», гистограмма всех сценариев, граница Парето
Опц.: AI-рекомендации	5 стратегий с таблицей сравнения, лучшая одиночная замена, ядро лучших решений
Опц.: неожиданные события и перераспределение	Страховка с пересчётом стратегий, стресс-тест, перераспределение, редактор событий
Опц.: автогенерация презентации	report.mjs: 5 слайдов, печать в PDF
Критерий: изменение решений меняет Score	Шаг 6 чек-листа; тест changing a decision changes the Score

14. Сторонние компоненты, данные и AI-инструменты

Раскрытие по п. 5.4.4 Положения. Весь код приложения создан командой в этом репозитории с помощью AI-ассистентов (см. ниже). Сторонние JS-библиотеки и CDN-скрипты не используются.

Компонент	Где используется	Лицензия / источник	Обязателен
Стандартная библиотека Python 3	server.py	PSF License	да
Шрифты Manrope и DM Sans (Google Fonts)	styles.css (@import)	SIL Open Font License 1.1	нет — без интернета системный шрифт
Синтетический датасет (районы, показатели, 14 мер, синергии, несовместимости, формула)	data.mjs, verification/spec.py	условие задачи «Аким на 5 часов» (организатор)	да
Городские события и их параметры	data.mjs → EVENTS	придуманы командой, синтетические	нет
anthropic — Python SDK Anthropic	server.py (LLM-объяснение)	MIT	нет
Модель Claude (Anthropic API)	/api/explain	коммерческий API, ключ пользователя	нет
z3-solver — SMT-решатель Z3 (Microsoft Research)	verification/z3_verify.py	MIT	нет
Lean 4 и Mathlib	verification/lean/	Apache 2.0	нет
Node.js (node:test)	запуск тестов	MIT	нет

AI-инструменты разработки (разрешены п. 5.4.12): при разработке команда использовала AI-ассистентов — OpenAI Codex и Claude Code (Anthropic) — для генерации и анализа кода, тестирования и документации. История разработки — в этом репозитории.

15. Потенциал развития и ограничения

Развитие и масштабирование

• Реальные данные. Модель задаётся данными (data.mjs и «Настройки модели»): её можно наполнить открытыми данными Астаны или другого города, откалибровать эффекты мер по фактическим проектам.
• Другие города и отрасли. Тот же подход «ограниченный бюджет → стратегии → объяснимый результат» подходит для здравоохранения, образования и инфраструктурных программ.
• Большие каталоги мер. Точный перебор работает до ~15 млн вариантов. Для больших каталогов та же SMT-кодировка из z3_verify.py служит точным оптимизатором без полного перебора.
• Командный режим. Серверная таблица результатов для хакатонов, обучения госслужащих и стратегических сессий.
• Агентный LLM-слой. Вопросы на естественном языке («что будет, если перенести школу в Есиль?») с вызовом того же проверяемого движка и стражем чисел.

Ограничения

• Данные и эффекты синтетические. Для реальных решений нужны открытые данные, калибровка и экспертная проверка причинно-следственных связей.
• Сценарии команд хранятся в браузере (localStorage) и передаются кодом или ссылкой. Общего серверного рейтинга пока нет.
• LLM-объяснение требует ключа Anthropic; без него работает аналитик на правилах.
• Формальная проверка относится к модели ТЗ; изменённые в настройках модели проверяются тестами и полным перебором, но не Z3/Lean.

16. Соответствие README требованиям Положения

Требование (п. 5.4.15, 5.6.4, 5.6.6, 5.4.4)	Раздел
Описание решения и его назначения	1
Описание архитектуры	8
Используемые технологии	9
Инструкции по установке	3
Инструкции по запуску	4
Необходимые зависимости и системные требования	2
Параметры окружения	5
Порядок проверки основного сценария	6, 7
Проверка без личных аккаунтов и ключей	2, 5
Раскрытие сторонних компонентов	14