Neural Wani: Toward Accelerating the Automated Theorem Prover wani for Dependent Type Theory

Researchers Nanako Miyagawa, Hinari Daido, and Daisuke Bekki introduced Neural Wani, an integration of a lightweight LSTM-based neural model into the automated theorem prover wani for Dependent Type Theory, achieving a 1.41x speedup on the JSeM dataset compared to the standard non-neural baseline. The approach, presented at the Third Workshop on the Bridges and Gaps between Formal and Computational Linguistics (BriGap-3) in Paris, France, in July 2026, predicts applicable inference rules to guide backward proof search, with slight overhead in simpler proofs but effective acceleration in complex DTT-based proving.

Abstract 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.- Anthology ID: - 2026.brigap-1.2 - Volume: Proceedings of the Third Workshop on the Bridges and Gaps between Formal and Computational Linguistics BriGap-3 /volumes/2026.brigap-1/ - Month: - July - Year: - 2026 - Address: - Paris, France - Editors: Timothée Bernard /people/timothee-bernard/ , Emmanuele Chersoni /people/emmanuele-chersoni/ , Giulia Rambelli /people/giulia-rambelli/unverified/ - Venues: BriGap /venues/brigap/ | WS /venues/ws/ - SIG: - Publisher: - Association for Computational Linguistics - Note: - Pages: - 12–21 - Language: - URL: https://aclanthology.org/2026.brigap-1.2/ https://aclanthology.org/2026.brigap-1.2/ - DOI: - Cite ACL : - Nanako Miyagawa, Hinari Daido, and Daisuke Bekki. 2026. Neural Wani: Toward Accelerating the Automated Theorem Prover wani for Dependent Type Theory https://aclanthology.org/2026.brigap-1.2/ . In Proceedings of the Third Workshop on the Bridges and Gaps between Formal and Computational Linguistics BriGap-3 , pages 12–21, Paris, France. Association for Computational Linguistics. - Cite Informal : Neural Wani: Toward Accelerating the Automated Theorem Prover wani for Dependent Type Theory https://aclanthology.org/2026.brigap-1.2/ Miyagawa et al., BriGap 2026 - PDF: https://aclanthology.org/2026.brigap-1.2.pdf https://aclanthology.org/2026.brigap-1.2.pdf