lingologos-pure-1

lingologos-pure-1 от tailot — компактный encoder-decoder transformer на 48,25 млн параметров, обученный с нуля превращать предложение-требование на одном из пяти языков (de, en, es, fr, it) в логическую алгебру в скобках. Декодирование идёт только через pushdown-автомат по допустимым наборам токенов, а готовое дерево проверяется Z3. Внешние веса не используются: корпус — синтетические параллельные пары LingoLOGOS.

⚙ Ключевые особенности

• 🧭 Пять языков и алфавит из 53 операторов, 136 leaf heads и 75 leaf values.
• 🔒 Генерация без маски не поддерживается: в ablation E5 легальность с маской — 1.0000, без маски — 0.0000.
• ✅ Exact tree — 0.9393 (634 из 675), bracket skeleton — 1.0000, truncated — 0.
• 🛡 Формальный аудит Z3: 675 деревьев, 0 unsatisfiable, 0 valid, 0 build errors; доля выдуманных чисел — 0.0074.
• 💻 48,25 млн параметров, словарь 3921, обучение — 20 эпох на 12 140 синтетических парах, RTX 5070 Ti.

💻 Пример

tokenizer = Tokenizer.load("tokenizer.json")
spec = json.load(open("mask_spec.json", encoding="utf-8"))
token_mask = TokenStreamMask(AlgebraMask.from_spec(spec["algebra"]), tokenizer)
model = load_model_safetensors("model.safetensors")
rule_start = tokenizer.token_id("<RULE_START>")
rule_end = tokenizer.token_id("<RULE_END>")
prefix = [rule_start]
# каждый шаг: logits = model(...); nxt = token_mask.mask_logits(logits, prefix).argmax()