0. Two adapters live in this repository. Read this first.
This repository has been published twice. Both adapters are here, neither is hidden, and
each one names the revision of the training data it was built from. A number quoted
without that pairing is meaningless, because the two revisions of the corpus differ in ways
that changed the model's behaviour.
Table with columns: revision 2 — current, revision 1 — previous | revision 2 — current | revision 1 — previous |
|---|
| where | repository root | previous/data-rev1/ |
| trained on | dataset revision 2, 11 000 rows | dataset revision 1, 9 000 rows |
| training data defects | none known | two, both listed below |
| passes the compiler (1 500 holdout) | 1 499/1 500 (99.9 %) | 1 492/1 500 (99.5 %) |
| means what the task asked | 1 392/1 500 (92.8 %) | 1 257/1 500 (83.8 %) |
| writes the theorem when asked | 453/453 (100 %) | 324/453 (71.5 %) |
| writes both calculations when asked | 20/20 | 0/20 |
| marks both optional fields when asked | 2/108 | 21/108 |
| GGUF | gguf/specgen-1.7b-v2-Q5_K_M.gguf | gguf/specgen-1.7b-v1-Q5_K_M.gguf |
Both columns are measured on the same 1 500 documents — the holdout of dataset
revision 2 — with the same greedy decoding and the same compiler. That matters: 64 of the
1 500 task texts changed between the revisions (revision 1 chose the phrasing register
non-reproducibly), so the previous adapter's outputs were regenerated on the new
prompts rather than carried over from its own publication run. The revision-1 numbers you
may have read on this page before — 1 491/1 500 and 83.8 % — were measured on the
revision-1 holdout and are reproduced in § 2.3 for continuity.
Revision 2 is better on every headline and worse on exactly one thing, and that one
thing is named, measured and explained in § 1.3 rather than buried. It is not caused by the
data fix.
What changed in the data between the revisions
Revision 1 of fts-specgen-dataset
carried two defects and one gap, all three of which this adapter's predecessor inherited:
- The gap: not one of the 9 000 training documents contained a utility and a theorem
at the same time. The
CMB-UTL-THM holdout template asks for both; the previous adapter
produced the theorem 0 times out of 129.
- The defect: 416 of 10 500 published documents answered a task naming two
calculations with a document containing one — the corpus generator printed both into
the task and only the first into the document. The previous adapter learned that mapping
exactly and reproduced it 20 times out of 20.
- Two smaller ones: 448 documents carried float noise (
7.199999999999999) that fell
outside the GBNF grammar after it was narrowed, and the phrasing register was chosen
non-reproducibly.
Revision 2 fixes all of them. Revision 2 of the corpus measures 0 two-calculation
divergences over all 12 950 documents and conforms to the grammar 12 950 of 12 950.
1. Read this before you read any number
1.1 The gate proves compilation, not meaning — and both are reported
This is the single most important sentence on this page.
Every "passes the compiler" number is produced by running the model's output through the
actual FTS toolchain: compile → validate (with coverage analysis) → testUtilities
(executes every пример in the document) → for documents with a theorem, prove +
certify + verifyCertificate. A document that passes has been proven well-formed,
well-typed, self-consistent and internally proved.
It has not been proven to mean what the task asked for in words. A document that
compiles perfectly while computing the wrong thing passes the gate.
So meaning is measured separately, and by a different instrument. The task text is parsed by
an independent reader into the same shape the compiler builds from the document, and the two
are compared element by element. That comparison's sensitivity is itself measured: 8 600
of 8 600 deliberate corruptions were caught (4 800 mutations of the document, 3 800 of the
task), and its six declared blind spots — changes that must not count, such as
«текст» ↔ строка — were verified to be silent.
Table with columns: verdict on this adapter's 1 500 holdout documents, count| verdict on this adapter's 1 500 holdout documents | count |
|---|
| means exactly what the task asked | 1 392 (92.8 %) |
| means something different | 108 (7.2 %) |
| did not compile at all | 0 |
Against the previous adapter's 1 257 (83.8 %), 235 and 8 on the same 1 500 tasks.
The honest reading of this page is: 99.9 % of outputs are valid FTS, and 92.8 % of outputs
mean what was asked. Those are two different numbers about two different things.
1.2 The two inherited defects are closed
Both defects that the previous adapter carried are gone, and each was checked with the
instrument that found it rather than by eye.
Table with columns: previous adapter, this adapter | previous adapter | this adapter |
|---|
CMB-UTL-THM — task asks for a calculation and a theorem | theorem present 0/129 | 129/129 |
| all templates whose reference has a theorem | 324/453 | 453/453 |
CMB-TWO-UTIL — task asks for two calculations | second one written 0/20 | 20/20 |
| extended holdout, 450 documents that all need both | theorem present 0/450 | |
The CMB-TWO-UTIL row is not an eyeball count of утилита blocks. It is the same
task-versus-document comparison used to find the defect in the corpus: on all 20 documents
the number of utilities now agrees with the task (utilities/<количество> divergences:
20 → 0).
One CMB-TWO-UTIL document still diverges, for an unrelated reason: CMB-TWO-UTIL:telecom:0
writes an example whose expected result the interpreter disagrees with
(FTS_EXAMPLE_MISMATCH on a boundary case, expected 0, got 0.2). It is the only
document in the whole 1 500 that the compiler rejects.
1.3 What got worse: optional fields, 21/108 → 2/108
This is a regression and it is not caused by the data fix.
The OBJ-OPTIONAL holdout template has 108 documents. Every one of their tasks names
exactly two optional fields ("«дата старта» — дата, необязательное"), and every
reference document marks exactly two (иногда является). The adapter must mark both.
Table with columns: correct on OBJ-OPTIONAL, documents emitting 0 / 1 / 2 marks | correct on OBJ-OPTIONAL | documents emitting 0 / 1 / 2 marks |
|---|
| previous adapter (data rev 1, 9 000 rows) | 21/108 | 47 / 40 / 21 |
| this adapter (data rev 2, 11 000 rows) | 2/108 | 43 / 40 / 25 |
Note the second column: this adapter emits the right number of marks slightly more often
(25 vs 21) and is still right less often, because it puts them on the wrong fields. It drops
the mark from the date field 106 times and invents one on the boolean field 23 times.
The cause is the 2 000 extra training rows, not the corrected data. The intermediate
adapter that added the same 2 000 rows to the uncorrected revision-1 corpus scores
2/108 as well — identically. Its full report ships as
eval/rev2/semcheck.ml32-trained-on-rev1.holdout.jsonl so this can be checked rather than
taken on trust. The data fix moved CMB-TWO-UTIL from 20 divergences to 0 and left
OBJ-OPTIONAL exactly where it was.
The root cause is in the training distribution, and it is exact:
OBJ-OPTIONAL is a held-out template — no training document has that shape. Optional
fields appear in training only inside CMB-STRUCT-UTL and CMB-STRUCT-UTL-THM, and there
they appear exactly once per document, always. Of the 11 000 training rows, 797 have
one optional field and 10 203 have none. Not one training document has two.
The 2 000 rows added for the theorem fix are 400 CMB-STRUCT-UTL-THM among them, all
single-optional; they raised the share of "exactly one иногда per document" from 397/9 000
to 797/11 000 and sharpened a prior that was already wrong for this template. The model has
never seen the thing it is being asked to do, and the extra data made it more confident about
the nearest thing it has seen.
Practical consequence: if your task marks more than one field as необязательное, check
that all of them came out as иногда является. The compiler cannot help you here — a field
declared required instead of optional is a perfectly valid document.
Fixing it needs training rows with two or more optional fields. None exist yet, so nothing
about this is speculative-but-fixed: it is measured, named, and open.
1.4 This writes specifications; it is not a chat model
The adapter was trained on one task shape with one system prompt (§ 6). Used as a general
assistant it will emit FTS at you. None of the numbers here describe that use.
1.5 Russian only
The dataset is Russian and so is the model's competence. The FTS surface syntax used here is
the Russian one. The English surface of the language is not covered — not measured and
not expected to work.
2. What was measured
2.1 The full 1 500-document holdout
The holdout is not a random slice. split.json divides the space of structural templates
and subject areas and is written before the first document is generated. A document is
training data only if both its template and its area are on the training side; everything
else is holdout, labelled with which thing is new.
Greedy decoding, no grammar constraint, no reference sheet in the prompt,
max_new_tokens = 1200, thinking disabled. Both rows of every table below are the two
adapters on the same 1 500 revision-2 tasks.
Table with columns: passes the real compiler, new area, new template, new template and area, total| passes the real compiler | new area | new template | new template and area | total |
|---|
| this adapter (data rev 2) | 500/501 (99.8 %) | 501/501 (100 %) | 498/498 (100 %) | 1 499/1 500 (99.9 %) |
| previous adapter (data rev 1) | 495/501 (98.8 %) | 501/501 (100 %) | 496/498 (99.6 %) | 1 492/1 500 (99.5 %) |
Table with columns: matches the reference structure, new area, new template, new template and area, total| matches the reference structure | new area | new template | new template and area | total |
|---|
| this adapter | 500/501 | 501/501 | 498/498 | 1 499/1 500 (99.9 %) |
| previous adapter | 475/501 | 436/501 | 433/498 | 1 344/1 500 (89.6 %) |
Table with columns: means what the task asked, total, where it diverges| means what the task asked | total | where it diverges |
|---|
| this adapter | 1 392/1 500 (92.8 %) | OBJ-OPTIONAL 106, OBJ-NESTED 1, CMB-TWO-UTIL 1 |
| previous adapter | 1 257/1 500 (83.8 %) | CMB-UTL-THM 129, OBJ-OPTIONAL 87, CMB-TWO-UTIL 20, other 7 |
The single compiler failure for this adapter is an FTS_EXAMPLE_MISMATCH (§ 1.2). The
previous adapter's 8 failures are all PARSE_ERROR at the compile stage.
Inside the 1 499 documents that passed: 3 102 examples were executed and 3 102 passed —
the documents' own пример blocks, run by the language's interpreter — and 453 theorems
were proved, certified, and each certificate independently re-checked against its own digest,
453 of 453. The adapter wrote a theorem in exactly the 453 documents whose reference has
one: none missing, none invented.
Note what the second table shows about this revision: structure match and compiler pass are
now the same 1 499 documents. In the previous adapter they were 148 documents apart, and
that gap was the missing theorems.
2.2 The extended holdout — 450 documents that all need a calculation and a theorem
This split exists to stress exactly the combination the previous adapter could not do.
Table with columns: compiler, theorem present, means what was asked | compiler | theorem present | means what was asked |
|---|
| this adapter | 446/450 (99.1 %) | 446/450 (99.1 %) | 444/450 (98.7 %) |
| previous adapter | 420/450 (93.3 %) | 0/450 (0 %) | not applicable — no theorem in any |
All 4 of this adapter's failures are PARSE_ERROR, all 4 in one template
(CMB-UTL-THM-MULTI: two unterminated « quotes, one stray token after a name, one
unrecognised theorem line). The previous adapter failed 30 documents across six templates.
2.3 The revision-1 measurement, kept for continuity
The previous adapter's published numbers were taken on the revision-1 holdout:
1 491/1 500 (99.4 %) through the compiler — 98.8 % / 100 % / 99.4 % by stratum —
1 364/1 500 (90.9 %) structural match, and 1 257/1 500 (83.8 %) semantic fidelity
with 234 divergences and 9 documents that did not compile. Those are not deleted and not
restated as the new baseline; § 2.1 re-measures the same adapter on the same tasks as the
new one, which is the comparison that carries weight.
3. Reference points, on the same 150 documents
Four systems, one fixed 150-document slice of the holdout (50 per stratum), same prompts,
same greedy decoding, same gate.
Table with columns: system, reference sheet in prompt, passes the compiler| system | reference sheet in prompt | passes the compiler |
|---|
Qwen3-1.7B, untuned | no | 0/150 (0 %) |
Qwen3-1.7B, untuned | yes (2 235 tokens) | 15/150 (10.0 %) |
Qwen3-14B (nf4), untuned | yes (2 235 tokens) | 79/150 (52.7 %) |
Qwen3-1.7B + adapter rev 1 | no | |
Two honest notes on the last two rows. The rev-2 row is one document behind, and it is the
single FTS_EXAMPLE_MISMATCH of § 1.2, which happens to fall in this slice; on the full
1 500 the order is the other way round (1 499 vs 1 492). And the three untuned baselines were
run on the revision-1 phrasing of these tasks, of which 5 of the 150 changed in revision 2
— too few to move a 0/15/79 result, but it is a difference and it is stated. On semantic
fidelity over the same 150, adapter rev 2 scores 140/150.
The comparison the table is for: a 1.7B model that has been trained beats a 14B model that
has been shown the manual, and it does it without the manual in its context.
3.1 An oddity in the same run, reported rather than smoothed over
The same 150 outputs were also run through the GBNF recogniser for
fts-gate/grammars/fts.gbnf:
Table with columns: system, compiler, grammar accepts| system | compiler | grammar accepts |
|---|
Qwen3-1.7B untuned, no sheet | 0/150 | 0/150 |
Qwen3-1.7B untuned + sheet | 15/150 | 0/150 |
Qwen3-14B (nf4) + sheet | 79/150 | 78/150 |
Qwen3-1.7B + adapter rev 1 | 150/150 | 150/150 |
The middle row does not behave like the others: 15 documents the compiler accepted, the
grammar rejected all of them. The grammar and the compiler are not the same acceptor and were
never claimed to be nested, but a 15-to-0 split is larger than that explains. Nobody has
diagnosed it. It is printed here because deleting an inconvenient row is how a measurement
becomes folklore.
3.2 A previous 24/25 result for the 14B that did not reproduce
An earlier run of this project recorded 24/25 for a 14B model with the reference sheet. On
this holdout the same configuration scored 79/150 (52.7 %).
The team's hypothesis is that the earlier run decoded under the GBNF grammar and this one did
not. That hypothesis has never been tested. The earlier run's raw record is not in the
evaluation tree, so it cannot be re-derived, and the two measurements use different document
sets of different sizes.
The two numbers are not comparable and must not be quoted as a before/after. The 79/150 in
§ 3 is what this work measured; 24/25 is an earlier number about a different run that this
work could not reproduce, and that is the whole of what is known.
4. Choosing the base — the difference was noise
Four pilots, identical LoRA and identical hyperparameters, trained on a 6 856-row subset and
scored on a fixed 180-document dev split. This experiment predates both revisions and was not
repeated; it is what chose the base, not what evaluates the current adapter.
Table with columns: base, epochs, passes the compiler, train time, McNemar vs Qwen3-1.7B 2ep| base | epochs | passes the compiler | train time | McNemar vs Qwen3-1.7B 2ep |
|---|
Qwen/Qwen3-4B | 1 | 175/180 (97.2 %) | 2 866 s | p = 0.774 |
Qwen/Qwen3-1.7B | 2 | 174/180 (96.7 %) | 2 502 s | — (chosen) |
|
4B's advantage is one document out of 180. A paired McNemar test gives p = 0.774 —
indistinguishable from noise. Paying 2.4× the parameters and 15 % more training time for that
is not supported by the measurement, so 1.7B was chosen.
The QVikhr result deserves a caveat the headline does not give it. 92.8 % against 96.7 %
is 7 documents, and p = 0.070 does not reach the conventional 0.05 threshold. The
direction agrees with this organisation's earlier finding that Russian SFT over an unchanged
Qwen tokeniser buys nothing for structured-output tasks
(digit-router-experiments),
but on this evidence alone "QVikhr is worse" is suggestive, not established. One seed, one
run, 180 documents.
5. Training
Table with columns: revision 2 — current, revision 1 — previous | revision 2 — current | revision 1 — previous |
|---|
| base | Qwen/Qwen3-1.7B, bf16 (not quantised) | same |
| method | LoRA, r = 32, alpha = 64, dropout 0.05 | same |
| target modules | q_proj, k_proj, v_proj, o_proj, gate_proj, , |
Why max_length had to go up. The 2 000 rows that carry a utility and a theorem are
longer than the rest — median 1 821 tokens against 1 048. At the previous 1 792 the trainer
would have silently dropped 1 081 of those 2 000, and the theorem fix would have half
failed without any error message. At 2 560, 0 rows were dropped. Cost: 2.6 GiB more memory
and 28 minutes more wall time.
It still fits in 13 GiB on one GPU.
No intermediate checkpoint-*/ state is published — it lets you resume a run and reproduces
nothing that the final adapter and train_summary.json do not.
6. How to use it
The system prompt is not optional. It is the one the model was trained under, verbatim:
Ты пишешь исполняемые спецификации на языке FTS (русская поверхность). Ответ — только текст спецификации, без пояснений и без ограждений кода.
import torch
from transformers import AutoTokenizer, AutoModelForCausalLM
from peft import PeftModel
SYS = ("Ты пишешь исполняемые спецификации на языке FTS (русская поверхность). "
"Ответ — только текст спецификации, без пояснений и без ограждений кода.")
tok = AutoTokenizer.from_pretrained("digitable-lol/specgen-qwen3-1.7b")
base = AutoModelForCausalLM.from_pretrained("Qwen/Qwen3-1.7B", dtype=torch.bfloat16,
device_map={"": 0})
model = PeftModel.from_pretrained(base, "digitable-lol/specgen-qwen3-1.7b")
model = model.merge_and_unload().eval()
msgs = [{"role": "system", "content": SYS},
{"role": "user", "content": "<задание на русском>"}]
prompt = tok.apply_chat_template(msgs, tokenize=False, add_generation_prompt=True,
enable_thinking=False)
ids = tok(prompt, return_tensors="pt", add_special_tokens=False).to(model.device)
out = model.generate(**ids, max_new_tokens=1200, do_sample=False)
print(tok.decode(out[0, ids["input_ids"].shape[1]:], skip_special_tokens=True))
To load the previous adapter instead, pass subfolder="previous/data-rev1". Its
behaviour is the right-hand column of § 0, and it is kept so that anything measured against
it stays reproducible — not because it is recommended.
Every number on this page is greedy (do_sample=False) with thinking disabled.
Sampling was not measured.
6.1 GGUF, for serving on a CPU
gguf/specgen-1.7b-v2-Q5_K_M.gguf this adapter, merged into the base and quantised
gguf/specgen-1.7b-v1-Q5_K_M.gguf the previous adapter, same recipe, kept
1.2 GiB each — the same byte count, which is what two runs of one recipe over one
architecture produce.
v2 was built by merging the LoRA into Qwen/Qwen3-1.7B in fp16, converting with
convert_hf_to_gguf.py and quantising with llama-quantize, both from llama.cpp
b10295 — the build this project pins and serves with. It quantises to 5.82 bits per
weight. v1 predates this record: it carries the same 310 tensors, the same
quantization_version 2 and the same file_type 17, so it is the same quantisation of the
same architecture, but which llama.cpp build produced it was never written down. That is
a gap in the record, not a claim.
The training tasks are short (the longest is 747 prompt tokens and 1 200 of answer), so an
8 192-token window is fourfold headroom; the full 40 960 the base was trained on would cost
gigabytes of KV cache for nothing.
6.2 Constrained decoding is free here
All 12 950 documents of dataset revision 2 are inside the language of the GBNF grammar
fts-gate/grammars/fts.gbnf — 12 950 of 12 950 accepted. Decoding under that grammar
therefore costs the model nothing it was going to do anyway, and removes the failure mode
that actually occurs (PARSE_ERROR).
This is a real improvement over the previous revision, not just a restatement. The
previous adapter trained on 448 documents that carried float noise such as
7.199999999999999 and fell outside the grammar once it was narrowed on 2026-08-07; under
constrained decoding it could be pushed off a token sequence its own training had made
likely. Revision 2 rebuilt those 448, so this adapter's training data and the grammar
agree.
No number in § 2 or § 3 was produced under the grammar. Everything above is
unconstrained. Grammar-constrained decoding is an available improvement, still not a measured
one.
The grammar ships in the dataset repository as fts.gbnf.
6.3 Verify the output; that is the point
The model is one half of the design. The other half is that the output is checkable:
# per document: compile -> validate -> testUtilities -> prove -> certify
node tools/verify.mjs < generations.ndjson > verdicts.ndjson
The gate runs at roughly 4 200 documents/second in-process. A specification you have not
compiled is a guess. And — § 1.1 — a specification you have compiled is still only a valid
document, not necessarily the right one.
7. Files
adapter_config.json PEFT config (r=32, alpha=64, 7 target modules)
adapter_model.safetensors 133 MiB of LoRA delta — trained on DATA REVISION 2
tokenizer.json the base tokenizer, unmodified
tokenizer_config.json
chat_template.jinja
train_summary.json hyperparameters + final metrics for this adapter
previous/data-rev1/ the previous adapter — trained on DATA REVISION 1
previous/data-rev1/README.md what it is, why it is kept, what is wrong with it
gguf/specgen-1.7b-v2-Q5_K_M.gguf this adapter, merged and quantised
gguf/specgen-1.7b-v1-Q5_K_M.gguf the previous one, kept
eval/rev2/ everything behind § 0-§ 2
specgen-qwen3-1.7b-ml32-rev2.holdout.ndjson this adapter, 1 500 holdout
specgen-qwen3-1.7b-ml32-rev2.holdout_ext.ndjson this adapter, 450 extended
specgen-qwen3-1.7b.rev2-holdout.ndjson previous adapter, SAME 1 500
specgen-qwen3-1.7b.rev2-holdout_ext.ndjson previous adapter, SAME 450
results.json every number above, machine-readable
results_ml32_trained_on_rev1.json the control run behind § 1.3
semcheck.*.jsonl per-document meaning verdicts
eval/*.ndjson the revision-1 evaluation record, unchanged
eval/reference.md the 2 235-token sheet given to the untuned baselines
MANIFEST.json sha256 of every file in this repository
eval/ is published so the claims are checkable rather than merely stated: those NDJSON
files are the models' actual output, and re-running them through the compiler reproduces
§ 2.
8. What was not measured
- Sampling. Greedy only. No temperature sweep, no self-consistency, no pass@k.
- Grammar-constrained decoding (§ 6.2) — the dataset conforms to the grammar, but no
evaluation on this page used it.
- Documents with more than one optional field, in training. § 1.3 — none exist, which is
why that class fails. Whether adding them fixes it is unknown, because it has not been
tried.
- CPU latency and throughput of the GGUF. The file is built and served, but no timing
claim is made here; the numbers that exist were taken on a loaded machine and are not
worth quoting.
- Any non-Russian surface.
- Variance. One seed, one training run per revision. The base comparison in § 4 is one
seed per base, which is why its differences are reported as noise rather than as a ranking.
- Documents longer than the training distribution.
max_length was 2 560 tokens and
nothing longer was tried.
- Real user requests. Every task the model has ever seen was generated by
tools/task.py
from the same structure that produced the reference document. Real requests are messier,
and none were tested.
9. Origin and licensing
Both adapters: BSD-2-Clause.
Unlike the router models in this organisation, there is no unresolved copyleft question here.
The FTS language and its compiler
(@digitable-lol/fts) and the verification gate
(@digitable-lol/fts-gate) are both BSD-2-Clause, both belong to this organisation, and
the training data was generated from them by this project's own code.
The base model is Qwen/Qwen3-1.7B, Apache-2.0. The adapter files are LoRA deltas and do
not redistribute it; using them requires downloading the base under its own terms. The GGUF
files do contain the merged base weights and are therefore a redistribution of
Qwen/Qwen3-1.7B under Apache-2.0, whose terms apply to them.
10. Integrity
MANIFEST.json lists the sha256 of every published file, recorded at upload time on the
machine that produced it. This project tracks runs by weight hash rather than by tag, because
a tag was once re-created from a different build while an evaluation was in flight and only
the digest made the swap visible.
11. По-русски
Что это и какая ревизия
LoRA-адаптер (133 МиБ) поверх Qwen/Qwen3-1.7B, который пишет исполняемые спецификации FTS
по заданию на обычном русском.
В репозитории лежат два адаптера, и у каждого названа ревизия данных, на которой он
обучен. Без этой пары число ничего не значит.
Table with columns: ревизия 2 — текущая, ревизия 1 — прежняя | ревизия 2 — текущая | ревизия 1 — прежняя |
|---|
| где | корень репозитория | previous/data-rev1/ |
| обучен на | ревизии 2 датасета, 11 000 строк | ревизии 1, 9 000 строк |
| проходит компилятор (1 500) | 1 499/1 500 (99,9 %) | 1 492/1 500 (99,5 %) |
| означает то, что просили | 1 392/1 500 (92,8 %) | 1 257/1 500 (83,8 %) |
| пишет теорему, когда просят | |
Обе колонки сняты на одних и тех же 1 500 документах — holdout ревизии 2 — одним и тем
же greedy-декодированием и одним и тем же компилятором. Это существенно: у 64 из 1 500
заданий текст изменился между ревизиями (в ревизии 1 регистр формулировки выбирался
невоспроизводимо), поэтому выдачи прежнего адаптера пересняты на новых заданиях, а не
взяты из его собственной публикации.
Главная оговорка
Гейт ручается, что документ компилируется, типизируется, исполняет свои примеры и
доказывает свою теорему. Он не ручается, что документ означает то, что просили словами.
Поэтому смысл меряется отдельным инструментом: задание читается независимым читателем в ту
же модель, которую компилятор строит из документа, и они сравниваются поэлементно.
Чувствительность самой метрики измерена: 8 600 из 8 600 намеренных порч поймано (4 800
порч документа, 3 800 — задания), и шесть её заявленных слепых пятен проверены на молчание.
Честное чтение страницы: 99,9 % выдач — валидный FTS, и 92,8 % выдач означают то, что
просили.
Оба унаследованных дефекта закрыты
Теорема рядом с расчётом. Было: шаблон CMB-UTL-THM — теорема написана 0 раз из 129,
при 257 из 257 на других шаблонах с теоремами. Причина лежала в данных: ни один из 9 000
обучающих документов не содержал утилиту и теорему одновременно. Стало: 129/129, а на
всех шаблонах с теоремой — 453/453. На расширенном holdout из 450 документов, где
теорема нужна всюду: было 0/450, стало 446/450 (99,1 %).
Два расчёта вместо одного. Было: на всех 20 заданиях CMB-TWO-UTIL, где просили два
расчёта, адаптер писал один — 20 из 20. Это была не дыра, а ошибка в данных: 416 из 10 500
документов ревизии 1 отвечали на задание с двумя расчётами документом с одним. Стало:
расхождений по числу утилит 0 из 20. Проверено не на глаз, а тем же сравнением
задание-против-документа, которым дефект нашли в датасете.
Один документ CMB-TWO-UTIL всё же расходится, но по другой причине: CMB-TWO-UTIL:telecom:0
пишет пример, с ожиданием которого интерпретатор не согласен (FTS_EXAMPLE_MISMATCH на
границе правила). Это единственный документ из 1 500, который компилятор отверг.
Что стало хуже: необязательные поля, 21/108 → 2/108
Это ухудшение, и вызвано оно не починкой данных.
В шаблоне OBJ-OPTIONAL 108 документов. Каждое задание называет ровно два
необязательных поля, каждый эталон помечает ровно два (иногда является).
Table with columns: верно, документов с 0 / 1 / 2 пометками | верно | документов с 0 / 1 / 2 пометками |
|---|
| прежний адаптер | 21/108 | 47 / 40 / 21 |
| этот адаптер | 2/108 | 43 / 40 / 25 |
Обратите внимание на вторую колонку: правильное количество пометок этот адаптер ставит
даже чаще (25 против 21), а прав всё равно реже — потому что ставит их не на те поля. Он
теряет пометку на поле-дате 106 раз и приписывает лишнюю полю-признаку 23 раза.
Причина — 2 000 добавленных обучающих строк, а не исправленные данные. Промежуточный
адаптер, добавивший те же 2 000 строк к неисправленному корпусу ревизии 1, даёт
те же 2/108. Его полный отчёт лежит в
eval/rev2/semcheck.ml32-trained-on-rev1.holdout.jsonl — это проверяемо, а не на слово.
Починка данных сдвинула CMB-TWO-UTIL с 20 расхождений до 0 и оставила OBJ-OPTIONAL там
же, где он был.
Корень — в распределении обучающих данных, и он точный:
OBJ-OPTIONAL — отложенный шаблон, ни одного обучающего документа такой формы нет.
Необязательные поля встречаются в обучении только внутри CMB-STRUCT-UTL и
CMB-STRUCT-UTL-THM, и там они всегда ровно по одному на документ. Из 11 000
обучающих строк 797 имеют одно необязательное поле и 10 203 — ни одного. Ни одна не
имеет двух.
Из 2 000 строк, добавленных ради теоремы, 400 — это CMB-STRUCT-UTL-THM, все с одним
необязательным полем; они подняли долю «ровно одно иногда на документ» с 397/9 000 до
797/11 000 и заострили ожидание, которое для этого шаблона и так было неверным. Модель
никогда не видела того, о чём её просят, а лишние данные сделали её увереннее в ближайшем
из виденного.
Что это значит на практике: если ваше задание помечает больше одного поля как
необязательное, проверьте, что все они вышли как иногда является. Компилятор здесь не
поможет — документ, где поле объявлено обязательным вместо необязательного, совершенно
валиден.
Чинится это обучающими строками с двумя и более необязательными полями. Таких пока нет,
поэтому здесь нет ничего «уже почти исправленного»: измерено, названо, открыто.
Результаты на полном holdout (1 500 док., greedy, без грамматики, без справочника)
Компилятор: 1 499/1 500 (99,9 %) — новая область 500/501 (99,8 %), новый шаблон 501/501
(100 %), шаблон+область 498/498 (100 %). Прежний адаптер на тех же заданиях: 1 492/1 500
(99,5 %) — 495/501, 501/501, 496/498.
Совпадение со структурой эталона: 1 499/1 500 (99,9 %) против 1 344/1 500 (89,6 %).
Заметьте: у этой ревизии совпадение со структурой и проход компилятора — одни и те же
1 499 документов; у прежнего адаптера между ними было 148 документов разницы, и этой
разницей были пропущенные теоремы.
Внутри прошедших: исполнено 3 102 примера, сошлись все 3 102; доказано и
сертифицировано 453 теоремы (453 из 453), каждый сертификат независимо перепроверен по
своему дайджесту. Теорема написана ровно в тех 453 документах, где она есть в эталоне: ни
одной пропущенной, ни одной лишней.
Расширенный holdout (450 документов, всюду нужны и расчёт, и теорема): компилятор
446/450 (99,1 %) против 420/450 (93,3 %); смысл 444/450 (98,7 %). Все 4 неудачи —
PARSE_ERROR в одном шаблоне CMB-UTL-THM-MULTI (две незакрытые «ёлочки», лишний текст
после имени, неопознанная строка теоремы).
Числа ревизии 1 сохранены: на holdout ревизии 1 прежний адаптер давал 1 491/1 500
(99,4 %), 98,8 / 100 / 99,4 по стратам, 1 364/1 500 структурного совпадения и 1 257/1 500
(83,8 %) смысловой верности. Они не удалены и не выданы за новую точку отсчёта — точкой
отсчёта служит переснятый прогон на тех же заданиях.
Обучение
LoRA r=32 α=64, 2 эпохи, 11 000 строк ревизии 2, max_len 2 560, отброшено 0,
5 075 с, пик 12,59 ГиБ, финальная потеря 0,0126. Прежний адаптер: 9 000 строк
ревизии 1, max_len 1 792, 3 442 с, 9,96 ГиБ, потеря 0,0154.
Почему пришлось поднять max_len. Строки, где есть и расчёт, и теорема, длиннее
остальных: медиана 1 821 токен против 1 048. При прежних 1 792 трейнер молча выбросил бы
1 081 из 2 000 таких строк, и починка теоремы наполовину не состоялась бы — без единого
сообщения об ошибке. При 2 560 отброшено 0.
Грамматика
Все 12 950 документов ревизии 2 лежат в языке fts-gate/grammars/fts.gbnf — 12 950 из
12 950. Это не пересказ прежней оговорки, а исправление: прежний адаптер обучался в том
числе на 448 документах с двоичным мусором вида 7.199999999999999, которые перестали
попадать в грамматику после того, как 7 августа её сделали конечной. Ревизия 2 их
пересобрала — обучающие данные этого адаптера и грамматика согласованы. Но ни одно число
на этой странице не получено под грамматикой: всё измерено без неё.
Не измерено
Сэмплирование (только greedy), декодирование под грамматикой, латентность GGUF, любая
нерусская поверхность, дисперсия (один seed на ревизию), реальные пользовательские
формулировки, и — главное — обучающие строки с двумя необязательными полями: их нет, и
поможет ли их добавление, никто не проверял.
Лицензия
Оба адаптера — BSD-2-Clause; язык FTS и гейт принадлежат этой же организации и тоже
BSD-2-Clause. База Qwen/Qwen3-1.7B (Apache-2.0) в файлах адаптера не
перераспространяется — это только LoRA-дельта. В файлах GGUF база содержится, они
являются перераспространением Qwen/Qwen3-1.7B под Apache-2.0.