Catch the Platypus! Negated Conditionals as a Challenge for Machine Translation from Natural Language into Logical Formalisms Using Large Language Models

Abstract

One of the most promising applications of large language models in the legal domain concerns the automated conversion of natural language legal texts into logical formalisms, that is, automated formalization. Major challenges to these approaches emerge from the semantic fuzziness of natural language, which leads to sentences that are particularly difficult to formalize—we call these sentences “platypus sentences.” For example, the natural negation of a sentence in natural language may have different, context-dependent meanings, which often do not correspond to the logical negation of a respective formalization of said sentence. In other words, natural negations and formalized negations often diverge from one another. This problem is further intensified when natural language conditionals (i.e., negated “if... then...” sentences) are negated. The paper at hand investigates how current large language models (GPT-5, Llama, and LogicLinguist) deal with automated formalization of negated conditionals. Our results indicate that these systems still cannot reliably deliver correct formalizations, although results can be enhanced, for example, by prompt engineering.    

Received: 13 January 2026 | Revised: 26 February 2026 | Accepted: 13 March 2026

Conflicts of Interest
The authors declare that they have no conflicts of interest to this work.

Data Availability Statement
Data sharing is not applicable to this article as no new data were created or analyzed in this study.

Author Contribution Statement
Bianca Steffes: Conceptualization, Methodology, Writing – original draft, Writing – review & editing, Visualization, Software. Diogo Sasdelli: Conceptualization, Methodology, Writing – original draft, Writing – review & editing, Visualization, Validation.