digitable-lol/README

Digitable

We build Digit, a local agent for the Russian-language course platform courses.digitable.life. Its design constraint is unusual: the language model is not allowed to be a source of facts. Every fact in an answer comes from a deterministic utility, a verbatim quote from the course corpus, or a formal certificate — the model only chooses which of those to invoke, or writes the artefact that a checker then verifies.

What is in this organisation

Two lines of work, and neither produces a general-purpose assistant.

Routers map a user query to a tool category and emit a tool call with extracted arguments — or refuse. They never write the content of an answer. Load one as a chat model and you will get nonsense, and none of our published metrics describe that use.

The specification generator writes executable FTS specifications from a task stated in ordinary Russian. Its outputs are not trusted either: they are compiled, type checked, executed and proved by a real toolchain, and only what survives counts.

Models

Repository	What it is
digit-router-0.6b	The shipping router. LoRA adapters (v1/v2/v3) over Qwen/Qwen3-0.6B plus merged GGUF quantisations. 424 MiB at Q5_K_M, ~500 ms per full two-step routing cycle on 8 CPU threads.
digit-router-1.7b	The same training run at 1.7B. Higher routing accuracy; measurably not worth 3× the parameters for this task.
digit-router-experiments	Three adapters that lost — Vikhr, ruadapt, QVikhr-3. Published so the negative result stays reproducible instead of becoming folklore.
specgen-qwen3-1.7b	Writes executable FTS specifications from Russian prose. 99.4 % of its output passes the real compiler on a 1 500-document held-out set in which every document is new in its structural template, its subject area, or both; the untuned base scores 0. 133 MiB of LoRA, trained in 57 minutes inside 10 GiB.

Datasets

Repository	What it is
digit-router-dataset	34 709 Russian rows for the two-step router over a 95-utility catalogue. 23.8 % are refusals, and that fraction is the point.
hard-negatives-ru	8 470 machine-verified near-miss question–chunk pairs, 2 967 paraphrases, and a 498-item twins set on which a zero-false-accept threshold was measured to cost 94 % of recall.
digit-eval-tasks	400 Russian evaluation tasks, 250 main and 150 red-team, for a system required to answer only from a tool, a quote or a certificate.
fts-specgen-dataset	10 500 "Russian task → executable FTS specification" pairs, every one compiler-checked — plus a negative control of 4 400 deliberately corrupted documents measuring what the checker misses.

How to read our numbers

Three conventions run through every card, and each exists because the obvious way to report these numbers is misleading:

• A counted refusal is not a conscious refusal. An eval harness scores an unparseable answer as a refusal, so a model that merely breaks scores like a model that knows when to decline. We always report both columns. The untuned 0.6B base scores 75.3 % counted against 9.3 % conscious — a 66-point gap that is entirely broken output.

• A filter that never rejects anything is not evidence. "All 10 500 documents passed the compiler" is worth nothing until somebody shows the compiler can fail things, so fts-specgen-dataset ships 4 400 documents corrupted on purpose in eleven ways and the verdict on each. The gate catches 91.6 %; the card names the three corruptions it catches worst and why. That measurement also changed the work: one class was caught 5.0 % of the time until the generator was taught to emit boundary examples, after which it was 72.8 %.

• Known defects are stated before the good tables, not in a footnote. The imatrix quantisation of the 0.6B router measurably breaks its ability to refuse and carries a do-not-deploy warning next to the file. At Q4 the routers emit structurally flawless tool calls with invented arguments, and a GBNF grammar does not catch that. Our v3 adapters are a routing regression against v2 on a single seed. The spec generator omits the theorem in 127 of 1 491 otherwise-valid documents, and its own training data turns out never to have shown it a utility and a theorem in the same document — a hole found only after the model made it visible. All of this is on the model pages.

A fourth, specific to the verified work: compiling is not meaning. Our gate proves a specification parses, type checks, runs its own examples and proves its own theorem. It does not prove the document says what the request asked for. We have not measured that, and we say so rather than letting a 99.4 % imply it.

Every published file's sha256 is recorded in a MANIFEST.json in its repository. We track runs by weight hash rather than by tag, because a tag was once re-created from a different build while a 250-task evaluation was in flight.

Base models are Qwen/Qwen3-* under Apache-2.0. The router training data is derived from a GPL-3.0 utility catalogue; we state that provenance on every page and do not claim to have resolved what it means for weights. The FTS work has no such question — the language, the compiler and the gate are ours under BSD-2-Clause — and the cards say so plainly instead of reusing the cautious wording where it is not needed.

---

По-русски

Мы делаем Digit — локального агента для платформы курсов courses.digitable.life. Ограничение архитектуры необычное: языковой модели запрещено быть источником фактов. Содержание ответа даёт детерминированная утилита, дословная цитата из корпуса курсов или формальный сертификат. Модель выбирает, что вызвать, — либо пишет артефакт, который затем проверяет программа.

Здесь лежат маршрутизаторы и генератор спецификаций, а не универсальные ассистенты. Маршрутизатор относит запрос к категории инструментов и извлекает аргументы либо отказывается; ответ он не пишет. Генератор спецификаций пишет исполняемые документы FTS — и им тоже не доверяют: их компилируют, типизируют, исполняют и доказывают настоящим инструментарием.

Три правила чтения наших чисел.

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

Второе: фильтр, который никогда ничего не отверг, — не доказательство. Фраза «все 10 500 документов прошли компилятор» ничего не стоит, пока не показано, что компилятор вообще способен что-то отвергнуть. Поэтому в fts-specgen-dataset опубликованы 4 400 намеренно испорченных документов (одиннадцать видов порчи) и вердикт по каждому. Гейт ловит 91,6 %, и в карточке названы три вида порчи, которые он ловит хуже всего, и почему. Этот замер ещё и изменил работу: один класс ловился на 5,0 %, пока генератор не научили добавлять граничные примеры, — после этого 72,8 %.

Третье: известные дефекты стоят до таблиц с хорошими числами, а не в примечаниях. imatrix-квант 0.6B ломает способность отказываться и помечен как непригодный к поставке; при Q4 модель выдаёт структурно безупречные вызовы с выдуманными аргументами, и грамматика этого не ловит; адаптеры v3 — измеренный регресс против v2 на одном seed; генератор спецификаций теряет теорему в 127 документах из 1 491 формально валидных — и его обучающие данные, как выяснилось, ни разу не показали ему утилиту и теорему в одном документе.

И четвёртое, для верифицированной части: компилируется — не значит «означает». Гейт доказывает, что документ разбирается, типизируется, исполняет свои примеры и доказывает свою теорему. Что он означает ровно то, что просили словами, — не доказывает. Мы это не измеряли и пишем об этом прямо, а не даём числу 99,4 % намекнуть на большее.

sha256 каждого опубликованного файла записан в MANIFEST.json соответствующего репозитория.