Programming with Generative AI (GenAI) models is a type of Neurosymbolic
programming and has seen tremendous adoption across many domains. However,
leveraging GenAI models in code today can be complex, counter-intuitive and
often require specialized frameworks, leading to increased complexity. This is
because it is currently unclear as to the right abstractions through which we
should marry GenAI models with the nature of traditional programming code
constructs. In this paper, we introduce a set of novel abstractions to help
bridge the gap between Neuro- and symbolic programming. We introduce Meaning, a
new specialized type that represents the underlying semantic value of
traditional types (e.g., string). We make the case that GenAI models, LLMs in
particular, should be reasoned as a meaning-type wrapped code construct at the
language level. We formulate the problem of translation between meaning and
traditional types and propose Automatic Meaning-Type Transformation (A-MTT), a
runtime feature that abstracts this translation away from the developers by
automatically converting between M eaning and types at the interface of LLM
invocation. Leveraging this new set of code constructs and OTT, we demonstrate
example implementation of neurosymbolic programs that seamlessly utilizes LLMs
to solve problems in place of potentially complex traditional programming
logic.

该论文介绍了一组新的抽象概念，用于将神经符号编程与生成式 AI 模型相结合，并提出了一个用于自动转换意义和传统类型的运行时特性。通过利用这一新的代码构造和自动转换特性，我们展示了神经符号程序的示例实现，这些程序灵活地利用了生成式 AI 模型来代替传统的复杂编程逻辑。

LLMs 是有意义类型的代码结构

LLMs are Meaning-Typed Code Constructs

Logical reasoning, i.e., deductively inferring the truth value of a
conclusion from a set of premises, is an important task for artificial
intelligence with wide potential impacts on science, mathematics, and society.
While many prompting-based strategies have been proposed to enable Large
Language Models (LLMs) to do such reasoning more effectively, they still appear
unsatisfactory, often failing in subtle and unpredictable ways. In this work,
we investigate the validity of instead reformulating such tasks as modular
neurosymbolic programming, which we call LINC: Logical Inference via
Neurosymbolic Computation. In LINC, the LLM acts as a semantic parser,
translating premises and conclusions from natural language to expressions in
first-order logic. These expressions are then offloaded to an external theorem
prover, which symbolically performs deductive inference. Leveraging this
approach, we observe significant performance gains on FOLIO and a balanced
subset of ProofWriter for three different models in nearly all experimental
conditions we evaluate. On ProofWriter, augmenting the comparatively small
open-source StarCoder+ (15.5B parameters) with LINC even outperforms GPT-3.5
and GPT-4 with Chain-of-Thought (CoT) prompting by an absolute 38% and 10%,
respectively. When used with GPT-4, LINC scores 26% higher than CoT on
ProofWriter while performing comparatively on FOLIO. Further analysis reveals
that although both methods on average succeed roughly equally often on this
dataset, they exhibit distinct and complementary failure modes. We thus provide
promising evidence for how logical reasoning over natural language can be
tackled through jointly leveraging LLMs alongside symbolic provers. All
corresponding code is publicly available at this https URL

通过使用神经符号计算来全面利用 LLMs 和符号化证明器，本文探索了以逻辑推理任务，特别是符合自然语言的任务为基础的解决方案。

LINC: 将语言模型与一阶逻辑证明器相结合的神经符号化逻辑推理方法

LINC: A Neurosymbolic Approach for Logical Reasoning by Combining  Language Models with First-Order Logic Provers

Neurosymbolic Programming (NP) techniques have the potential to accelerate
scientific discovery. These models combine neural and symbolic components to
learn complex patterns and representations from data, using high-level concepts
or known constraints. NP techniques can interface with symbolic domain
knowledge from scientists, such as prior knowledge and experimental context, to
produce interpretable outputs. We identify opportunities and challenges between
current NP models and scientific workflows, with real-world examples from
behavior analysis in science: to enable the use of NP broadly for workflows
across the natural and social sciences.

Neurosymbolic Programming techniques combine neural and symbolic components to learn complex patterns from data, and can interface with prior knowledge to produce interpretable outputs, providing opportunities for scientific discovery.