一句话：提出 AdaRule，用 LLM 反馈迭代归纳模式自适应翻译规则，免手工规则实现 NL→LTL 转换，平均提升至少 21.1%。
将自然语言（NL）规约翻译为线性时序逻辑（LTL）公式是连接人类意图与形式化系统验证的关键环节。尽管大语言模型（LLM）使该任务更可行，但现有 NL2LTL 系统多依赖手工翻译规则或针对特定模式的模板，构建成本高且难以跨领域泛化；同时 NL–LTL 数据集只提供配对样例，未显式标注哪些语言元素体现了模式特有的翻译约定。为此，作者提出 AdaRule：一种反馈引导的、通过自动规则归纳实现模式自适应 NL2LTL 翻译的方法。其核心思想是先让 LLM 仅用通用基础规则进行翻译，再通过比较预测 LTL 与真实 LTL 公式，识别通用规则的不足，并据此归纳出捕捉模式特有约定的新翻译规则。AdaRule 由两个协作的 LLM 组件构成：负责转换的 Translator 与分析失败翻译以生成纠正规则的 Learner，归纳出的规则被注入 Translator 的提示中以改进后续预测。通过迭代学习，系统无需人工工程即可逐步适应模式特有约定。在四个 NL2LTL 基准数据集与三种基础 LLM 上的实验表明，AdaRule 平均至少优于其他基线 21.1%。
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.
@inproceedings{paperbot11860,
title = {ADARULE: LLM-Driven Natural Language to LTL Conversion via Pattern-Adaptive Rule Induction},
author = {Jiayi Hu and Jingling Sun and Chong Wang and Yihao Huang and Jincao Feng and Yilongfei Xu and Yong Li and Kailong Wang and Weikai Miao and Jin Song Dong and Geguang Pu},
booktitle = {ICSE},
year = {2026},
doi = {10.1145/3744916.3787821}
}