This repository provides the code and data for Logic-LM, a framework designed to enhance Large Language Models' (LLMs) logical reasoning capabilities by integrating them with symbolic solvers. It targets researchers and developers working on LLM reasoning, offering a method to translate natural language problems into symbolic formulations for deterministic inference and self-correction.

How It Works

Logic-LM employs a two-stage process: first, an LLM converts natural language problems into a symbolic representation. Second, a deterministic symbolic solver executes inference on this formulation. A self-refinement module further improves accuracy by using solver error messages to revise the symbolic translations, aiming for more faithful logical reasoning.

Quick Start & Requirements

• Install: pip install -r requirements.txt
• Prerequisites: OpenAI API key, Python. Supports text-davinci-003 and gpt-4 models.
• Datasets: Preprocessed data for ProofWriter, PrOntoQA, FOLIO, LogicalDeduction, and AR-LSAT are available in the ./data folder.
• Documentation: https://arxiv.org/abs/2305.12295

Highlighted Details

• Achieves an average performance boost of 39.2% over standard LLM prompting and 18.4% over Chain-of-Thought prompting on five logical reasoning datasets.
• Includes a self-refinement module to iteratively improve symbolic formalizations based on solver feedback.
• Supports multiple logical reasoning benchmarks, including deductive reasoning, first-order logic, constraint satisfaction, and analytical reasoning.
• Offers backup strategies (random or LLM-based) for cases where symbolic solver execution fails.

Maintenance & Community

The project is associated with the NLP Group at UC Santa Barbara. For issues, users can contact Liangming Pan or open an issue on the GitHub repository.

Licensing & Compatibility

The repository's license is not explicitly stated in the README. The SMT solver code is modified from SatLM.

Limitations & Caveats

The README does not specify the license, which may impact commercial use. Successful execution relies on the LLM's ability to generate correct symbolic formulations, and the effectiveness of the self-refinement module depends on informative error messages from the symbolic solver.