<?xml version="1.0" encoding="UTF-8"?>
<modsCollection xmlns="http://www.loc.gov/mods/v3">
<mods ID="saeki-bekki-2026-proof">
    <titleInfo>
        <title>Where Does Proof Search Spend Its Effort? A Visualization and Profiling Tool for Formal NLI</title>
    </titleInfo>
    <name type="personal">
        <namePart type="given">Koharu</namePart>
        <namePart type="family">Saeki</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-08</dateIssued>
    </originInfo>
    <typeOfResource>text</typeOfResource>
    <relatedItem type="host">
        <titleInfo>
            <title>Proceedings of the 6th Workshop on Natural Language Meets Logic and Machine Learning (NALOMA)</title>
        </titleInfo>
        <name type="personal">
            <namePart type="given">Hitomi</namePart>
            <namePart type="family">Yanaka</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Lasha</namePart>
            <namePart type="family">Abzianidze</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <originInfo>
            <publisher>Association for Computational Linguistics</publisher>
            <place>
                <placeTerm type="text">Prague, Czechia</placeTerm>
            </place>
        </originInfo>
        <genre authority="marcgt">conference publication</genre>
        <identifier type="isbn">979-8-89176-389-0</identifier>
    </relatedItem>
    <abstract>Recent work has substantially accelerated proof search in interactive theorem provers by integrating large language models, for both Lean and Coq.The natural language inference (NLI) counterpart lacks an analogous infrastructure: the behavior of dedicated DTT-based provers such as wani, inside the Japanese NLI system lightblue, is observable today only through verbose textual logs. This opacity blocks ML-acceleration efforts such as Neural Wani that need to know where the search spends its time and why it fails.We present a profiling and visualization tool for wani, implemented as a web-based component of the lightblue development environment, that exposes the proof search through a four-panel dashboard, Search Tree, Flame Graph, Rule Statistics, and Failure Analysis, each making one aspect of prover behavior directly inspectable.The tool provides the observability that ML-acceleration research in NLI currently needs but cannot easily obtain.It is released as open source software and provided as a Docker image.</abstract>
    <identifier type="citekey">saeki-bekki-2026-proof</identifier>
    <location>
        <url>https://aclanthology.org/2026.naloma-1.7/</url>
    </location>
    <part>
        <date>2026-08</date>
        <extent unit="page">
            <start>50</start>
            <end>59</end>
        </extent>
    </part>
</mods>
</modsCollection>

%0 Conference Proceedings
%T Where Does Proof Search Spend Its Effort? A Visualization and Profiling Tool for Formal NLI
%A Saeki, Koharu
%A Bekki, Daisuke
%Y Yanaka, Hitomi
%Y Abzianidze, Lasha
%S Proceedings of the 6th Workshop on Natural Language Meets Logic and Machine Learning (NALOMA)
%D 2026
%8 August
%I Association for Computational Linguistics
%C Prague, Czechia
%@ 979-8-89176-389-0
%F saeki-bekki-2026-proof
%X Recent work has substantially accelerated proof search in interactive theorem provers by integrating large language models, for both Lean and Coq.The natural language inference (NLI) counterpart lacks an analogous infrastructure: the behavior of dedicated DTT-based provers such as wani, inside the Japanese NLI system lightblue, is observable today only through verbose textual logs. This opacity blocks ML-acceleration efforts such as Neural Wani that need to know where the search spends its time and why it fails.We present a profiling and visualization tool for wani, implemented as a web-based component of the lightblue development environment, that exposes the proof search through a four-panel dashboard, Search Tree, Flame Graph, Rule Statistics, and Failure Analysis, each making one aspect of prover behavior directly inspectable.The tool provides the observability that ML-acceleration research in NLI currently needs but cannot easily obtain.It is released as open source software and provided as a Docker image.
%U https://aclanthology.org/2026.naloma-1.7/
%P 50-59

Markdown (Informal)

[Where Does Proof Search Spend Its Effort? A Visualization and Profiling Tool for Formal NLI](https://aclanthology.org/2026.naloma-1.7/) (Saeki & Bekki, NALOMA 2026)

• Where Does Proof Search Spend Its Effort? A Visualization and Profiling Tool for Formal NLI (Saeki & Bekki, NALOMA 2026)

ACL

• Koharu Saeki and Daisuke Bekki. 2026. Where Does Proof Search Spend Its Effort? A Visualization and Profiling Tool for Formal NLI. In Proceedings of the 6th Workshop on Natural Language Meets Logic and Machine Learning (NALOMA), pages 50–59, Prague, Czechia. Association for Computational Linguistics.