Dependent Type Semantics (DTS) provides a highly rigorous framework for natural language inference (NLI), yet its scalability is severely bottlenecked by the need for manually created world knowledge. To overcome this knowledge acquisition bottleneck, we present a novel neuro-symbolic NLI system that integrates Hyperbolic Entailment Cones for automated conceptual hierarchy discovery. By exploiting the geometric properties of hyperbolic space, our model efficiently learns lexical entailment relations and dynamically injects them as logical axioms during the DTS proof-search process. Evaluations on our constructed diagnostic dataset show that our hybrid approach broadens the coverage of complex lexical variations and paraphrases without manual engineering.

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.

We propose a Natural Language Inference (NLI) system based on compositional semantics. The system combines lightblue, a syntactic and semantic parser grounded in Combinatory Categorial Grammar (CCG) and Dependent Type Semantics (DTS), with wani, an automated theorem prover for Dependent Type Theory (DTT). Because each computational step reflects a theoretical assumption, system evaluation serves as a form of hypothesis verification. We evaluate the inference system using the Japanese Semantic Test Suite JSeM, and demonstrate how error analysis provides feedback to improve both the system and the underlying linguistic theory.