Coherency through formalisations of Structured Natural Language, A case study on FRETish

• URL: http://arxiv.org/abs/2605.10462v1
• Date: Mon, 11 May 2026 12:30:53 GMT
• Title: Coherency through formalisations of Structured Natural Language, A case study on FRETish
• Abstract summary: Formalisation is the process of writing system requirements in a formal language.<n>In this paper we propose a new guideline: Coherency through Formalisations.<n>We analyze NASA's Formal Requirement Elicitation Tool FRET and propose an alternative automated translation of the Controlled Natural Language FRETish to the formal language of MTL.
• Score: 0.0
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: Formalisation is the process of writing system requirements in a formal language. These requirements mostly originate in Natural Language. In the field of Formal Methods, formalisation is often identified as one of the most delicate and complicated steps in the verification process. Not seldomly, formalisation tools and environments choose various levels of requirement descriptions: Natural Language, Technical Language, Diagram Representations and Formal Language, to mention a few. In the literature, there are various maxims and principles of good practice to guide the process of requirement formalisation. In this paper we propose a new guideline: Coherency through Formalisations. The guideline states that the different levels of formalisation mentioned above should roughly follow the same logical structure. The principle seems particularly relevant in the setting where LLMs are prompted to perform reasoning tasks that can be checked by formal tools using Structured Natural Language to act as an intermediate layer bridging both paradigms. In the light of coherency, we analyze NASA's Formal Requirement Elicitation Tool FRET and propose an alternative automated translation of the Controlled Natural Language FRETish to the formal language of MTL. We compare our translation to the original translation and prove equivalence using model checking. Some statistics are performed which seem to favor the new translation. As expected, the translation process yielded interesting reflections and revealed inconsistencies which we present and discuss.

Related papers

• Position: Natural Language Should Not Fully Replace Formal Languages [11.90605417129287]
  We argue that natural language is optimized for underspecification in open-ended contexts.<n>We show that natural language excels at low specificity tasks, while formal languages are advantageous on tasks with stricter requirements.
  arXiv  Detail & Related papers  (2026-05-10T15:01:16Z)
• Shaping Schema via Language Representation as the Next Frontier for LLM Intelligence Expanding [88.11781604392606]
  This paper defines language representation as the linguistic and symbolic constructs used to map and model the real world.<n>We argue that shaping schemas through advanced language representation is the next frontier for expanding Large Language Models.
  arXiv  Detail & Related papers  (2026-05-10T02:42:29Z)
• NILE: Formalizing Natural-Language Descriptions of Formal Languages [0.0]
  This paper explores how natural-language descriptions of formal languages can be compared to their formal representations and how semantic differences can be explained.<n>We introduce a representation language for formal languages, Nile, which is designed so that Nile expressions can mirror the syntactic structure of natural-language descriptions.
  arXiv  Detail & Related papers  (2026-02-23T11:42:56Z)
• Between Circuits and Chomsky: Pre-pretraining on Formal Languages Imparts Linguistic Biases [47.920937001420505]
  Pretraining language models on formal language can improve their acquisition of natural language.<n>We show that languages capturing hierarchical dependencies indeed enable language models to achieve lower loss on natural language.<n>We also give mechanistic evidence of transfer from formal to natural language.
  arXiv  Detail & Related papers  (2025-02-26T15:55:55Z)
• 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)
• Trustworthy Formal Natural Language Specifications [3.8073142980733]
  This paper shows it is possible to build support for specifications written in expressive subsets of natural language. We implement a means to provide specifications in a modularly formal subset of English, and have them automatically translated into formal claims. We produce proof certificates explaining how each word was interpreted and how the sentence's structure was used to compute the meaning.
  arXiv  Detail & Related papers  (2023-10-05T20:41:47Z)
• nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models [3.1143846686797314]
  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.
  arXiv  Detail & Related papers  (2023-03-08T20:08:53Z)
• Language Models as Inductive Reasoners [125.99461874008703]
  We propose a new paradigm (task) for inductive reasoning, which is to induce natural language rules from natural language facts. We create a dataset termed DEER containing 1.2k rule-fact pairs for the task, where rules and facts are written in natural language. We provide the first and comprehensive analysis of how well pretrained language models can induce natural language rules from natural language facts.
  arXiv  Detail & Related papers  (2022-12-21T11:12:14Z)
• Detecting Text Formality: A Study of Text Classification Approaches [78.11745751651708]
  This work proposes the first to our knowledge systematic study of formality detection methods based on statistical, neural-based, and Transformer-based machine learning methods. We conducted three types of experiments -- monolingual, multilingual, and cross-lingual. The study shows the overcome of Char BiLSTM model over Transformer-based ones for the monolingual and multilingual formality classification task.
  arXiv  Detail & Related papers  (2022-04-19T16:23:07Z)
• Learning Symbolic Rules for Reasoning in Quasi-Natural Language [74.96601852906328]
  We build a rule-based system that can reason with natural language input but without the manual construction of rules. We propose MetaQNL, a "Quasi-Natural" language that can express both formal logic and natural language sentences. Our approach achieves state-of-the-art accuracy on multiple reasoning benchmarks.
  arXiv  Detail & Related papers  (2021-11-23T17:49:00Z)
• 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)
• A Matter of Framing: The Impact of Linguistic Formalism on Probing Results [69.36678873492373]
  Deep pre-trained contextualized encoders like BERT (Delvin et al.) demonstrate remarkable performance on a range of downstream tasks. Recent research in probing investigates the linguistic knowledge implicitly learned by these models during pre-training. Can the choice of formalism affect probing results? We find linguistically meaningful differences in the encoding of semantic role- and proto-role information by BERT depending on the formalism.
  arXiv  Detail & Related papers  (2020-04-30T17:45:16Z)

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.