README.md

# Digitable

We build **Digit**, a local agent for the Russian-language course platform
[courses.digitable.life](https://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](https://github.com/digitable-lol/flang) 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`](https://huggingface.co/digitable-lol/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`](https://huggingface.co/digitable-lol/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`](https://huggingface.co/digitable-lol/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`](https://huggingface.co/digitable-lol/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`](https://huggingface.co/datasets/digitable-lol/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`](https://huggingface.co/datasets/digitable-lol/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`](https://huggingface.co/datasets/digitable-lol/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`](https://huggingface.co/datasets/digitable-lol/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](https://courses.digitable.life). Ограничение архитектуры
необычное: языковой модели запрещено быть источником фактов. Содержание ответа даёт
детерминированная утилита, дословная цитата из корпуса курсов или формальный сертификат.
Модель выбирает, что вызвать, — либо пишет артефакт, который затем проверяет программа.

**Здесь лежат маршрутизаторы и генератор спецификаций, а не универсальные ассистенты.**
Маршрутизатор относит запрос к категории инструментов и извлекает аргументы либо
отказывается; ответ он не пишет. Генератор спецификаций пишет исполняемые документы
[FTS](https://github.com/digitable-lol/flang) — и им тоже не доверяют: их компилируют,
типизируют, исполняют и доказывают настоящим инструментарием.

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

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

**Второе: фильтр, который никогда ничего не отверг, — не доказательство.** Фраза «все
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` соответствующего
репозитория.