Linguistic Theories Coincide with Misformalization in Temporal Logic

Gordon, Colin S.

Automated Software Engineering: New Ideas and Results Track (ASE NIER), November 2025

Abstract

One of the key challenges in using formal methods is producing accurate formalizations of natural language requirements, as providing incorrect formalizations may miss bugs or even codify their existence. Yet despite this critical role, recent studies have revealed that even experienced experts make mistakes when formalizing relatively simple specifications in Linear Temporal Logic (LTL). We analyze the data from one recent study from the perspective of linguistic pragmatics --- the systems by which words carry additional non-explicit meaning. We find that nearly half of novice mistakes and 80\% of expert mistakes in the dataset could be explained by misunderstanding whether and when these enrichments of what is said with additional meaning should be formalized. We conclude that further study of the relationship between natural language specifications and pragmatics has potential to reduce misformalizations.

Bibtex

@inproceedings{asenier25,
    title = {{Linguistic Theories Coincide with Misformalization in Temporal
             Logic}},
    author = {Gordon, Colin S.},
    year = {2025},
    booktitle = {Automated Software Engineering: New Ideas and Results Track
                 (ASE NIER)},
  publisher = {{IEEE}},
  abbr = {ASE NIER},
  bibtex_show = {true},
  selected={true},
  note = {Acceptance Rate 37\% (37/99). To Appear..},
  abstract = {
One of the key challenges in using formal methods is producing accurate formalizations of natural language requirements, as providing incorrect formalizations may miss bugs or even codify their existence. Yet despite this critical role, recent studies have revealed that even experienced experts make mistakes when formalizing relatively simple specifications in Linear Temporal Logic (LTL).

We analyze the data from one recent study from the perspective of linguistic pragmatics --- the systems by which words carry additional non-explicit meaning. We find that nearly half of novice mistakes and 80\% of expert mistakes in the dataset could be explained by misunderstanding whether and when these enrichments of what is said with additional meaning should be formalized. We conclude that further study of the relationship between natural language specifications and pragmatics has potential to reduce misformalizations.
  },
}