tailot/lingologos-pure-1

An encoder-decoder transformer trained from scratch to turn a requirement sentence in one of 5 languages into a bracketed logic algebra, decoding only through a pushdown automaton over the admissible token sets and certified afterwards by Z3. No external weights are involved: the archive contains this model alone, and the training corpus is the synthetic parallel corpus of the LingoLOGOS repository.

The weights are in model.safetensors (lingologos-transformer-1), the vocabulary in tokenizer.json (lingologos-bpe-1) and the constraint in mask_spec.json. Generation without the mask is not supported: gate E5 below measures what the network does on its own.

Measured on the test split

675 rows never seen during training, greedy decoding, seed 23. Final verdict of the evaluation tool: PASS.

gate	measurement
E1 exact tree	0.9393 (634 of 675), bracket skeleton 1.0000, truncated 0
E2 legality of the generated stream	675 of 675 accepted by an independent oracle
E3 formal audit	675 trees in Z3, 675 contingent, 0 unsatisfiable, 0 valid, 0 build errors
E3 invented numbers	5 numeric payloads absent from the input sentence, rate 0.0074 over 675 checked numbers
E5 ablation at identical weights	legality with the mask 1.0000, without the mask 0.0000, streams reaching the end marker 0

Where the errors are

Exact-tree accuracy by logic family:

family	accuracy	exact / rows
conditional	0.9568	177 / 185
frequency	1.0000	35 / 35
recurrence	1.0000	255 / 255
threshold	0.8350	167 / 200

By domain:

domain	accuracy	exact / rows
agenda	1.0000	120 / 120
domotica	0.8516	132 / 155
finanze	0.9652	111 / 115
produttivita	1.0000	135 / 135
salute	0.9067	136 / 150

By language:

language	accuracy	exact / rows
de	0.9333	126 / 135
en	0.9481	128 / 135
es	0.9407	127 / 135
fr	0.9333	126 / 135
it	0.9407	127 / 135

The bracket skeleton is correct on every generated example, so the remaining errors are labelling errors inside a well formed tree: the weakest family is threshold at 0.8350 and the weakest domain is domotica at 0.8516.

How to run it

The network is consumed through src/neuro_symbolic in the source repository; the package in this repository is enough to rebuild it together with mask_spec.json and tokenizer.json.

import json
import torch
from neuro_symbolic.masking import AlgebraMask, TokenStreamMask
from neuro_symbolic.model import load_model_safetensors
from neuro_symbolic.tokenizer import Tokenizer

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>")
source = torch.tensor([tokenizer.encode(sentence, add_bos=True)])
attention = torch.ones_like(source, dtype=torch.bool)
prefix = [rule_start]
while len(prefix) < model.config.max_decoder_positions:
    logits = model(source, attention, torch.tensor([prefix]))[0, -1]
    nxt = int(token_mask.mask_logits(logits, prefix).argmax())
    prefix.append(nxt)
    if nxt == rule_end:
        break
print(tokenizer.decode_symbol_stream(prefix))

Every step goes through mask_logits, which sets each illegal continuation to minus infinity; neuro_symbolic.training.generate_batch does the same for a whole batch at once, and dataset/tools/evaluate_model.py is a complete working caller.

What is not in this model

• It reads requirements and writes algebra. The opposite direction, algebra to sentence, is specified in the repository but never trained, so do not expect verbalizations.
• It does not learn the algebra from free text: with the mask removed it produces no legal stream at all (gate E5) while staying inside the learned symbol vocabulary.
• It can pick a number that is not in the sentence. The mask allows any numeric payload, so only the Z3 plus registry audit catches it, at the rate measured above.
• It is demonstrative, not generalist: 20 epochs over 12,140 synthetic pairs, 53 operators and 5 languages built from 5 pattern families.

Provenance

item	value
format	lingologos-transformer-1
package format	lingologos-release-1
external weights	none
parameters	48253952
trainable parameters	48253952
vocabulary	3921
trained at epoch	11
best validation loss	0.004036883175915053
peak learning rate	0.0005
batch size	64
epochs	20
gradient clipping	1.0
weight decay	0.01
mixed precision	auto
training device	NVIDIA GeForce RTX 5070 Ti
algebra alphabet	53 operators, 136 leaf heads, 75 leaf values

Files in this release

file	bytes	sha256
README.md	6018	c5ed915096456fcf
config.json	542	baa159c898c3c78e
evaluation_report.json	9373	9a742c099dbffbb2
mask_spec.json	13630	8514f4d2b52ad1ae
model.safetensors	193044672	7f4be4dcd9d46d31
tokenizer.json	170831	fbe3ccf591d6655a

The first sixteen hex digits of each checksum are shown; metadata.json carries the full digests of every file in the release, including this card.

Source repository, training scripts, tests and the roadmap that produced this model: github.com/tailot/LingoLOGOS.