Elamur Research⌕
☰
home / papers / 2026 / Neural Wani: Toward Accelerating the Automated Theorem Prover wani for Dependent Type Theory

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

Paper · 2026 · Nanako Miyagawa, Hinari Daido and Daisuke Bekki

Summary

The authors address a bottleneck in a formal-semantics NLI pipeline. In this pipeline, the CCG-based parser lightblue produces Dependent Type Semantics (DTS) representations, and the prover wani then tries to establish entailment in Dependent Type Theory (DTT). Because the DTT search space is huge, wani's depth-first backward search slows down sharply whenever an unsuitable rule is chosen early on.

Neural Wani adds a lightweight LSTM that takes a proof search query (a judgment with no proof term yet) and outputs a probability distribution over applicable inference rules. Wani then expands rules in that predicted order. Earlier work predicted rules from judgments that already contained proof terms, so this setting is harder. Inputs are delexicalized into abstract structural tokens, which makes the predictor independent of the input language. Because the symbolic core is left intact, the prover remains sound.

On held-out JSeM problems, Neural Wani is on average 1.41× faster than plain wani, though simple proofs incur slight overhead. The work shows that neural guidance can make interpretable, logic-based NLI more practical.

Key points

  • Encoding of judgments:
    • Lexical constants become placeholders Word1–Word31, with an UNKNOWN token for any overflow.
    • Bound variables become Var'0–Var'6 using De Bruijn indices, which removes α-equivalence issues.
    • The "EO~delimiter" scheme marks the boundaries of each judgment component.
  • Why an LSTM rather than a Transformer: the model is called at every node of the search tree, so latency matters more than model capacity.
  • Prior result: the predecessor model, which had access to proof terms, reached micro-F1 0.982. The new task removes proof terms, which is the setting a real prover actually faces.
  • Evaluation on JSeM:
    • The average speedup is 1.41×, mainly on problems where the baseline tends to time out.
    • The predictor is most accurate on the (Membership) and (ΠE) rules.
  • Main limitation: the model was trained on type-checking data as a stand-in for real proof search trajectories, which creates a distribution shift. Ongoing projects aim to collect authentic proof search data.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Fields, topics and concepts

📚 Shelves 2The field of science this work belongs to (OpenAlex fields).Computer Science · 16,667 worksArtificial Intelligence · 16,194 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,426 works

Cite

Cite as Nanako Miyagawa, Hinari Daido and Daisuke Bekki. 2026. Neural Wani: Toward Accelerating the Automated Theorem Prover wani for Dependent Type Theory. Proceedings of the Third Workshop on the Bridges and Gaps between Formal and Computational Linguistics (BriGap-3).

The paper itself, not this page. BibTeX from the library's record of the work.

@inproceedings{miyagawa2026neural,
  title = {{Neural Wani: Toward Accelerating the Automated Theorem Prover wani for Dependent Type Theory}},
  author = {Nanako Miyagawa, Hinari Daido and Daisuke Bekki},
  booktitle = {Proceedings of the Third Workshop on the Bridges and Gaps between Formal and Computational Linguistics (BriGap-3)},
  year = {2026},
  url = {https://aclanthology.org/2026.brigap-1.2/}
}

References

18 references, 2 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Lasha Abzianidze. 2015. Towards a wide-coverage tableau method for natural logic. In New Frontiers in Artificial Intelligence: JSAI-isAI 2014 Workshops, LENLS, JURISIN, and GABA, Revised Selected Papers, volume 9067 of Lecture Notes in Artificial Intelligence, pages 66–82. Springer. find
  2. Ai Kawazoe, Ribeka Tanaka, Koji Mineshima, and Daisuke Bekki. 2015b. An inference problem set for evaluating semantic theories and semantic processing systems for Japanese. In Proceedings of the Twelfth International Workshop on Logic and Engineering of Natural Language Semantics, pages 67–73. find
  3. Daisuke Bekki. 2014. Representing anaphora with dependent types. In Logical Aspects of Computational Linguistics, volume 8535 of Lecture Notes in Computer Science, pages 14–29. Springer. find
  4. Honoka Kobayashi, Hinari Daido, and Daisuke Bekki. 2026. Neural DTS: Shizen-gengo-suiron-shisutemu-e-no sōkyoku-bunruiki-no kumikomi (trans. Neural DTS: Incorporating hyperbolic classifiers into natural language inference systems). In Proceedings of the 32nd Annual Conference of the Association for… find
  5. Daisuke Bekki and Ai Kawazoe. 2016. Implementing variable vectors in a CCG parser. In Logical Aspects of Computational Linguistics, pages 52–67. Springer. find
  6. Konstantinos Kogkalidis, Orestis Melkonian, and Jean-Philippe Bernardy. 2024. Learning structure-aware representations of dependent types. In Advances in Neural Information Processing Systems 37 (NeurIPS 2024). find
  7. Annual Conference of the Association for Natural Language Processing. find
  8. Mark Steedman. 1996. Surface Structure and Interpretation. The MIT Press. find
  9. Asa Tomita and Daisuke Bekki. 2026. LLM-o mochiita chishiki-hokan-no tōgō-ni-yoru shizen-gengo-suiron-shisutemu lightblue-no kakuchō (trans. Extending the natural language inference system lightblue by integrating LLM-based knowledge completion). In Proceedings of the 32nd Annual Conference of th… find
  10. Bill MacCartney and Christopher D. Manning. 2008. Modeling semantic containment and exclusion in natural language inference. In Proceedings of the 22nd International Conference on Computational Linguistics (Coling 2008), pages 521–528, Manchester, UK. find
  11. Coling 2008 Organizing Committee. find
  12. Per Martin-Löf. 1984. Intuitionistic type theory. Bibliopolis. find
  13. Asa Tomita, Mai Matsubara, Hinari Daido, and Daisuke Bekki. 2025. Natural language inference with CCG parser and automated theorem prover for DTS. In Proceedings of the Second Workshop on the Bridges and Gaps between Formal and Computational Linguistics (BriGap-2), pages 1–7, Düsseldorf, Germany. As… find
  14. Pascual Martínez-Gómez, Koji Mineshima, Yusuke Miyao, and Daisuke Bekki. 2017. On-demand injection of lexical knowledge for recognising textual entailment. In Proceedings of the 15th Conference of the European Chapter of the Association for Computational Linguistics: Volume 1, Long Papers, pages 710…
  15. Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Łukasz Kaiser, and Illia Polosukhin. 2017. Attention is all you need. In Advances in Neural Information Processing Systems.
  16. Mai Matsubara, Yasunori Hokazono, Mitsuhiro Tsunoda, Koutaro Tamura, Hinari Daido, Asa Tomita, and Daisuke Bekki. 2026. Gengogakuteki-paipurain-ni motozuku datōsei-no kenshō: Kin’yū-tekisuto-o taishō-to-shite (trans. Validity verification based on a linguistic pipeline: A case study of financial… find
  17. Mingzhe Wang, Yihe Tang, Jian Wang, and Jia Deng. 2017. Premise selection for theorem proving by deep graph embedding. In Advances in Neural Information Processing Systems 30 (NIPS 2017). find
  18. Koji Mineshima, Pascual Martínez-Gómez, Yusuke Miyao, and Daisuke Bekki. 2015. Higher-order logical inference with compositional semantics. In Proceedings of the 2015 Conference on Empirical Methods in Natural Language Processing, pages 2055–2061, Lisbon, Portugal. Association for Computational Ling… find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/miyagawa-2026-neural-wani-accelerating-automated-theorem/