Understanding the meaning of negated sentences remains one of the challenges for language models even in the era of large language models (LLMs). We analyze systematicity regarding LLM understanding of negation from two perspectives: behavioral systematicity and representational systematicity. For behavioral systematicity, we confirm that through demonstrations and in-context learning, LLMs can recognize negation expressions and negation scope within sentences to some extent, but they fail to achieve perfect performance. In particular, the difficulty of the negation scope recognition for models varies depending on the output format. For representational systematicity, we analyze the extent to which LLMs can construct function vectors related to the tasks necessary for understanding negation from in-context examples. The experiments suggest that while models can compose the function vectors for negation tasks, extracting the function vector for recognizing scope is more challenging.

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.

Chain-of-thought (CoT) reasoning is widely used in large language models (LLMs), but the resulting reasoning traces remain underexplored.We study these traces through the lens of discourse-level negation.Specifically, we distinguish between corrective negation, which rejects a prior reasoning step, and refining negation, which narrows or qualifies it, and introduce metrics to quantify their use in human- and LLM-authored reasoning traces.Across multiple benchmarks, we find that negation occurs much more frequently in intermediate reasoning traces than in final response texts.We then test whether negation-based features provide predictive and descriptive signal for correctness, model identity, and human-vs.-LLM authorship.For correctness prediction, negation-based features consistently outperform simple structural baselines and in several settings add complementary signal to embedding-based representations, although embeddings remain stronger overall.In a controlled comparison on correct human and LLM traces from the same dataset, our strongest results arise in human-vs.-LLM classification, where negation features outperform both structural and embedding baselines.Overall, these findings position discourse-level negation as an interpretable feature for reasoning-trace analysis, with especially strong utility for provenance-related classification and modest but consistent value for correctness prediction.

Large Language Models (LLMs) have demonstrated significant promise in formal theorem proving.In this study, we investigate the ability of LLMs to discover novel theorems and produce verified proofs. We propose a pipeline called *Conjecturing-Proving Loop* (CPL), which iteratively generates mathematical conjectures and attempts to prove them in Lean 4.A key feature of CPL is that each iteration conditions the LLM on previously generated theorems and their formal proofs, enabling parameter-free improvement of proof strategies via in-context learning.We provide both theoretical and experimental evidence that CPL increases the discovery rate of hard-to-prove theorems compared to frameworks that generate statements and proofs simultaneously.Moreover, our experiments show that reusing the LLM’s own formally verified outputs as context consistently improves subsequent proof success, demonstrating the effectiveness of self-generated in-context learning for neural theorem proving.

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.

We outline a general account of VQA using a perception-oriented formal semantic framework. We believe that it is instructive to describe VQA not only in terms of an engineering challenge, but also as a linguistically and philosophically relevant task that can help us better understand the relation between language, perception and the world. Specifically, we will argue that linguistic meaning helps us structure our takes on visual scenes, enabling us to classify situations so that we e.g. can answer questions and determine whether a sentence correctly describes a scene.

We study how to evaluate and train natural-language-to-formula generation whensurface similarity is a poor proxy for semantic correctness. Focusing ontranslation into Presburger arithmetic, we introduce a geometric distancebetween formulas by viewing each formula as a set of integer lattice pointsand assigning an exponentially decaying weight to that set. The resultingdistance yields finite comparisons even for infinite definable sets, can becomputed through quantifier elimination, polyhedral decomposition, andlattice-point generating functions, and inherits the standard metric properties. Wethen use this distance in experiments on supervised fine-tuning and GRPO fortranslating arithmetic statements into formal formulas. The results show thata distance-aware reward substantially improves parsability and adjustedsemantic quality compared with a string-similarity-only reward, while alsorevealing the remaining challenge of preserving quantifier structure.