Nanako Miyagawa
2026
Neural Wani: Toward Accelerating the Automated Theorem Prover wani for Dependent Type Theory
Nanako Miyagawa | Hinari Daido | Daisuke Bekki
Proceedings of the Third Workshop on the Bridges and Gaps between Formal and Computational Linguistics (BriGap-3)
Nanako Miyagawa | Hinari Daido | Daisuke Bekki
Proceedings of the Third Workshop on the Bridges and Gaps between Formal and Computational Linguistics (BriGap-3)
This paper proposes Neural Wani, an integration of a neural model into the automated theorem prover wani for Dependent Type Theory (DTT), aimed at accelerating proof search in natural language inference (NLI) pipelines. We implemented a lightweight LSTM-based model to predict the probability distribution of applicable inference rules and integrated it into wani’s backward inference process. Evaluation using the JSeM dataset demonstrates that Neural Wani achieves a 1.41x speedup compared to the standard non-neural baseline. Although slight overhead is observed in simpler proofs, our results indicate that neural-symbolic integration effectively guides search in complex DTT-based automated theorem proving.