Linguistic Theories Coincide with Misformalization in Temporal Logic

Gordon, Colin S.

Automated Software Engineering: New Ideas and Results Track (ASE NIER), November 2025, doi: 10.1109/ASE63991.2025.00329

pdf doi ieee

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},
	doi = {10.1109/ASE63991.2025.00329},
	ieee = {https://ieeexplore.ieee.org/document/11334431},
	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. },
}