Modalis: Gamifying Modal Logic

Modalis is a text-based dungeon crawler that uses a neurosymbolic architecture to teach the semantics of modal logic. It combines a deterministic Kripke model generator (Python) with a narrative Large Language Model (Qwen-2.5-7B) to create procedurally generated logic puzzles.

Problem & Solution

Modal logic is intuitive when visualized with Kripke models and diagrams, but this understanding often fails to transfer when working with text-based formulas. Modalis bridges this gap by turning modal logic semantics into an interactive game loop where players:

1. Navigate a procedurally generated Kripke model (worlds connected by accessibility relations)
2. Observe local conditions (what propositions are true at each location)
3. Reason about modal formulas using both □ (necessity) and ◇ (possibility) operators
4. Receive deterministic grading from a ground-truth logic engine

This creates a bridge between theoretical understanding and practical intuition.

Architecture

The system uses a hybrid neurosymbolic design with clear separation of concerns:

Backend (Logic Engine)

• Kripke Model Generator: Procedurally generates diverse, non-trivial models with rejection sampling to ensure multiple atomic propositions and avoid logical redundancies
• Formula Generator: Creates formulas matched to difficulty levels with semantic diversity constraints
• Ground Truth Evaluator: Recursive model checker that determines the correct answer deterministically

Semantic Layer

• Translates abstract logical structures into narrative game elements (worlds → locations, accessibility → paths, valuation → sensor data)
• Implements partial observability; the LLM only sees the current world and immediate neighbors, reducing interpretability burden and improving response quality

Neural Interface (LLM)

• Model: Qwen-2.5-7B-Instruct (selected for strong reasoning at smaller scale)
• Role: Game Master that translates Kripke models into coherent narratives and explains logical outcomes
• Governance: Strict system prompt guides operator translation (□ vs ◇) to prevent hallucinations

Project Structure

• modalis_game.ipynb: The complete game implementation. This single file contains the logic engine, the semantic mapping layer, and the neural interface setup.

Installation & Requirements

This project is designed to run entirely in the cloud using Google Colab. No local installation is required.

• Platform: Google Colab
• Hardware: Free Tier T4 GPU (or better)
• Python Dependencies: torch, transformers, accelerate, bitsandbytes (these are installed automatically when you run the notebook).

How to Run

1. Download the Notebook: Download the cosi112_final_project.ipynb file from this repository.
2. Upload to Google Colab:

• Go to colab.research.google.com.
• Click File > Upload notebook and select the .ipynb file.

3. Enable GPU Runtime:

• In the Colab menu, go to Runtime > Change runtime type.
• Under "Hardware accelerator," select T4 GPU.
• Click Save.

4. Execute the Game:

• Go to Runtime > Run all.
• Wait for the model to load (approx. 2-3 minutes).
• Scroll to the final cell to see the game interface.

How to Play

1. Select Difficulty: Enter a number (1-5) to generate a new dungeon with increasing complexity.
2. Read the Scenario: The Game Master describes your location and the status of your scanners (p and q).
3. Analyze the Logic:
   • Possibility (◇): "Is there a path...?" (Check if at least one neighbor satisfies the condition).
   • Necessity (□): "Is it true for all paths...?" (Check if every neighbor satisfies the condition).
4. Answer: Type yes or no to submit your answer. The system grades you using the ground truth logic engine. Type hint for a rephrased question.
5. Learn: The system explains the outcome by tracing the logical connections in the model.

Key Technical Achievements

• Procedural Diversity: Rejection sampling ensures non-trivial puzzles with multiple atomic propositions, avoiding vacuously true or trivial formulas
• Logical Consistency: Ground truth evaluator maintains deterministic grading independent of LLM output
• Efficient Context Usage: Semantic layer's partial observability approach allows a smaller LLM to reason effectively about large logical structures
• Replayability: Infinite unique puzzles through procedural generation with structural and semantic constraints

Limitations & Future Work

• LLM Reasoning: The 7B model occasionally conflates universal (□) and existential (◇) quantifiers in complex explanations
• Hallucinations: While the semantic layer mitigates this, complex nested formulas can trigger LLM inaccuracies in step-by-step reasoning
• Future Improvements:
  • Upgrade to larger, more capable LLM for deterministic explanations
  • Expand to other logical systems (Linear Temporal Logic, Epistemic Logic)
  • Add more deterministic narrative generation to the backend