ADARULE: LLM-Driven Natural Language to LTL Conversion via Pattern-Adaptive Rule Induction

Translating natural language (NL) specifications into Linear Temporal Logic (LTL) formulas is critical for bridging human intent and formal system verification. While large language models (LLMs) have made this task more feasible, adapting NL2LTL systems to different domains remains challenging due to varied linguistic conventions. Existing methods typically rely on manually crafted translation rules or pattern-specific templates, which are costly to construct and do not generalize across domains. A core challenge is that NL–LTL datasets provide paired examples but do not explicitly indicate which linguistic elements reflect pattern-specific translation conventions. To address this problem, we propose AdaRule, a feedback-guided approach for pattern-adaptive NL2LTL translation via automatic rule induction. The key insight is that even without explicit supervision, we can leverage LLMs to perform NL2LTL translation using only basic, general-purpose rules. By comparing the predicted LTL with ground truth LTL formulas, the LLM can identify where the general rules fall short and uses this feedback to induce new translation rules that capture pattern-specific conventions. AdaRule consists of two collaborative LLM-based components: a Translator that performs the NL2LTL conversion, and a Learner that analyzes failed translations to generate corrective rules. These rules are incorporated into the Translator’s prompts to improve future predictions. Through iterative learning, AdaRule progressively adapts to pattern-specific conventions without requiring manual engineering. Experiments on four benchmark NL2LTL datasets and three different foundation LLMs show that AdaRule outperforms the other baselines by at least 21.1% on average, demonstrating the effectiveness of automatic rule induction. Our code is available at https://github.com/TrustIntelligence/ADARULE.