Source-linked AI summary
FOLIO: Natural Language Reasoning with First-Order Logic
Simeng Han, Hailey Schoelkopf, Yilun Zhao, Zhenting Qi, Martin Riddell, Wenfei Zhou, James Coady, David Peng, Yujie Qiao, Luke Benson, Lucy Sun, Alex Wardle-Solano, Hannah Szabo, Ekaterina Zubova, Matthew Burtell, Jonathan Fan, Yixin Liu, Brian Wong, Malcolm Sailor, Ansong Ni, Linyong Nan, Jungo Kasai, Tao Yu, Rui Zhang, Alexander R. Fabbri, Wojciech Kryscinski, Semih Yavuz, Ye Liu, Xi Victoria Lin, Shafiq Joty, Yingbo Zhou, Caiming Xiong, Rex Ying, Arman Cohan, Dragomir Radev
TL;DR
Existing benchmarks provide inadequate evidence about models’ ability to perform complex logical reasoning. The paper introduces FOLIO, an expert-annotated natural-language dataset with formally verified first-order logic annotations, and evaluates language models on reasoning and NL-FOL translation. FOLIO remains challenging for leading LLMs, while the dataset’s rigorous construction limits its current scale.
Problem
Existing natural-language tasks and benchmarks inadequately measure complex logical reasoning capabilities, motivating an independent evaluation of this ability.
Method
FOLIO pairs expert-written natural-language reasoning stories with first-order logic annotations, supports NL-FOL translation, and evaluates models through supervised fine-tuning and prompting.
Results
FOLIO challenges leading language models: the most capable publicly available LLM achieves 53.1% on hybrid-written stories under few-shot prompting, while GPT-4 achieves the best results among GPT-series models in the reported NL-reasoning results.
Takeaways & Limitations
FOLIO provides a challenging benchmark for measuring progress in first-order logic reasoning and a dataset for NL-FOL translation evaluation.
Takeaways & Limitations
FOLIO prioritizes high-quality expert annotation over scale, limiting expansion for studying how training-data size affects fine-tuning performance.
Abstract
from arXiv · showhide
Large language models (LLMs) have achieved remarkable performance on a variety of natural language understanding tasks. However, existing benchmarks are inadequate in measuring the complex logical reasoning capabilities of a model. We present FOLIO, a human-annotated, logically complex and diverse dataset for reasoning in natural language (NL), equipped with first-order logic (FOL) annotations. FOLIO consists of 1,430 examples (unique conclusions), each paired with one of 487 sets of premises used to deductively reason for the validity of each conclusion. The logical correctness of the premises and conclusions is ensured by their FOL annotations, which are automatically verified by an FOL inference engine. In addition to the main NL reasoning task, NL-FOL pairs in FOLIO constitute a new NL-FOL translation dataset. Our experiments on FOLIO systematically evaluate the FOL reasoning ability of supervised fine-tuning on medium-sized language models. For both NL reasoning and NL-FOL translation, we benchmark multiple state-of-the-art language models. Our results show that a subset of FOLIO presents a challenge for one of the most capable {Large Language Model (LLM)} publicly available, GPT-4.
1 Introduction
FOLIO addresses limitations in existing logical-reasoning benchmarks by providing expert-written natural-language problems with first-order logic annotations and challenging evaluations. Its results indicate that complex FOL reasoning remains difficult for leading language models.
- Motivation: Existing benchmarks inadequately measure complex logical reasoning and often provide limited reasoning complexity, language naturalness, or logical diversity.Some benchmarks also fail to isolate logical reasoning from other reasoning abilities.
- Dataset: FOLIO asks models to determine whether conclusions follow from premises defining a world, using first-order logic reasoning problems written in natural language.The dataset targets high language naturalness, vocabulary diversity, factuality, and reasoning complexity.
- Dataset: FOLIO combines expert-written stories with parallel FOL formulas that ensure the logical validity of natural-language premises and conclusions.Its examples are mostly aligned with real-world knowledge and include diverse logic patterns and reasoning depths.
- Dataset: Table 2 illustrates stories requiring all five premises and reasoning with universal quantification, negation, conjunction, and disjunction.The example contains three conclusions with corresponding FOL formulas and labels.
- Results: 53.1% is achieved by the most capable publicly available LLM on hybrid-written stories under few-shot prompting, only slightly above random.The result highlights the difficulty of FOLIO’s logical reasoning task.
- Contributions: The paper releases FOLIO, proposes NL-FOL translation, and benchmarks fine-tuned and few-shot language models to measure logical reasoning capabilities.These contributions are intended to facilitate progress measurement in language-model logical reasoning.
2 Related Work
Prior text-reasoning benchmarks cover capabilities such as natural-language inference, commonsense, multi-hop, inductive, and deductive reasoning, but logical-reasoning datasets often sacrifice naturalness or expressive complexity. FOLIO is positioned as a more natural, diverse, and formally annotated first-order logic benchmark, while remaining difficult for LLMs.
- Existing benchmarks: Earlier benchmarks evaluate natural-language inference, commonsense knowledge, multi-hop reasoning, inductive reasoning, and deductive reasoning over text.These benchmarks address different reasoning abilities and do not all target first-order logic.
- Existing benchmarks: Synthetic deductive-reasoning datasets often contain unnatural sentences and limited logical forms, whereas first-order logic is more expressive.CLUTRR focuses on inductive reasoning, which is outside the scope of first-order logic.
- Existing benchmarks: ProntoQA uses queries resolvable through Modus Ponens, while FOLIO requires multiple types of inference rules.This distinguishes FOLIO’s reasoning demands from a single-rule logical setting.
- FOLIO: FOLIO is described as the first large-scale FOL reasoning dataset with formal FOL annotations, natural language, real-world knowledge, and diverse logic patterns.The comparison emphasizes reasoning depth, distinct logic patterns, and vocabulary variety.
- FOLIO: FOLIO aims to prevent high performance from superficial strategies and shallow heuristics, and reports that many LLMs fall short on complex first-order logic reasoning.The authors conclude that substantial room for improvement remains.
3 FOLIO Corpus Construction
FOLIO combines expert manual annotation with hybrid construction and extensive quality control to produce natural-language stories with complex, diverse, and formally verified logical structure. Its statistics indicate substantial reasoning depth, vocabulary breadth, and diversity, while ambiguity reduction introduces a documented tradeoff.
- Corpus construction: Expert annotators wrote and reviewed stories requiring semantic parsing, first-order logic knowledge, and strong analytical skills.Separate checks involved experts in natural language processing, computational linguistics, and first-order logic.
- Corpus construction: FOLIO was built through six stages spanning WikiLogic, HybLogic, language and logic quality control, alignment, and verification.The process required 980 man-hours.
- Collection methods: WikiLogic uses Wikipedia seeds and unrestricted story topics, producing varied topics, abundant AST variations, and broad vocabulary.Stories were written from scratch without templates and include parallel FOL sentences for premises and conclusions.
- Collection methods: HybLogic combines multiple valid syllogisms into chained templates and adds conjunction, disjunction, and implication to facilitate complex story generation.A syllogism contains two premises and one conclusion; one syllogism’s conclusion can become the next premise.
- Quality control: Quality control addressed factuality, bias, grammar, naturalness, ambiguity, FOL consistency, NL-FOL equivalence, and commonsense premises.The protocol reduced ambiguity but limited some language variation, while preserving variation in sentence and logical structures.
- Dataset statistics: 28.7% of FOLIO examples require five or more reasoning depths, while its mode is four and its AST diversity exceeds previous datasets.FOLIO contains 4,351 words; Wikipedia-based examples account for 74% of vocabulary and 63% of stories.
4 Task Definition
FOLIO defines natural-language reasoning with first-order logic and NL-FOL translation as complementary tasks. The first determines conclusion truth from premises, while the second translates aligned natural-language stories into semantically equivalent FOL stories and evaluates syntax and inference execution.
- Task overview: FOLIO defines two tasks: natural-language reasoning with first-order logic and NL-FOL translation.
- Natural-language reasoning: In natural-language reasoning, models classify each conclusion as True, False, or Unknown given the story’s premises and conclusions.Each NL story has parallel FOL premises and conclusions with logically and semantically similar meanings.
- NL-FOL translation: NL-FOL translation maps each natural-language sentence to a logically and semantically equivalent first-order formula while preserving conclusion truth values.The task also requires discourse-level consistency rather than sentence-level translation alone.
- Evaluation: NL-FOL translation is evaluated by syntactic validity and inference-engine execution accuracy.Syntactic validity checks formula well-formedness, while execution accuracy compares inferred conclusion labels; a more reliable metric is left for future work.
5 Experiments
Experiments evaluate FOLIO on logical reasoning and NL-FOL translation using supervised fine-tuning, few-shot prompting, and specialized prompting or reasoning methods. Results show substantial variation across models and methods, while syntactic FOL generation exceeds logically faithful translation.
- Tasks and evaluation: Experiments cover logical reasoning and NL-FOL translation, using accuracy for logical reasoning and the metrics defined for translation.The study evaluates both fully supervised fine-tuning and few-shot prompting, while translation uses few-shot prompting.
- Dataset split: FOLIO is split by story into 1,001 training, 203 validation, and 226 test examples, evaluating models on unseen stories.The split is 70%/15%/15%.
- Logical reasoning: 65.7% accuracy is achieved by Flan-T5-Large, the strongest fully supervised fine-tuning result; BERT-base and RoBERTa-base each reach 56.83%.BERT-large improves 2.2% over BERT-base, while RoBERTa-large improves 3.1% over BERT-large.
- Logical reasoning: Under few-shot NL prompting, LLaMA-13B reaches 33.63%, LLaMA-70B reaches 43.97%, text-davinci-002 reaches 49.53%, and GPT-3.5 reaches 58.34%.LLaMA-70B improves by around 4% with chain-of-thought and tree-of-thought prompting, while GPT-4 performs best among GPT-series models.
- Logical reasoning: Chain-of-thought prompting raises GPT-4 performance by more than 4%, self-consistency adds 0.6%, and tree-of-thought performs slightly better than the self-consistent chain-of-thought version.LINC improves around 9% over few-shot GPT-4, while Logic-LM and DetermLR each improve by more than 13%.
- NL-FOL translation: GPT-3.5-Turbo and GPT-4 achieve around 93% syntactic validity in NL-FOL translation, but low inference-engine execution accuracy indicates limited logical or semantic fidelity.The results suggest that sufficiently large models can reproduce FOL patterns more readily than they can preserve an NL story’s meaning in FOL.
6 Error Analysis
FOLIO errors increase with reasoning depth and logical complexity, especially for few-shot LLMs, while human evaluation identifies faulty reasoning chains as the dominant GPT-4 failure mode.
- Reasoning depth: Few-shot GPT-3.5 and GPT-4 perform much better on 0–3-depth examples than on 4–7-depth examples.Fine-tuned RoBERTa shows a smaller depth-related performance gap.
- Reasoning depth: Fine-tuning on longer, more difficult reasoning chains can improve performance on equally long test chains.The authors connect this pattern to training examples containing longer reasoning chains.
- Dataset subsets: In NL-FOL translation, performance is 10 points better on HybLogic than on WikiLogic.The authors attribute this possibility to WikiLogic’s more diverse sentence-level logical and language patterns and FOL annotations.
- GPT-4 error types: Approximately 65% of incorrect GPT-4 truth-value predictions involve inaccurate reasoning chains for complex problems with intricate steps.Other errors involve erroneous intermediate derivations, complex syntax, or commonsense shortcuts.
- Human evaluation: Expert annotators achieve 95.98% truth-value accuracy versus 61.82% for non-experts, a 34.16-point gap.The comparison indicates that sufficient first-order-logic domain knowledge is necessary for accurate annotation.
7 Conclusion
The paper concludes that FOLIO is an expert-written, natural-language dataset with FOL formulas, diverse logic patterns, and substantial vocabulary. Experiments show that FOLIO challenges a highly capable publicly available LLM.
- FOLIO is an expert-written logical-reasoning dataset equipped with first-order-logic formulas.
- FOLIO uses real-world knowledge in natural language and contains many distinct logic patterns and a large vocabulary.
- Experiments show that FOLIO presents a challenge for one of the most capable publicly available large language models.
8 Limitations
The paper prioritizes a very high-quality dataset over scale. Rigorous domain-expert annotation limits how far the dataset could be expanded with the available resources.
- FOLIO prioritizes high-quality logical-reasoning evaluation rather than merely maximizing dataset size.
- Scaling the rigorous annotation process would require resources beyond the authors’ current means, preventing further expansion for studying training-data size effects.
A Annotator Selection
FOLIO uses qualified annotators and a structured protocol to produce natural-language examples with consistent, logically faithful FOL translations and verified conclusions.
- Annotator Selection: Annotators were college or graduate students with native or near-native English proficiency and formal first-order logic education.Natural-language quality checks were performed by experts meeting these criteria.
- FOL Annotation Protocol: FOLIO uses explicit conventions for disjunction, including exclusive “either-or” and inclusive “or both,” while retaining natural wording.Annotators decide whether ordinary “or” is inclusive or exclusive from linguistic context.
- FOL Annotation Protocol: The dataset favors natural expressions such as “Some A is B” and “All A are B” over more formal existential or conditional phrasing.The protocol also provides a natural construction for negation over exclusive disjunction.
- FOL Verification: FOL is used as an unambiguous representation whose formulas can be passed to an inference engine for exact conclusion truth values.A parser converts human-written formulas to the engine’s input format, and the prover returns True, False, or Unknown.
- FOL Representation: The annotation protocol excludes temporal and modal logic and primarily uses one-place and two-place predicates.N-place predicates are used when applicable, without Davidsonian or neo-Davidsonian semantics.
- FOL Annotation Protocol: The protocol preserves natural-language semantics and sentence structure while avoiding unnecessary semantic decomposition.For example, “John is a bachelor” becomes “Bachelor(John)” in FOL.
H Distribution of Readability
The paper reports FOLIO’s readability distribution and presents example stories with model predictions in the WikiLogic and HybLogic settings.
- Readability Distribution: Figure 3 shows the distribution of FOLIO examples’ Dale-Chall readability scores.The supplied passage identifies the figure but does not report specific score ranges or summary statistics.
- Example Stories: Tables 9 and 10 provide example WikiLogic and HybLogic stories together with model predictions.These examples are used in the paper’s case-study analysis.
I Case study
The case studies contrast GPT-4 and RoBERTa-Large predictions on WikiLogic and explain a more complex HybLogic reasoning example.
- WikiLogic: In the WikiLogic example, conclusion A is True from premises 5 and 3, while conclusions B and C are Unknown.The premises do not determine whether Cerura vinula has thin antennae or is a pest.
- WikiLogic: GPT-4 correctly predicts WikiLogic conclusions A and C, whereas RoBERTa-Large predicts all conclusions incorrectly.The comparison is reported for the example shown in Table 9.
- HybLogic: In the HybLogic example, conclusion B is False because the premises imply that James does not perform better than others and lacks time-management ability.The first conclusion remains Unknown because the premises do not determine whether James exercises weekly.
- HybLogic: Conclusion C is also False because the relevant conjunction is false, while the implication is evaluated through the equivalent form ¬p ∨ q.The example explicitly applies this equivalence during its reasoning process.
J Model Performance Analysis
FOLIO models show label-dependent performance, limited sensitivity to premise order, and slightly better few-shot results when NL sentences accompany FOL formulas.
- Label Performance: 61.9% with fine-tuning and 54.0% with few-shot prompting is the accuracy on False or Unknown conclusions.Models are significantly better at correctly predicting True conclusions and tend to overpredict True.
- Premise Ordering: Accuracy changes by roughly 1% in most settings after premise shuffling, indicating little useful information in the original premise order.The test targets possible spurious correlations between premise ordering and conclusion labels.
- Input Formats: Combining NL sentences with their FOL formulas slightly improves few-shot truth-value prediction compared with using either representation alone.The comparison includes prompts using only FOL formulas and prompts concatenating each NL sentence with its annotated FOL statement.