Skip to main content

Prerequisites

Before installing NL2FOL, ensure you have the following:

Python 3.7+

Python 3.7 or higher is required

CUDA (Optional)

NVIDIA GPU with CUDA for faster inference

CVC4/CVC5

SMT solver binary for logical verification

OpenAI API Key

Required if using GPT models

Clone the Repository

First, clone the NL2FOL repository:
git clone https://github.com/lovishchopra/NL2FOL.git
cd nl2fol

Install Python Dependencies

The project requires several key dependencies for LLM inference, transformers, and SMT solving.

Core Dependencies

Install all required packages using the provided requirements file:
pip install -r requirements.txt

Key Packages

The main dependencies include:
  • transformers (v4.33.3): Hugging Face transformers library for LLM access
  • torch (v2.4.1): PyTorch for model inference
  • torchvision (v0.19.1): Vision utilities
  • accelerate (v1.0.1): Distributed training and inference
  • tokenizers: Fast tokenization
  • sacremoses: Text preprocessing
  • openai (v1.52.0): OpenAI API client for GPT models
  • httpx (v0.27.2): Modern HTTP client
  • requests: HTTP library for API calls
  • pandas: DataFrame operations for dataset handling
  • numpy: Numerical computing
  • scikit-learn: Metrics calculation (via joblib)
  • pydantic (v2.9.2): Data validation
  • tqdm: Progress bars
  • click: CLI argument parsing
The requirements.txt includes many conda-built packages. If you encounter issues, consider using a conda environment or removing the file path references from the requirements.

Install SMT Solver

The project uses CVC4 or CVC5 for SMT solving. Download and install the solver:

CVC4 Installation

# Download CVC4 binary
wget https://github.com/CVC4/CVC4/releases/download/1.8/cvc4-1.8-x86_64-linux-opt

# Make it executable
chmod +x cvc4-1.8-x86_64-linux-opt

# Move to project root (or add to PATH)
mv cvc4-1.8-x86_64-linux-opt ./cvc4

CVC5 Installation (Alternative)

# Download CVC5 binary
wget https://github.com/cvc5/cvc5/releases/latest/download/cvc5-Linux

# Make it executable
chmod +x cvc5-Linux

# Move to project root
mv cvc5-Linux ./cvc5
The code references ./cvc4 in src/fol_to_cvc.py:24. Ensure the binary is named correctly or update the path in the code.

Set Up OpenAI API Key

If you plan to use GPT models, configure your OpenAI API key:
export OPENAI_API_KEY="your-api-key-here"
Or add it to your shell profile:
echo 'export OPENAI_API_KEY="your-api-key-here"' >> ~/.bashrc
source ~/.bashrc

Verify GPU Access (Optional)

If using a GPU, verify CUDA availability:
python -c "import torch; print(f'CUDA available: {torch.cuda.is_available()}'); print(f'GPU count: {torch.cuda.device_count()}')"
Expected output:
CUDA available: True
GPU count: 1

Directory Structure

After installation, ensure your directory structure looks like this:
nl2fol/
├── src/
│   ├── nl_to_fol.py          # Main NL to FOL conversion
│   ├── fol_to_cvc.py          # FOL to SMT conversion
│   ├── cvc.py                 # CVC script generator
│   ├── helpers.py             # Utility functions
│   └── interpret_smt_results.py
├── eval/
│   └── get_metrics.py         # Evaluation metrics
├── data/
│   ├── fallacies.csv          # Fallacy dataset
│   ├── fallacies_climate.csv  # Climate fallacies
│   └── nli_*.csv              # NLI datasets
├── prompts/                   # LLM prompt templates
├── results/                   # Output directory (create if needed)
├── requirements.txt
├── cvc4 (or cvc5)            # SMT solver binary
└── README.md

Create Output Directories

Create necessary directories for storing results:
mkdir -p results
The SMT output directories will be created automatically when running the pipeline.

Troubleshooting

Ensure you have the correct version:
pip install transformers==4.33.3 --upgrade
Reduce batch size or use CPU inference:
export CUDA_VISIBLE_DEVICES=""
Verify the binary path matches the code:
ls -la ./cvc4
# Or update line 24 in src/fol_to_cvc.py
Verify your API key is set:
echo $OPENAI_API_KEY

Next Steps

Quick Start Guide

Learn how to run your first logical fallacy detection

Build docs developers (and LLMs) love