specgen-qwen3-1.7b

A LoRA adapter over Qwen/Qwen3-1.7B that turns a task written in ordinary Russian into an executable FTS specification — a document that a real compiler parses, type checks, runs the examples of, and proves the theorem of.

On a 1 500-document holdout whose structural templates and subject areas were split off before any data was generated, 99.9 % of what this adapter writes passes the real compiler and 92.8 % of it means what the task asked. The untuned base model, on the same documents, scores 0.

133 MiB of adapter, plus a 1.2 GiB GGUF for CPU serving.

---

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.

	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:

1. 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.
2. 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.
3. 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.

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.

	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	446/450 (99.1 %)

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.

	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.

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 %)

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 %)

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.

	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.

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	150/150 (100 %)
Qwen3-1.7B + adapter rev 2	no	149/150 (99.3 %)

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:

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.

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)
Qwen/Qwen3-1.7B	1	173/180 (96.1 %)	1 249 s	—
Vikhrmodels/QVikhr-3-1.7B-Instruction-noreasoning	1	167/180 (92.8 %)	1 262 s	p = 0.070

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

	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, up_proj, down_proj	same
training data	fts-specgen-dataset revision 2, 11 000 rows	revision 1, 9 000 rows
rows dropped for length	0	0
epochs	2	2
lr	1e-4	1e-4
batch	2 × grad-accum 8 = effective 16	same
max length	2 560 tokens	1 792 tokens
optimiser	adamw_bnb_8bit	same
wall time	5 075 s (85 min)	3 442 s (57 min)
peak GPU memory	12.59 GiB	9.96 GiB
final train loss	0.0126	0.0154
PEFT	0.20.0	0.20.0

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)          # thinking OFF
ids = tok(prompt, return_tensors="pt", add_special_tokens=False).to(model.device)
out = model.generate(**ids, max_new_tokens=1200, do_sample=False)  # greedy
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 по заданию на обычном русском.

В репозитории лежат два адаптера, и у каждого названа ревизия данных, на которой он обучен. Без этой пары число ничего не значит.

	ревизия 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 %)
пишет теорему, когда просят	453/453 (100 %)	324/453 (71,5 %)
пишет оба расчёта, когда просят	20/20	0/20
помечает оба необязательных поля	2/108	21/108
GGUF	specgen-1.7b-v2-Q5_K_M.gguf	specgen-1.7b-v1-Q5_K_M.gguf

Обе колонки сняты на одних и тех же 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 документов. Каждое задание называет ровно два необязательных поля, каждый эталон помечает ровно два (иногда является).

	верно	документов с 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.