Intermediate Languages Matter: Formal Choice Drives Neurosymbolic LLM Reasoning

TL;DR

This paper investigates how the choice of formal language impacts the reasoning capabilities of neurosymbolic LLM systems, highlighting the importance of selecting appropriate intermediate languages for improved performance.

Contribution

It demonstrates that the formal language choice significantly influences reasoning ability, introduces the intermediate language challenge, and compares effects of different in-context examples.

Findings

Formal language choice affects reasoning performance

Context-aware encodings improve reasoning

Comments or markdown have no significant effect

Abstract

Large language models (LLMs) achieve astonishing results on a wide range of tasks. However, their formal reasoning ability still lags behind. A promising approach is Neurosymbolic LLM reasoning. It works by using LLMs as translators from natural to formal languages and symbolic solvers for deriving correct results. Still, it remains unclear what the contributing factors to the success of Neurosymbolic LLM reasoning are. This paper shows that one important factor is the choice of the formal language. By comparing 4 formal languages on 3 datasets over 6 LLMs, we show that the choice of formal language affects both the syntactic and the semantic reasoning capability. Thereby, we introduce the intermediate language challenge, which is the challenge of picking a suitable formal language for neurosymbolic reasoning. Further, we compare the effects of using different in-context-learning examples in an ablation study. We conclude that on average, context-aware encodings help LLMs to reason, while there is no apparent effect of using comments or markdown syntax.