nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models

• URL: http://arxiv.org/abs/2303.04864v1
• Date: Wed, 8 Mar 2023 20:08:53 GMT
• Title: nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models
• Authors: Matthias Cosler, Christopher Hahn, Daniel Mendoza, Frederik Schmitt, Caroline Trippel
• Abstract summary: We present nl2spec, a framework for applying Large Language Models (LLMs) derive formal specifications from unstructured natural language. We introduce a new methodology to detect and resolve the inherent ambiguity of system requirements in natural language. Users iteratively add, delete, and edit these sub-translations to amend erroneous formalizations, which is easier than manually redrafting the entire formalization.
• Score: 3.1143846686797314
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: A rigorous formalization of desired system requirements is indispensable when performing any verification task. This often limits the application of verification techniques, as writing formal specifications is an error-prone and time-consuming manual task. To facilitate this, we present nl2spec, a framework for applying Large Language Models (LLMs) to derive formal specifications (in temporal logics) from unstructured natural language. In particular, we introduce a new methodology to detect and resolve the inherent ambiguity of system requirements in natural language: we utilize LLMs to map subformulas of the formalization back to the corresponding natural language fragments of the input. Users iteratively add, delete, and edit these sub-translations to amend erroneous formalizations, which is easier than manually redrafting the entire formalization. The framework is agnostic to specific application domains and can be extended to similar specification languages and new neural models. We perform a user study to obtain a challenging dataset, which we use to run experiments on the quality of translations. We provide an open-source implementation, including a web-based frontend.

Related papers

• Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
  We propose a metric for evaluating the quality of specifications for verification-aware languages. We show that our metric agrees closely on a human-labeled dataset of Dafny specifications for the popular MBPP code-generation benchmark. We also outline formal verification challenges that need to be addressed to apply the technique more widely.
  arXiv  Detail & Related papers  (2024-06-14T06:52:08Z)
• How Proficient Are Large Language Models in Formal Languages? An In-Depth Insight for Knowledge Base Question Answering [52.86931192259096]
  Knowledge Base Question Answering (KBQA) aims to answer natural language questions based on facts in knowledge bases. Recent works leverage the capabilities of large language models (LLMs) for logical form generation to improve performance.
  arXiv  Detail & Related papers  (2024-01-11T09:27:50Z)
• Coupling Large Language Models with Logic Programming for Robust and General Reasoning from Text [5.532477732693001]
  We show that a large language model can serve as a highly effective few-shot semantically. It can convert natural language sentences into a logical form that serves as input for answer set programs. We demonstrate that this method achieves state-of-the-art performance on several benchmarks, including bAbI, StepGame, CLUTRR, and gSCAN.
  arXiv  Detail & Related papers  (2023-07-15T03:29:59Z)
• Soft Language Clustering for Multilingual Model Pre-training [57.18058739931463]
  We propose XLM-P, which contextually retrieves prompts as flexible guidance for encoding instances conditionally. Our XLM-P enables (1) lightweight modeling of language-invariant and language-specific knowledge across languages, and (2) easy integration with other multilingual pre-training methods.
  arXiv  Detail & Related papers  (2023-06-13T08:08:08Z)
• Natural Language Decomposition and Interpretation of Complex Utterances [47.30126929007346]
  We introduce an approach to handle complex-intent-bearing utterances from a user via a process of hierarchical natural language decomposition. Our approach uses a pre-trained language model to decompose a complex utterance into a sequence of simpler natural language steps. Experiments show that the proposed approach enables the interpretation of complex utterances with almost no complex training data.
  arXiv  Detail & Related papers  (2023-05-15T14:35:00Z)
• Controlled Text Generation with Natural Language Instructions [74.88938055638636]
  InstructCTG is a controlled text generation framework that incorporates different constraints. We first extract the underlying constraints of natural texts through a combination of off-the-shelf NLP tools and simple verbalizes. By prepending natural language descriptions of the constraints and a few demonstrations, we fine-tune a pre-trained language model to incorporate various types of constraints.
  arXiv  Detail & Related papers  (2023-04-27T15:56:34Z)
• Prompting Language Models for Linguistic Structure [73.11488464916668]
  We present a structured prompting approach for linguistic structured prediction tasks. We evaluate this approach on part-of-speech tagging, named entity recognition, and sentence chunking. We find that while PLMs contain significant prior knowledge of task labels due to task leakage into the pretraining corpus, structured prompting can also retrieve linguistic structure with arbitrary labels.
  arXiv  Detail & Related papers  (2022-11-15T01:13:39Z)
• The Whole Truth and Nothing But the Truth: Faithful and Controllable Dialogue Response Generation with Dataflow Transduction and Constrained Decoding [65.34601470417967]
  We describe a hybrid architecture for dialogue response generation that combines the strengths of neural language modeling and rule-based generation. Our experiments show that this system outperforms both rule-based and learned approaches in human evaluations of fluency, relevance, and truthfulness.
  arXiv  Detail & Related papers  (2022-09-16T09:00:49Z)
• Formal Specifications from Natural Language [3.1806743741013657]
  We study the ability of language models to translate natural language into formal specifications with complex semantics. In particular, we fine-tune off-the-shelf language models on three datasets consisting of structured English sentences.
  arXiv  Detail & Related papers  (2022-06-04T10:49:30Z)
• From English to Signal Temporal Logic [7.6398837478968025]
  We propose DeepSTL, a tool and technique for the translation of informal requirements, given as free English sentences, into Signal Temporal Logic (STL), a formal specification language for cyber-physical systems. A major challenge to devise such a translator is the lack of publicly available informal requirements and formal specifications. In the second step, we use a state-of-the-art transformer-based neural translation technique, to train an accurate attentional translator of English to STL.
  arXiv  Detail & Related papers  (2021-09-21T16:13:29Z)
• Automatic Extraction of Rules Governing Morphological Agreement [103.78033184221373]
  We develop an automated framework for extracting a first-pass grammatical specification from raw text. We focus on extracting rules describing agreement, a morphosyntactic phenomenon at the core of the grammars of many of the world's languages. We apply our framework to all languages included in the Universal Dependencies project, with promising results.
  arXiv  Detail & Related papers  (2020-10-02T18:31:45Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.