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

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. InProceedings 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)