Natural Language Reasoning using Coq: Interaction and Automation
Stergios Chatzikyriakidis
Résumé : Dans cet article, nous présentons une utilisation des assistants des preuves pour traiter l'inférence en Language Naturel (NLI). D' abord, nous proposons d'utiliser les theories des types modernes comme langue dans laquelle traduire la sémantique du langage naturel. Ensuite, nous implémentons cette sémantique dans l'assistant de preuve Coq pour raisonner sur ceux-ci. En particulier, nous évaluons notre proposition sur un sous-ensemble de la suite de tests FraCas, et nous montrons que 95.2% des exemples peuvent être correctement prédits. Nous discutons ensuite la question de l'automatisation et il est démontré que le langage de tactiques de Coq permet de construire des tactiques qui peuvent automatiser entièrement les preuves, au moins pour les cas qui nous intéressent.
Abstract : In this paper, we present the use of proof-assistant technology in order to deal with Natural Language Inference. We first propose the use of modern type theories as the language in which we translate natural language semantics to. Then, we implement these semantics in the proof-assistant Coq in order to reason about them. In particular we evaluate against a subset of the FraCas test suite and show a 95.2% accuracy and also precision levels that outperform existing approaches at least for the comparable parts. We then discuss the issue of automation, showing that Coq's tactical language allows one to build tactics that can fully automate proofs, at least for the cases we have looked at.
Mots clés : Inference en Langage Naturel, Théorie des Types, Sémantique Formelle, FraCas, Coq, Automatisation des Preuves
Keywords : Natural Language Inference, Type Theory, Formal Semantics, FraCas, Coq, Proof automation