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

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.