State-of-the-art neural models can now reach human performance levels across
various natural language understanding tasks. However, despite this impressive
performance, models are known to learn from annotation artefacts at the expense
of the underlying task. While interpretability methods can identify influential
features for each prediction, there are no guarantees that these features are
responsible for the model decisions. Instead, we introduce a model-agnostic
logical framework to determine the specific information in an input responsible
for each model decision. This method creates interpretable Natural Language
Inference (NLI) models that maintain their predictive power. We achieve this by
generating facts that decompose complex NLI observations into individual
logical atoms. Our model makes predictions for each atom and uses logical rules
to decide the class of the observation based on the predictions for each atom.
We apply our method to the highly challenging ANLI dataset, where our framework
improves the performance of both a DeBERTa-base and BERT baseline. Our method
performs best on the most challenging examples, achieving a new
state-of-the-art for the ANLI round 3 test set. We outperform every baseline in
a reduced-data setting, and despite using no annotations for the generated
facts, our model predictions for individual facts align with human
expectations.

本研究提出了一种模型无关的逻辑框架，以确定每个输入中负责每个模型决策的特定信息并生成可解释的自然语言推理模型，其性能优于当前最先进的神经模型，适用于高度挑战性的 ANLI 数据集。

使用生成的事实作为原子的自然语言推理的逻辑推理

Logical Reasoning for Natural Language Inference Using Generated Facts  as Atoms

Cognitive theories for reasoning are about understanding how humans come to
conclusions from a set of premises. Starting from hypothetical thoughts, we are
interested which are the implications behind basic everyday language and how do
we reason with them. A widely studied topic is whether cognitive theories can
account for typical reasoning tasks and be confirmed by own empirical
experiments. This paper takes a different view and we do not propose a theory,
but instead take findings from the literature and show how these, formalized as
cognitive principles within a logical framework, can establish a quantitative
notion of reasoning, which we call plausibility. For this purpose, we employ
techniques from non-monotonic reasoning and computer science, namely, a solving
paradigm called answer set programming (ASP). Finally, we can fruitfully use
plausibility reasoning in ASP to test the effects of an existing experiment and
explain different majority responses.

本文使用非单调推理和计算机科学中的答案集编码（ASP）来形式化作为认知原则的文献发现，建立一个名为‘plausibility’的推理概念，并将其用于测试现有实验的效果并解释不同的多数响应。

个体人类推理的量化符号方法

A Quantitative Symbolic Approach to Individual Human Reasoning

We present a general logical framework for reasoning about agents' cognitive
attitudes of both epistemic type and motivational type. We show that it allows
us to express a variety of relevant concepts for qualitative decision theory
including the concepts of knowledge, belief, strong belief, conditional belief,
desire, conditional desire, strong desire and preference. We also present two
extensions of the logic, one by the notion of choice and the other by dynamic
operators for belief change and desire change, and we apply the former to the
analysis of single-stage games under incomplete information. We provide sound
and complete axiomatizations for the basic logic and for its two extensions.
The paper is under consideration in Theory and Practice of Logic Programming
(TPLP).

该论文提出了一个关于代理人认知态度和动机类型推理的普遍的逻辑框架，它使我们能够表达多种相关概念，包括知识、信念、条件信念、欲望、条件欲望、偏好等，在此基础上，提出了具有选择机制和信念改变、欲望改变的动态运算符的两个扩展，并将前者应用于不完全信息下的单阶段博弈分析。

认知态度及其变化的质性理论

A Qualitative Theory of Cognitive Attitudes and their Change

Lambeks Syntactic Calculus, commonly referred to as the Lambek calculus, was
innovative in many ways, notably as a precursor of linear logic. But it also
showed that we could treat our grammatical framework as a logic (as opposed to
a logical theory). However, though it was successful in giving at least a basic
treatment of many linguistic phenomena, it was also clear that a slightly more
expressive logical calculus was needed for many other cases. Therefore, many
extensions and variants of the Lambek calculus have been proposed, since the
eighties and up until the present day. As a result, there is now a large class
of calculi, each with its own empirical successes and theoretical results, but
also each with its own logical primitives. This raises the question: how do we
compare and evaluate these different logical formalisms? To answer this
question, I present two unifying frameworks for these extended Lambek calculi.
Both are proof net calculi with graph contraction criteria. The first calculus
is a very general system: you specify the structure of your sequents and it
gives you the connectives and contractions which correspond to it. The calculus
can be extended with structural rules, which translate directly into graph
rewrite rules. The second calculus is first-order (multiplicative
intuitionistic) linear logic, which turns out to have several other,
independently proposed extensions of the Lambek calculus as fragments. I will
illustrate the use of each calculus in building bridges between analyses
proposed in different frameworks, in highlighting differences and in helping to
identify problems.

该论文通过建立 Lambek calculus 的扩展和变体的两个统一框架，利用证明网和图重写规则建立逻辑框架，用于在不同的语言分析框架之间架起桥梁，强调区别，帮助识别问题。