@inproceedings{saeki-bekki-2026-proof,
    title = "Where Does Proof Search Spend Its Effort? A Visualization and Profiling Tool for Formal {NLI}",
    author = "Saeki, Koharu  and
      Bekki, Daisuke",
    editor = "Yanaka, Hitomi  and
      Abzianidze, Lasha",
    booktitle = "Proceedings of the 6th Workshop on Natural Language Meets Logic and Machine Learning ({NALOMA})",
    month = aug,
    year = "2026",
    address = "Prague, Czechia",
    publisher = "Association for Computational Linguistics",
    url = "https://preview.aclanthology.org/ingest-naloma/2026.naloma-1.7/",
    pages = "50--59",
    ISBN = "979-8-89176-389-0",
    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."
}