Neurosymbolic AI for Natural Language Inference in F rench : combining LLM s and theorem provers for semantic parsing and natural language reasoning (2025)

Abstract: In this article, we describe the first comprehensive neurosymbolic pipeline for the task of Natural Language Inference (NLI) for French, with the synergy of Large Language Models (CamemBERT) and automated theorem provers (GrailLight, LangPro). LLMs prepare the input for GrailLight by tagging each token with Part-of-Speech and grammatical information based on the Type-Logical Grammar formalism. GrailLight then produces the lambda-terms given as input to the LangPro theorem prover, a tableau-based theorem prover for natural logic originally developped for English. Currently, the proposed system works on the French version of SICK dataset. The results obtained are comparable to the ones on the English and Dutch versions of SICK with the same LangPro theorem prover, and are better than the results of recent transformers on this specific dataset.Finally, we have identified ways to further improve the results obtained, such as giving access to the theorem prover to lexical knowledge via a knowledge base for French.

## introduction in natural language processing (nlp), the classification task of predicting, for a given pair of sentences, the correct label between two (entailment, not entailment) or, better, three @xcite given ones is conventionally called natural language inference (nli) or recognising textual entailment (rte). the code for the paper's pipeline is available on github. the datasets are all available on github and on huggingface. deep learning methods have proven effective for the task, with quickly improving performance over the last years. however, they lack explainability, and they might predict a correct inference label based on heuristics that has little to do with reasoning but heavily relying on the nature of the training datasets @xcite @xcite . on the other hand, symbolic methods include using theorem provers for rule-based reasoning between the two sentences provided. in this case, the input has to be clearly structured. to get the best of both worlds, neurosymbolic ai methods can be used, where deep learning methods can be leveraged to prepare the input by converting the sentences to their logical form for the theorem prover, which is then used for reasoning on the sentences and outputs its label prediction as well as the proof with the rules it applied to reach this prediction. after having introduced the context of the task and of the methods adopted, the article follows the structure below: ## conclusion and perspectives in this paper, we have presented the first combination of transformers with automated theorem provers applied to the task of natural language inference for french. the task of nli with neurosymbolic methods can be split into two subparts: semantic parsing and natural language reasoning. the first one is necessary in order to convert the sentences to a form that can be processed by the theorem prover, that is, in the form of lambda terms or first-order logical formulae. in the case of french, to achieve this, one first needs to add partof-speech and type-logical grammar tags to the tokens of the sentences with the help of deepgrail, then feed this to the graillight logical parser. the langpro theorem prover, that we chose here to use for the natural language reasoning, accepts lambdaterms as an input. we adapted it from english to french, mainly by aligning french linguistic structures to their equivalents in english, and by mapping words that can modify meaning to their english translations. the current performance of the model is promising, surpassing the performance of recent transformer encoder models evaluated on the french sick dataset. it is on par with the results obtained by langpro on the english and dutch versions of sick, as long as more lexical knowledge is added for french as well. finally, the present work also resulted in the first (nli) datasets with sentences and their lambda-term representations available for french. for the future, we plan to adapt and evaluate alternative semantic parsers, notably by using the deepgrail parsers and by adapting spindle @xcite to generate lambda-terms for our french datasets. we also plan to extend the coverage of langpro for french, so that it can handle fracas and gqnli, as well. finally, we aim at establishing another method based on a second theorem prover, for comparison reasons.