[3G5-GS-6] Language media processing:

[3G5-GS-6-04] Toward the Development of an Automatic Theorem Prover "Neural Wani" for Dependent Type Theory

〇Nanako Miyagawa¹, Sora Tagami¹, Daisuke Bekki¹ (1. Ochanomizu University)

Keywords:Dependent Type Theory, Formal Semantics, Automatic Theorem Prover

Wani is an automated theorem prover for Dependent Type Theory (DTT), which is part of the pipeline recently proposed as a "linguistic" approach to natural language inference. However, the execution speed of wani is one of the bottlenecks in the pipeline, since proof-search in DTT is undecidable. We have therefore set up a project called Neural Wani to develop a neural network model that will increase the speed of wani by implementing a neural classifier that selects the next inference rule to apply. In this study, as part of the Neural Wani project, we implemented a neural classifier for type checking in DTT, which is a one step less difficult problem than proof search in DTT. We also compared several different strategies for embedding DTT judgments and evaluated their efficiency.