CISPA
Browse
cispa_all_4006.pdf (639.67 kB)

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

Download (639.67 kB)
conference contribution
posted on 2024-03-05, 12:15 authored by Matthias CoslerMatthias Cosler, Hahn, Christopher, Mendoza, Daniel, Frederik SchmittFrederik Schmitt, Trippel, Caroline
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.

History

Preferred Citation

Matthias Cosler, Christopher Hahn, Daniel Mendoza, Frederik Schmitt, Caroline Trippel. nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models. In: Lecture Notes in Computer Science (LNCS, volume 13965). 2023.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

Computer Aided Verification: 35th International Conference

Legacy Posted Date

2023-08-11

Volume

Lecture Notes in Computer Science (LNCS, volume 13965)

Open Access Type

  • Gold

BibTeX

@inproceedings{cispa_all_4006, author = {Matthias Cosler AND Christopher Hahn AND Daniel Mendoza AND Frederik Schmitt AND Caroline Trippel}, title = {nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models}, booktitle = {Lecture Notes in Computer Science (LNCS, volume 13965)}, year = {2023} }

Usage metrics

    Categories

    No categories selected

    Licence

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC