TwIL‑LM: μικρά μοντέλα τυπικής λογικής που τρέχουν τοπικά

Τι είναι σήμερα το TwIL‑LM και τι άλλαξε

Η ονομασία TwIL‑LM χρειάζεται πλέον έκδοση. Το επίσημο repository της webAI έχει στο main το TwIL‑LM2: ένα πλήρως συγχωνευμένο μοντέλο 1,7 δισ. παραμέτρων πάνω στο SmolLM2‑1.7B‑Instruct. Φορτώνεται απευθείας ως causal language model και δεν χρειάζεται ξεχωριστό LoRA adapter κατά το inference. Το αρχικό TwIL‑LM v1, που ήταν PEFT LoRA adapter μόνο για το supervised fine-tuning στάδιο, παραμένει αρχειοθετημένο στο branch και tag TwIL-LM1.

Η αλλαγή δεν είναι απλή μετονομασία. Σύμφωνα με την τρέχουσα model card, το TwIL‑LM2 προέκυψε από LoRA supervised fine-tuning, checkpoint fusion, WiSE‑FT interpolation και reinforcement learning. Τα headline metrics του v1 και του v2 προέρχονται από διαφορετικά πρωτόκολλα και δεν πρέπει να μπαίνουν στην ίδια σειρά σαν να είναι άμεσα συγκρίσιμα.

Οι εργασίες παραμένουν στενές και σαφείς: μετάφραση φυσικής γλώσσας σε first‑order logic, ταξινόμηση entailment, semantic parsing, Lean formalization και critique, procedural reasoning και rule induction. Το context window είναι 8.192 tokens και η τεκμηριωμένη γλώσσα είναι τα αγγλικά. Άρα ένα ελληνικό use case χρειάζεται δική του αξιολόγηση και δεν κληρονομεί αυτομάτως τα αγγλικά αποτελέσματα.

Γιατί το autoformalization έχει επιχειρηματική σημασία

Autoformalization είναι η μετατροπή μιας ανθρώπινης διατύπωσης σε τυπική, μηχανικά ελέγξιμη μορφή. Δεν είναι περίληψη και δεν είναι απόφαση. Μεταφέρει ένα επιχείρημα σε μεταβλητές, σχέσεις, ποσοδείκτες ή κανόνες, ώστε ένα δεύτερο σύστημα να μπορεί να ελέγξει σύνταξη, συνέπεια ή ικανοποίηση περιορισμών.

Στο e‑commerce, μια πολιτική όπως «η προσφορά ισχύει μόνο για συγκεκριμένη κατηγορία, χώρα και χρονικό διάστημα» μπορεί να γίνει υποψήφιος κανόνας. Το μοντέλο μπορεί να προτείνει τη δομή, αλλά δεν πρέπει να ενεργοποιήσει την έκπτωση. Το αποτέλεσμα χρειάζεται parser, test cases με οριακές περιπτώσεις, σύγκριση με τους εμπορικούς όρους και τελική έγκριση από owner.

Στο marketing, η ίδια αρχή μπορεί να μετατρέψει ένα brief σε ελέγξιμους περιορισμούς: ποιο κοινό είναι επιλέξιμο, ποιο claim απαιτεί εγκεκριμένη πηγή και πότε πρέπει να σταματήσει μια ροή. Αυτές είναι πιθανές εφαρμογές της αρχιτεκτονικής και όχι τεκμηριωμένες παραγωγικές χρήσεις του συγκεκριμένου μοντέλου. Η σωστή σύνδεση με αυτοματισμούς επιχειρήσεων και AI ξεκινά από περιορισμένο task, όχι από την υπόσχεση ότι ένα μοντέλο «καταλαβαίνει όλους τους κανόνες».

Η επιχειρηματική αξία βρίσκεται στο ελεγχόμενο ενδιάμεσο artifact. Μια formalization μπορεί να αποθηκευτεί, να γίνει diff, να περάσει από validator και να συνδεθεί με την απόφαση του ανθρώπου. Έτσι το workflow αποκτά traceability που λείπει από μια απλή συνομιλιακή απάντηση.

Τι δείχνουν τα benchmarks του TwIL‑LM2

Η τρέχουσα model card αναφέρει paired βελτίωση του macro gate από 0,263 στο SmolLM2 base σε 0,393 στο TwIL‑LM2. Στο αναλυτικό Track A, το strict‑7 είναι 0,2386, το semantic parsing token‑F1 0,8428, το Lean formalization token‑F1 0,6199, το entailment accuracy 0,5850 και το rule‑induction derivation score 0,5136.

Αυτά είναι αποτελέσματα του επίσημου evaluation harness της webAI, όχι ανεξάρτητη αναπαραγωγή. Η τεκμηρίωση δίνει 200 prompts ανά objective, greedy decoding, budget 2.048 νέων tokens και συνολικό μήκος 8.192 tokens. Η model card εξηγεί επίσης ότι διαφορετικά aggregates μετρούν διαφορετικές ιδιότητες: το strict‑7 δεν δίνει partial credit, ενώ το macro gate περιλαμβάνει loose matching σε ορισμένες free‑text εργασίες.

Η ακρίβεια της μορφής έχει πρακτική αξία όταν το output πρέπει να καταναλωθεί από parser ή theorem prover. Όμως ακόμη και μια υψηλή token‑F1 επίδοση δεν αποδεικνύει ότι κάθε παραγόμενη λογική πρόταση είναι σωστή. Όπως δείχνει και η σύγκριση μοντέλων υπό διαφορετικές συνθήκες, το score πρέπει πάντα να διαβάζεται μαζί με το prompt contract, το decoding και το failure mode.

Γιατί ένα καλό benchmark δεν αρκεί

Το TwIL‑LM2 βελτιώνει το δικό του base σε όλες τις έξι objective lanes του Track A, όμως δεν διατηρεί πλήρως τη γενική held‑out επίδοση. Η model card αναφέρει πτώση του macro σε δέκα datasets από 0,4456 σε 0,4333 και σε δεκατέσσερα datasets από 0,3838 σε 0,3742. Βελτιώνονται ορισμένα checkable tasks, ενώ υποχωρούν εργασίες ανοικτού, πολυβηματικού reasoning και instruction following.

Αυτό είναι αναμενόμενο trade‑off εξειδίκευσης, όχι λεπτομέρεια που πρέπει να κρυφτεί. Η ομάδα δεν επιλέγει TwIL‑LM2 επειδή «είναι καλύτερο στο reasoning». Το επιλέγει μόνο αν το target task μοιάζει με εκείνο που μετρήθηκε και αν ολόκληρη η ροή αποδίδει καλύτερα από το base ή μια απλούστερη deterministic λύση.

Τα aggregates θέλουν προσοχή. Το token‑F1, το exact match, η accuracy, η perplexity και το derivation score δεν μετρούν το ίδιο πράγμα. Η ανάμειξή τους σε έναν αριθμό βοηθά στην πλοήγηση, αλλά δεν αντικαθιστά test set με πραγματικές προτάσεις, γνωστές σωστές formalizations και κατηγορίες σφάλματος.

Η ίδια αρχή ισχύει στη βελτίωση ενός μοντέλου από άλλο μοντέλο και στη self‑distillation του reasoning: μια μέθοδος μπορεί να ανεβάσει συγκεκριμένο metric και να μεταφέρει ή να ενισχύσει άλλο failure mode. Το production gate πρέπει να μετρά το δικό σας κόστος λάθους.

Τοπική εκτέλεση, GGUF και πραγματικό hardware

Η επίσημη κάρτα διαθέτει bf16 weights 3,19 GiB και GGUF builds Q4_K_M 0,98 GiB, Q5_K_M 1,14 GiB, Q8_0 1,70 GiB και F16 3,19 GiB. Το Q4_K_M προτείνεται ως compact default και αναφέρεται ότι τρέχει σε CPU ή περίπου 2 GB VRAM. Αυτή η δήλωση αφορά δυνατότητα φόρτωσης και inference, όχι αποδεκτή latency για κάθε επιχείρηση.

Τα δημοσιευμένα Track A και Track B αποτελέσματα μετρήθηκαν στα bf16 weights μέσω vLLM, όχι στα quantized GGUF. Η ίδια η model card προειδοποιεί για μικρές αποκλίσεις, πιθανότερα στο Q4_K_M, χωρίς να τις έχει ποσοτικοποιήσει. Άρα κάθε artifact χρειάζεται ξεχωριστό evaluation με parseability, verifier pass rate, latency, peak memory και πραγματικό hardware.

Η τοπική εκτέλεση μπορεί να μειώσει την αυτόματη αποστολή inputs σε τρίτο inference endpoint και να δώσει περισσότερο έλεγχο σε logs, retention και deployment. Δεν εγγυάται ιδιωτικότητα από μόνη της. Χρειάζονται access control, ενημερώσεις, απομόνωση αρχείων, κρυπτογράφηση, monitoring και σαφές incident ownership.

Η διαφορά ανάμεσα σε «τρέχει τοπικά» και «λειτουργεί αξιόπιστα τοπικά» φαίνεται και σε άλλα local AI συστήματα. Το μικρό artifact διευκολύνει το pilot, αλλά context, token budget, parallel requests και verifier latency καθορίζουν την πραγματική χωρητικότητα. Για μεγάλα inputs, η διαχείριση context παραμένει κρίσιμη, όπως και στα LLM μεγάλου context.

Generator, parser, verifier και ανθρώπινος owner

Η ασφαλής αρχιτεκτονική δεν ζητά από το ίδιο μοντέλο να γράψει, να βαθμολογήσει και να εγκρίνει τη δική του formalization. Διαχωρίζει ρόλους και κρατά τα αποτελέσματα κάθε σταδίου. Έτσι ένα λάθος μορφής δεν συγχέεται με λογική αντίφαση και μια λογικά έγκυρη έκφραση δεν συγχέεται με σωστή επιχειρηματική πρόθεση.

Αν αποτύχει οποιοδήποτε στάδιο, το αποτέλεσμα επιστρέφει για διόρθωση και δεν περνά σε σύστημα παραγωγής. Το audit trail κρατά την αρχική πρόταση, το prompt template, το μοντέλο και revision, την προτεινόμενη formalization, τα parser errors, το verifier result και την ανθρώπινη απόφαση.

Αυτό το trace είναι εξίσου σημαντικό με την τελική ακρίβεια. Χωρίς provenance, η ομάδα δεν γνωρίζει αν μια αλλαγή προήλθε από νέο artifact, prompt, quantization, test set ή ανθρώπινη εξαίρεση. Η ανάγκη θυμίζει την ιχνηλάτηση προέλευσης σε AI skills: ό,τι αλλάζει πρέπει να μπορεί να συνδεθεί με έκδοση και υπεύθυνο.

Δεδομένα, άδεια και governance πριν από pilot

Η τρέχουσα model card περιγράφει συνθετικό corpus τυπικής λογικής και διαδικασία πολλών σταδίων πάνω στο SmolLM2. Όμως ένα επιχειρηματικό pilot δεν πρέπει να θεωρεί το training mix κατάλληλο για δικούς του όρους, προϊόντα ή γλώσσα. Χρειάζεται gold set από πραγματικές περιπτώσεις, με ανωνυμοποίηση όπου απαιτείται και ξεχωριστή ομάδα οριακών ή αντιφατικών παραδειγμάτων.

Η άδεια είναι άμεσο go/no‑go σημείο. Τα βάρη του TwIL‑LM2 διανέμονται με webAI Non‑Commercial License version 1.0, ενώ το SmolLM2 base είναι Apache 2.0. Η ανοικτή πρόσβαση στο repository δεν ισοδυναμεί με άδεια εμπορικής παραγωγής. Η επιχείρηση πρέπει να ελέγξει τη χρήση που σχεδιάζει και να λάβει κατάλληλη νομική ή αδειοδοτική επιβεβαίωση πριν συνδέσει το μοντέλο με revenue‑generating workflow.

Το NIST AI RMF οργανώνει τη διαχείριση κινδύνου σε govern, map, measure και manage. Για ένα TwIL‑LM pilot αυτό μεταφράζεται σε owner και πολιτική, χαρτογράφηση failure modes, μέτρηση πάνω σε πραγματικές περιπτώσεις και συγκεκριμένη απόφαση για το αν η χρήση προχωρά, περιορίζεται ή τερματίζεται.

Έξι βήματα για ασφαλές επιχειρηματικό pilot

Το pilot πρέπει να αποδείξει ότι το συνολικό σύστημα παράγει ελέγξιμα artifacts με αποδεκτό κόστος λάθους. Δεν χρειάζεται να ξεκινήσει από όλες τις πολιτικές της επιχείρησης. Μία στενή κατηγορία κανόνων με σαφές success criterion είναι αρκετή για να αποκαλύψει αν η τεχνολογία ταιριάζει.

Πού χρειάζεται αυστηρό «όχι» στην αυτοματοποίηση

Το TwIL‑LM2 δεν είναι γενικός assistant και δεν είναι verifier. Δεν πρέπει να χρησιμοποιείται ως αυτόνομος κριτής σε ιατρικές, νομικές, χρηματοοικονομικές ή safety‑critical αποφάσεις. Δεν πρέπει επίσης να μετατρέπει παραγόμενο FOL ή Lean σε παραγωγική ενέργεια χωρίς κατάλληλο checker και ανθρώπινο ownership.

Το «όχι» ισχύει και σε καθημερινές εμπορικές ροές όταν το λάθος είναι δύσκολο να ανακληθεί. Ένας εσφαλμένος κανόνας μπορεί να δώσει λάθος τιμή, να αποκλείσει πελάτη, να παραβιάσει όρο καμπάνιας ή να δημιουργήσει ασυνεπή εμπειρία. Το γεγονός ότι η ενέργεια δεν είναι safety‑critical δεν μηδενίζει το οικονομικό, νομικό και reputational ρίσκο.

Αποφύγετε επίσης τα ανοιχτά use cases που ζητούν μακριές αφηγηματικές αλυσίδες reasoning. Η held‑out αξιολόγηση δείχνει ότι η εξειδίκευση δεν διατηρεί κάθε γενική ικανότητα του base. Για ασαφή ή εκτός διανομής inputs, η σωστή έξοδος του workflow μπορεί να είναι «χρειάζεται άνθρωπος», όχι μια αναγκαστική formalization.

Τέλος, μην θεωρήσετε τα ελληνικά ισοδύναμα με τα τεκμηριωμένα αγγλικά tasks. Το test set πρέπει να μετρήσει ελληνική σύνταξη, αρνήσεις, νομικούς ή εμπορικούς όρους, code switching και τον τρόπο με τον οποίο ο tokenizer χειρίζεται το πραγματικό λεξιλόγιο της ομάδας.

Συμπέρασμα: μικρό μοντέλο, ελέγξιμη χρήση

Το TwIL‑LM2 είναι ενδιαφέρον επειδή συνδυάζει στενή εξειδίκευση, μικρό footprint και τοπική εκτέλεση. Στο επίσημο Track A βελτιώνει το δικό του base σε formal‑logic objectives και δείχνει ισχυρή structured‑output επίδοση. Ταυτόχρονα, η ίδια τεκμηρίωση καταγράφει held‑out regressions, μη εμπορική άδεια και ανάγκη για task‑specific verification.

Για μια ελληνική επιχείρηση, το σωστό επόμενο βήμα δεν είναι deployment. Είναι ένα περιορισμένο proof of concept με νομικά επιτρεπτή χρήση, κλειδωμένο artifact, πραγματικό gold set, parser, solver ή theorem prover, ανθρώπινη έγκριση και μετρήσιμα failure modes.

Αν το σύστημα μειώνει τον χρόνο μετατροπής κανόνων χωρίς να κρύβει τα λάθη, η μικρή κλίμακα γίνεται πλεονέκτημα. Αν ζητά από την ομάδα να εμπιστευτεί μη επαληθευμένες formalizations ή να αγνοήσει την άδεια και τις υποχωρήσεις εκτός task, το workflow έχει σχεδιαστεί λάθος.