Investigating the reasoning abilities of transformer models, and discovering
new challenging tasks for them, has been a topic of much interest. Recent
studies have found these models to be surprisingly strong at performing
deductive reasoning over formal logical theories expressed in natural language.
A shortcoming of these studies, however, is that they do not take into account
that logical theories, when sampled uniformly at random, do not necessarily
lead to hard instances. We propose a new methodology for creating challenging
algorithmic reasoning datasets that focus on natural language satisfiability
(NLSat) problems. The key idea is to draw insights from empirical sampling of
hard propositional SAT problems and from complexity-theoretic studies of
language. This methodology allows us to distinguish easy from hard instances,
and to systematically increase the complexity of existing reasoning benchmarks
such as RuleTaker. We find that current transformers, given sufficient training
data, are surprisingly robust at solving the resulting NLSat problems of
substantially increased difficulty. They also exhibit some degree of
scale-invariance - the ability to generalize to problems of larger size and
scope. Our results, however, reveal important limitations too: a careful
sampling of training data is crucial for building models that generalize to
larger problems, and transformer models' limited scale-invariance suggests they
are far from learning robust deductive reasoning algorithms.

本研究通过提出一种新的方法构建具有挑战性的自然语言可满足性问题数据集，以研究 transformer 模型的推理能力，发现这些模型在解决困难的 NLSat 问题方面表现出非常强的能力，但仍然存在限制，包括需要选取适当的训练数据才能适用于更大的问题和限制其推理能力的问题。