Formal Specifications from Natural Language
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 and their corresponding formal representation: 1) First-order
logic (FOL), commonly used in software verification and theorem proving; 2)
linear-time temporal logic (LTL), which forms the basis for industrial hardware
specification languages; and 3) regular expressions (regex), frequently used in
programming and search. Our experiments show that, in these diverse domains,
the language models achieve competitive performance to the respective
state-of-the-art with the benefits of being easy to access, cheap to fine-tune,
and without a particular need for domain-specific reasoning. Additionally, we
show that the language models have a unique selling point: they benefit from
their generalization capabilities from pre-trained knowledge on natural
language, e.g., to generalize to unseen variable names.