<?xml version="1.0" encoding="UTF-8"?>
<modsCollection xmlns="http://www.loc.gov/mods/v3">
<mods ID="miyagawa-etal-2026-neural">
    <titleInfo>
        <title>Neural Wani: Toward Accelerating the Automated Theorem Prover wani for Dependent Type Theory</title>
    </titleInfo>
    <name type="personal">
        <namePart type="given">Nanako</namePart>
        <namePart type="family">Miyagawa</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <name type="personal">
        <namePart type="given">Hinari</namePart>
        <namePart type="family">Daido</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <name type="personal">
        <namePart type="given">Daisuke</namePart>
        <namePart type="family">Bekki</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <originInfo>
        <dateIssued>2026-07</dateIssued>
    </originInfo>
    <typeOfResource>text</typeOfResource>
    <relatedItem type="host">
        <titleInfo>
            <title>Proceedings of the Third Workshop on the Bridges and Gaps between Formal and Computational Linguistics (BriGap-3)</title>
        </titleInfo>
        <name type="personal">
            <namePart type="given">Timothée</namePart>
            <namePart type="family">Bernard</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Emmanuele</namePart>
            <namePart type="family">Chersoni</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Giulia</namePart>
            <namePart type="family">Rambelli</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <originInfo>
            <publisher>Association for Computational Linguistics</publisher>
            <place>
                <placeTerm type="text">Paris, France</placeTerm>
            </place>
        </originInfo>
        <genre authority="marcgt">conference publication</genre>
    </relatedItem>
    <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.</abstract>
    <identifier type="citekey">miyagawa-etal-2026-neural</identifier>
    <location>
        <url>https://aclanthology.org/2026.brigap-1.2/</url>
    </location>
    <part>
        <date>2026-07</date>
        <extent unit="page">
            <start>12</start>
            <end>21</end>
        </extent>
    </part>
</mods>
</modsCollection>

%0 Conference Proceedings
%T Neural Wani: Toward Accelerating the Automated Theorem Prover wani for Dependent Type Theory
%A Miyagawa, Nanako
%A Daido, Hinari
%A Bekki, Daisuke
%Y Bernard, Timothée
%Y Chersoni, Emmanuele
%Y Rambelli, Giulia
%S Proceedings of the Third Workshop on the Bridges and Gaps between Formal and Computational Linguistics (BriGap-3)
%D 2026
%8 July
%I Association for Computational Linguistics
%C Paris, France
%F miyagawa-etal-2026-neural
%X 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.
%U https://aclanthology.org/2026.brigap-1.2/
%P 12-21

Markdown (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)

• Neural Wani: Toward Accelerating the Automated Theorem Prover wani for Dependent Type Theory (Miyagawa et al., BriGap 2026)

ACL

• Nanako Miyagawa, Hinari Daido, and Daisuke Bekki. 2026. Neural Wani: Toward Accelerating the Automated Theorem Prover wani for Dependent Type Theory. 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.