Research map / Large language models / Agents, code and math
Grammar-Forced Translation of Natural Language to Temporal Logic using LLMs
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes GraFT, which lifts atomic propositions with a fine-tuned BERT tagger and translates lifted NL to LTL with a fine-tuned T5 using grammar-forced training and grammar-constrained decoding, improving end-to-end NL-to-TL accuracy.
Problem
Translating natural language into temporal logic is hard due to inaccurate atomic proposition (AP) lifting, co-references, and dependence on limited training data.
Approach
Restrict the valid output tokens at each step using known structure: AP lifting becomes masked token labeling with a handful of integer IDs (BERT), and the seq2seq translation uses TL grammar masks during both grammar-forced training (teacher-forced grammar states) and constrained decoding (T5).
Key results
- With 2000 training examples, GraFT (BERT lifting + T5) reaches 99.90% on CW, 99.80% on GLTL, and 99.10% on Navi end-to-end, versus 98.20/97.40/90.00 for the best NL2TL variant.
- With 500 training examples, GraFT achieves 97.70% (CW), 91.50% (GLTL), and 85.00% (Navi), outperforming NL2TL with GPT-4o-mini (93.00/83.80/80.40).
- In out-of-distribution settings, GraFT outperforms NL2TL on all reported train-pair splits, e.g. CW+Navi gives 58.8% vs 21.2% on CW and 73.1% vs 51.6% on Navi.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use GraFT instead of the strongest reported NL2TL baseline | End-to-end translation with 500 training examples · CW | accuracy: 93.00 -> 97.70 | Helped |
| Use GraFT instead of the strongest reported NL2TL baseline | End-to-end translation with 500 training examples · GLTL | accuracy: 83.80 -> 91.50 | Helped |
| Use GraFT instead of the strongest reported NL2TL baseline | End-to-end translation with 500 training examples · Navi | accuracy: 83.70 -> 85.00 | Helped |
| Use GraFT instead of the strongest reported NL2TL baseline | End-to-end translation with 2000 training examples · CW | accuracy: 98.20 -> 99.90 | Helped |
| Use GraFT instead of the strongest reported NL2TL baseline | End-to-end translation with 2000 training examples · GLTL | accuracy: 97.40 -> 99.80 | Helped |
| Use GraFT instead of the strongest reported NL2TL baseline | End-to-end translation with 2000 training examples · Navi | accuracy: 90.00 -> 99.10 | Helped |
| Use GraFT instead of NL2TL | Out-of-distribution translation trained on GLTL+Navi · Navi | accuracy: 55.3 -> 73.0 | Helped |
| Use GraFT instead of NL2TL | Out-of-distribution translation trained on CW+Navi · CW | accuracy: 21.2 -> 58.8 | Helped |
| Use GraFT instead of NL2TL | Out-of-distribution translation trained on CW+GLTL · Navi | accuracy: 14.6 -> 21.2 | Helped |
| Use BERT masked-language AP lifting instead of GPT-4 causal AP lifting (ablation) | AP lifting on sequences with 6–10 APs · CW | accuracy: 81.88 -> 97.10 | Helped |
| Use BERT masked-language AP lifting instead of GPT-4 causal AP lifting (ablation) | AP lifting on sequences with 11–15 APs · CW | accuracy: 70.34 -> 95.78 | Helped |
Surprising findings
- Ungrounded seq2seq with grammar forcing still gains heavily over NL2TL in some splits, while NL2TL with CW+Navi training fails to learn the CW distribution (21.2%) despite CW being in training.
Limitations
- Theoretical argument on lower cross-entropy and gradient variance is a sketch with loose assumptions (e.g., Assumption 1 correct grammar; claim of strict variance reduction only heuristic).
- Evaluated only on three benchmarks with restricted, small AP sets; AP-lifting accuracy degrades for 11-15 APs with the MLM approaches (e.g., BERT ~96% on CW).
Experimental setup
Datasets: Navigation GLTL CW
Benchmarks: CW GLTL Navi
Metrics: end-to-end translation accuracy AP lifting top-1 accuracy out-of-domain accuracy
Baselines: NL2LTL NL2Spec NL2TL Ungrounded Seq2Seq
Builds on: NL2TL NL2LTL NL2Spec T5 BERT
Closest papers by meaning
- A Benchmark for Learning to Translate a New Language from One Grammar Book (ICLR 2024 · similarity 0.85)
- Can LLMs Really Learn to Translate a Low-Resource Language from One Grammar Book? (ICLR 2025 · similarity 0.85)
- Divide and Translate: Compositional First-Order Logic Translation and Verification for Complex Logical Reasoning (ICLR 2025 · similarity 0.85)
- A Paradigm Shift in Machine Translation: Boosting Translation Performance of Large Language Models (ICLR 2024 · similarity 0.84)
- Autonomous Evaluation of LLMs for Truth Maintenance and Reasoning Tasks (ICLR 2025 · similarity 0.84)
- TimeBill: Time-Budgeted Inference for Large Language Models (AAAI 2026 · similarity 0.84)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.