ConformalNL2LTL: Translating Natural Language Instructions into Temporal Logic Formulas with Conformal Correctness Guarantees

1. Probleemstelling

Autonome systemen maken vaak gebruik van Lineaire Temporele Logica (LTL) om complexe missies te specificeren (bijv. surveillance, data-gathering). Het handmatig definiëren van LTL-formules vereist echter aanzienlijke domeinexpertise en is tijdrovend. Natuurlijke taal (NL) wordt daarom gezien als een aantrekkelijk alternatief voor missie-specificatie.

Hoewel er methoden bestaan om NL-instructies naar LTL te vertalen met behulp van Large Language Models (LLM's), missen deze methoden correctheidsgaranties. LLM's kunnen onzeker zijn over hun output, maar bestaande systemen behandelen hun antwoorden vaak als "ground truth". Dit kan leiden tot vertaalde LTL-formules die niet overeenkomen met de oorspronkelijke intentie, wat resulteert in robotplannen die de opdracht niet correct uitvoeren.

Het centrale probleem is het ontwerpen van een vertaalalgoritme dat:

1. NL-instructies omzet in semantisch equivalente LTL-formules.
2. Een door de gebruiker gespecificeerde succesrate garandeert (bijv. 99% kans op een correcte vertaling) voor onbekende instructies.
3. De hoeveelheid menselijke interventie minimaliseert.

2. Methodologie: ConformalNL2LTL

De auteurs stellen ConformalNL2LTL voor, een raamwerk dat Conformal Prediction (CP) combineert met LLM's om onzekerheid te kwantificeren en correctheid te garanderen.

Kernarchitectuur

Het proces wordt opgevat als een reeks interafhankelijke Vraag-Antwoord (QA) taken die iteratief een LTL-formule opbouwen.

• Iteratieve Opbouw: In elke stap $k$ wordt een prompt gesteld aan een LLM om de volgende operator (tijdelijk/logisch) of atomaire propositie (AP) te genereren, gebaseerd op de NL-taak en de tot nu toe opgebouwde formule.
• Twee LLM's: Het systeem gebruikt een primaire LLM ($\psi_p$) en een auxiliaire LLM ($\psi_{aux}$).
• Onzekerheidskwantificatie via CP: In plaats van één antwoord te accepteren, vraagt het systeem de primaire LLM $m$ keer om een antwoord. De frequentie van unieke antwoorden dient als een proxy voor vertrouwen.
• Semantische Filtering: Antwoorden die semantisch equivalent zijn (bijv. "auto" vs. "voertuig") worden samengevoegd om de frequenties te corrigeren.

Het Help-Mechanisme (Uncertainty Handling)

Het systeem gebruikt Conformal Prediction om een voorspellingsset (prediction set) te construeren die met een bepaalde betrouwbaarheid ($1-\alpha$) het juiste antwoord bevat.

1. Zelfvertrouwen: Als de voorspellingsset van de primaire LLM een enkelvoudige verzameling is (singleton), wordt het antwoord geaccepteerd.
2. Hulp van de secundaire LLM: Als de set meerdere opties bevat (hoge onzekerheid), wordt de auxiliaire LLM geraadpleegd. De voorspellingssets van beide modellen worden gekruist (intersectie).
   • Als de intersectie een singleton is, wordt dat antwoord gekozen.
   • Als de intersectie leeg is of meerdere opties bevat, wordt menselijke hulp ingeroepen om de keuze te maken.
3. Stopconditie: Als de intersectie leeg is en geen correct antwoord bevat, of als de gebruiker stopt, wordt de vertaling als mislukt beschouwd.

Theoretische Basis

De methode transformeert het probleem naar een sequentie van prompts. Door een calibratie-dataset te gebruiken, wordt een non-conformity score (NCS) berekend. Dit stelt het systeem in staat om voorspellingssets te construeren die theoretisch gegarandeerd de ground truth bevatten met een kans van minstens $1-\alpha$, onder de aanname van i.i.d. (independent and identically distributed) data.

3. Belangrijkste Bijdragen

1. Eerste CP-toepassing voor NL-naar-LTL: Het is de eerste methode die Conformal Prediction toepast op LLM's voor het vertalen van natuurlijke taal naar formele logica, met garanties voor vertalingsnauwkeurigheid.
2. Samenwerking van LLM's: Een innovatief raamwerk waarbij een primaire en een auxiliaire LLM samenwerken om menselijke interventie te minimaliseren voordat de gebruiker wordt geraadpleegd.
3. Toepasbaarheid: De methode werkt zowel voor open-source als gesloten-source LLM's (waar logit-scores niet beschikbaar zijn), door gebruik te maken van sampling-frequenties.
4. Theoretische en Empirische Garanties: Het paper levert bewijzen dat de gewenste succesrate wordt behaald en valideert dit empirisch met zeer lage rates van menselijke interventie.

4. Resultaten

De auteurs hebben experimenten uitgevoerd met GPT-4o (primair) en Deepseek v3 (auxiliair) op een dataset van 1.000 scenario's (gemengd van makkelijk tot moeilijk).

• Succesrates: Het systeem bereikte de door de gebruiker gespecificeerde succesrates (95%, 97%, 99%) zeer nauwkeurig.
  • Bij een doel van 99% succesrate was de empirische succesrate 99,24%.
• Menselijke Interventie:
  • De hulprate (percentage van de stappen waarbij hulp nodig was) was extreem laag: 0,378% bij een 99% doelsuccesrate.
  • De hulpfrequentie (percentage van de scenario's waarbij minimaal één keer hulp nodig was) was 4%.
• Vergelijking met Baselines:
  • Bestaande methoden (zoals Lang2LTL, nl2spec) en een variant van ConformalNL2LTL zonder CP (UA-NL2LTL) presteerden aanzienlijk slechter in termen van succesrate (ranging van 53% tot 88%) of vereisten geen garanties.
  • Het verwijderen van de auxiliaire LLM leidde tot een sterke toename van menselijke interventie (van 0,378% naar 7,43% bij 99% doel), wat de waarde van de tweede LLM onderstreept.
• Out-of-Distribution (OOD): Zelfs bij distributiesverschuivingen (nieuwe taken die niet in de calibratie zaten), behield het systeem een redelijke succesrate (84,5% bij 99% doel), hoewel de theoretische garanties dan niet strikt gelden.

5. Betekenis en Impact

ConformalNL2LTL is een doorbraak voor de toepassing van LLM's in veiligheidskritieke autonome systemen.

• Betrouwbaarheid: Het lost het probleem op van "hallucinaties" of onzekerheid in LLM's door wiskundige garanties te bieden voor de vertaling naar formele logica.
• Autonomie: Door de hulp van een tweede LLM te gebruiken voordat de mens wordt ingeschakeld, wordt de behoefte aan menselijke supervisie drastisch verlaagd, wat essentieel is voor schaalbare autonome robots.
• Modulariteit: Het framework kan naadloos worden geïntegreerd met bestaande LTL-planners (zoals TL-RRT*), waardoor robuuste en correcte robotplannen kunnen worden gegenereerd op basis van eenvoudige natuurlijke taalcommando's.

Kortom, dit werk maakt het mogelijk om robots te programmeren met natuurlijke taal met de zekerheid dat de vertaalde missie correct is, zonder dat er constant een mens nodig is om de output te controleren.