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.

Linguistically-oriented formal NLI systems ensure the validity and transparency of inference. However, the combinatorial explosion of candidates, which we term the branching problem, imposes prohibitive computational overhead and a heavy cognitive burden on grammar developers. We argue that a central cause is a mismatch between the exhaustive execution paradigm and the actual workflow of grammar developers. To overcome this barrier, we propose restructuring the development workflow from exhaustive execution to interactive exploration driven by developer decisions. We realize this shift in Express, a web-based interactive development environment for lightblue, a Japanese automated inference system built upon Combinatory Categorial Grammar and Dependent Type Semantics. Express transforms branches at each stage of parsing, type checking, and proof search into explicitly selectable units, transferring control over the reasoning process to the developer. Our evaluation shows that this paradigm shift effectively reduces unnecessary computation and cognitive burden during grammar development: in a user study, we observed a 96% reduction in explored paths and improvement in the task success rate from 25% to 100%. Furthermore, a case study demonstrates a roughly 12× reduction in debugging turnaround time.