⚡ electrical engineering

ReasonSTL: Bridging Natural Language and Signal Temporal Logic via Tool-Augmented Process-Rewarded Learning

Het artikel introduceert \textsc{ReasonSTL}, een framework met hulpmiddelen dat lokale open-source taalmodellen aanpast via leerprocessen met beloning om natuurlijke taalvereisten nauwkeurig en privé te vertalen naar Signal Temporal Logic (STL)-formules, en biedt zo een kosteneffectief alternatief voor handmatige specificatie en commerciële API's.

Oorspronkelijke auteurs: Bowen Ye, Zhijian Li, Junyue Huang, Junkai Ma, Xiang Yin

Gepubliceerd 2026-05-12

📖 4 min leestijd☕ Koffiepauze-leesvoer

CC BY 4.0

Oorspronkelijke auteurs: Bowen Ye, Zhijian Li, Junyue Huang, Junkai Ma, Xiang Yin

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je een ingenieur bent die een zelfrijdende auto of een robotarm ontwerpt. Je hebt een briljant idee voor hoe deze zich moet gedragen, maar je kunt het alleen beschrijven in gewoon Engels, zoals: "Als de auto te dicht bij de muur komt, moet hij binnen twee seconden stoppen."

Het probleem is dat het "brein" van de computer geen Engels spreekt. Het spreekt een strenge, wiskundige taal genaamd Signal Temporal Logic (STL). Deze taal is als een superprecies recept dat de machine exact vertelt wat het moet doen, tot op de milliseconde en de millimeter.

Het Probleem:
Tot nu toe was het omzetten van je Engelse zin in dit strenge wiskundige recept een nachtmerrie.

Handmatige Vertaling: Je zou een menselijke expert nodig hebben om het te vertalen. Dit is traag, duur en moeilijk schaalbaar.
AI Vragen (De "Black Box"): Je zou een krachtige, commerciële AI (zoals een enorme cloudgebaseerde chatbot) kunnen vragen dit te doen. Maar dit is riskant. Je zou per ongeluk de geheime veiligheidsregels van je bedrijf naar een server van een derde partij kunnen sturen. Bovendien kost het elke keer veel geld als je een vraag stelt.
Oude AI-pogingen: Eerdere lokale AI-modellen waren als studenten die het alfabet uit hun hoofd hadden geleerd, maar geen wiskunde konden doen. Ze zouden het recept raden, maar als ze een getal verkeerd hadden (bijvoorbeeld "2 seconden" zeggen in plaats van "2,5 seconden"), zou het hele project mislukken.

De Oplossing: REASONSTL
De auteurs hebben een nieuw systeem gecreëerd genaamd REASONSTL. Denk hierbij aan het inhuren van een lokale, privacygerichte leerling met een zeer specifieke werkwijze. In plaats van alleen het antwoord te raden, volgt deze leerling een strikt drie-stappenproces:

De Vertaler (Redenering): De leerling leest je Engelse zin en breekt deze op. "Oké, 'te dichtbij' betekent afstand. 'Twee seconden' moet worden omgezet naar milliseconden."
De Rekenaar (Gereedschapsgebruik): In plaats van de wiskunde te raden, pakt de leerling een rekenmachine (een "gereedschap") erbij. Het heeft specifieke gereedschappen voor het omzetten van eenheden (voet naar meter), het berekenen van tijd en het doen van wiskunde. Het moet deze gereedschappen gebruiken om de getallen goed te krijgen.
De Architect (Constructie): Zodra de getallen zijn geverifieerd, bouwt de leerling het uiteindelijke wiskundige recept (het STL-formule) volgens een strikt blauwdruk (een JSON-boomstructuur) zodat er geen haakjes ontbreken of verwarrende symbolen zijn.

Hoe Ze de Leerling Opleidden
Ze vertelden de leerling niet alleen aan het einde "Goed gedaan" of "Slecht gedaan". Ze gebruikten een speciale trainingsmethode genaamd Process-Rewarded Learning.

Stel je een leraar voor die toekijkt hoe de leerling werkt. Als de leerling de rekenmachine correct gebruikt maar vervolgens het huis ondersteboven bouwt, zegt de leraar: "Goede wiskunde, slecht bouwen."
Als de leerling probeert de wiskunde te raden zonder de rekenmachine te gebruiken, stopt de leraar hen onmiddellijk.
Dit zorgt ervoor dat de leerling leert stap voor stap te denken en de juiste gereedschappen te gebruiken, in plaats van alleen antwoorden uit het hoofd te leren.

De Nieuwe Test: STL-BENCH
Om te zien of deze leerling eigenlijk goed was, bouwde het team een nieuwe, strengere test genaamd STL-BENCH.

Het is als een eindexamen dat realistische scenario's bevat (zoals lucht- en ruimtevaart of robotica), niet alleen verzonnen zinnen.
Het is tweetalig (Engels en Chinees).
Het test specifiek of de leerling de "saai maar kritieke" zaken aankan: eenheden omzetten, wiskunde doen en complexe tijdslimieten begrijpen.

De Resultaten
Het team testte hun model met 4 miljard parameters (een "klein" maar slim lokaal model) tegen enorme commerciële AI-modellen en andere methoden.

Privacy & Kosten: Omdat het lokaal draait op hun eigen computers, is het gratis om herhaaldelijk uit te voeren en blijven alle gegevens privé.
Prestaties: Verrassend presteerde deze lokale leerling beter dan de enorme commerciële "black box" AI-modellen qua nauwkeurigheid. Het was beter in het goed krijgen van de wiskunde en het bouwen van de juiste structuur.
Menselijke Controle: Toen mensen de resultaten bekeken, was het lokale model net zo goed als de dure commerciële modellen.

In het Kort
REASONSTL is een nieuwe manier om lokale AI-modellen te leren menselijke veiligheidsregels om te zetten in strenge computercodes. Door de AI te dwingen "haar werk te tonen" met behulp van rekenmachines en gereedschappen, en door het te trainen om op elke stap voorzichtig te zijn, hebben ze een systeem gecreëerd dat privé, goedkoop en verrassend nauwkeurig is, waardoor het een veilig alternatief is voor het sturen van gevoelige data naar grote cloudbedrijven.

Technische Samenvatting: REASONSTL

Probleemstelling

Signal Temporal Logic (STL) is een formele taal die essentieel is voor het specificeren van ruimtelijk-temporele eisen aan real-waardige signalen in cyber-fysieke systemen (CPS) en autonome systemen. Hoewel STL rigoureuze verificatie en synthese mogelijk maakt, formuleren praktici eisen doorgaans in natuurlijke taal (NL). Het vertalen van deze NL-beschrijvingen naar uitvoerbare STL-formules vormt een kritieke knelpunt.

Bestaande aanpakken ondervinden aanzienlijke beperkingen:

Handmatige Specificatie: Vereist expertkennis, is arbeidsintensief en schaalt niet.
Commerciële LLM-API's: Hoewel ze bekwaam zijn, brengen ze hoge tokenkosten met zich mee en roepen ze privacyzorgen op door het doorsturen van gevoelige systeemvereisten naar derden.
Vorige Geautomatiseerde Methoden:
- DeepSTL vertrouwt op neurale machinevertaling die vanaf nul wordt getraind, wat generalisatie beperkt.
- KGST gebruikt een hybride pijplijn met proprietaire API's, wat privacy- en kostenproblemen met zich meebrengt.
- RESTL werkt lokaal maar genereert formules direct zonder tussenliggende redenering, wat de interpreteerbaarheid en correctheid in gevaar brengt.
Technische Uitdagingen: NL-naar-STL-vertaling vereist niet alleen syntactische geldigheid, maar ook semantische gronding, rekenbewust redeneren (bijv. eenheidsconversie, rekenkundige bewerkingen) en een nauwkeurige behandeling van tijdsintervallen en domeinspecifieke signalen. Kleine fouten in drempelwaarden of operatoren kunnen leiden tot incorrecte semantiek.

Methodologie: REASONSTL

De auteurs stellen REASONSTL voor, een lokaal, tool-verrijkt framework dat is ontworpen voor rekenbewuste NL-naar-STL-generatie. De kernfilosofie is om het vertaalproces te ontleden in expliciete redenering, deterministische tooloproepen en gestructureerde formuleconstructie, in plaats van te vertrouwen op een enkele stap sequentiële voorspelling.

1. Tool-Verrijkte Generatie

In plaats van ruwe tekst te genereren, genereert het model een gestructureerde uitrol bestaande uit redeneringssegmenten, tooloproepen en tool-uitvoer, die culmineren in een gestructureerde STL-JSON-boom.

Toolset: Het framework maakt gebruik van een compacte, getypeerde set deterministische tools:
- parse_duration: Normaliseert tijdsuitdrukkingen (bijv. "30 minuten" $\to$ 1800).
- convert_unit: Converteert fysieke eenheden (bijv. ft $\to$ m).
- eval_math_expr: Evalueert rekenkundige expressies voor drempelwaarden.
- calc_time_diff: Berekent tijdsverschillen uit tijdstippen.
Ontkoppeling: Dit ontwerp scheidt linguïstische interpretatie en structurele redenering van exacte numerieke berekening, waardoor het proces controleerbaar en verifieerbaar wordt.

2. Uitkomst-Gebonden Proces-Gerelateerde Optimalisatie

REASONSTL introduceert een nieuwe trainingsstrategie die zowel tussenliggende tool-gebruikstrajecten als de uiteindelijke formuleconstructie superviseert.

Procesbeloningen: Tussenliggende fasen (tooloproepen, redenering) krijgen beloningen toegekend op basis van lokale correctheid (geldigheid van argumenten, uitvoerbaarheid, consistentie).
Uitkomst-Begrenzing: Cruciaal is dat tussenliggende beloningen worden begrensd door de correctheid van de uiteindelijke STL-formule. Als de uiteindelijke formule onjuist is, wordt de maximaal haalbare beloning voor tussenliggende stappen verlaagd. Dit voorkomt dat het model "plausibele maar semantisch ongeldige" redeneersporen versterkt die leiden tot verkeerde eindresultaten.
Prefix Maskering: Als een tussenliggende stap faalt, worden daaropvolgende afhankelijke fasen gemaskeerd voor achterwaartse updates, zodat het model leert om fouten vroeg te stoppen of te corrigeren.
Optimalisatie: Het framework gebruikt een groepsrelatieve beleidsdoelstelling (vergelijkbaar met PPO maar zonder likelihood-ratio clipping) om het model te optimaliseren op basis van deze begrenste beloningen.

3. STL-BENCH: Een Nieuwe Benchmark

Om rekenbewuste NL-naar-STL-generatie te evalueren, stellen de auteurs STL-BENCH voor, een tweetalige (Engels/Chinees) benchmark die is gebaseerd op real-world CPS-signalen.

Kenmerken: Het dekt 6 engineeringdomeinen, 33 scenario's en 41 domein-gegronde signaalvariabelen.
Complexiteit: 73% van de steekproeven vereist tussenliggende berekening (toolgebruik). Het bevat expliciete annotaties voor tool-gebruikstrajecten, temporele normalisatie en eenheidsconversie.
Structuur: STL-formules worden weergegeven als JSON-bomen om schema-validatie en recursieve structurele matching mogelijk te maken, verder dan eenvoudige stringmatching.
Validatie: De dataset is opgebouwd via template-geankerde generatie, regelgebaseerde validatie en gestratificeerde menselijke audit om labels van hoge kwaliteit te waarborgen.

Belangrijkste Bijdragen

Lokaal Tool-Verrijkt Framework: REASONSTL is een lokaal, open-source framework dat NL naar STL converteert via meerstapsredenering en deterministische tooloproepen, met expliciete behandeling van temporele normalisatie, eenheidsconversie en rekenkundige evaluatie.
Uitkomst-Gebonden Proces Supervisie: Een trainingsstrategie die gezamenlijk tussenliggende tool-gebruikstrajecten en uiteindelijke formuleconstructie superviseert, waardoor het risico op het versterken van ongeldige redeneerpaden wordt verminderd door tussenliggende beloningen te begrenzen met de uiteindelijke correctheid.
Rekenbewuste Benchmark (STL-BENCH): Een tweetalige benchmark met domein-gegronde signalen, fysieke eenheden, rekenkundige beperkingen en expliciete tool-gebruikannotaties, die een rigoureuze evaluatie van rekenbewuste generatie mogelijk maakt.

Experimentele Resultaten

Experimenten zijn uitgevoerd op zowel de gevestigde DeepSTL-benchmark als de nieuwe STL-BENCH.

Prestaties op DeepSTL: Een model met 4B parameters (Qwen3-4B) getraind met REASONSTL-DIRECT (een variant voor directe generatie) behaalde 81,43% Formule-nauwkeurigheid en 82,57% Formaatnauwkeurigheid. Dit presteerde significant beter dan de sterkste black-box API-baseline (Claude-Opus-4.7) met meer dan 15 procentpunten en verbeterde de vorige state-of-the-art (RESTL) met ongeveer 21 punten.
Prestaties op STL-BENCH:
- Het volledige REASONSTL-model (met redenering en tools) behaalde 51,0% Formule-nauwkeurigheid in het Engels en 47,0% in het Chinees, en presteerde beter dan zowel het basismodel als zorgvuldig geprompte API-baselines (bijv. GPT-5.4, Kimi-K2.6).
- Menselijke Verificatie: Op een subset van 100 steekproeven per taal, kwam REASONSTL overeen met of overtrof de prestaties van proprietaire modellen, met een nauwkeurigheid van 53% in het Engels en 51% in het Chinees.
- Generalisatie: Op een handmatig geschreven, template-vrije testset behaalde REASONSTL de hoogste Formule-nauwkeurigheid (54%), presteerde iets beter dan sterke API-baselines en behield tegelijkertijd een hogere inferentie-doorvoer dan sommige commerciële modellen.
Ablatiestudies: Resultaten bevestigden dat hoewel Supervised Fine-Tuning (SFT) helpt bij formatinitialisatie, Reinforcement Learning (RL) met procesbeloningen en tool-verrijkte redenering de primaire drijvende kracht is voor prestatiewinst.

Betekenis en Beweringen

Het artikel beweert dat REASONSTL een transparant, kostenefficiënt en privacybehoudend alternatief biedt voor het opstellen van formele specificaties. Door de volledige pijplijn lokaal en open-source te houden, worden de privacy- en kostenbarrières die gepaard gaan met commerciële LLM-API's aangepakt.

De auteurs benadrukken dat het vermogen van het framework om de taak te ontleden in deterministische berekeningen en gestructureerde redenering het generatieproces controleerbaar en vatbaar voor validatie maakt, een cruciaal kenmerk voor veiligheidskritieke CPS-toepassingen. Hoewel het systeem state-of-the-art prestaties behaalt, merken de auteurs nederig op dat het momenteel het beste geschikt is als mens-in-de-lus opstelassistent in plaats van een volledig autonoom vervanging voor expertspecificatieontwerp, vooral in veiligheidskritieke contexten waar resterende semantische fouten door domeinexperts moeten worden gecontroleerd.