englund/quantum-lean-hard-vvuq-dataset

Quantum Lean Hard VVUQ Dataset

Overview

This dataset contains challenging Lean 4 verification and repair problems designed to test advanced reasoning capabilities and demonstrate the effectiveness of Physics World Models (PWMs) in formal verification.

Problem Categories

• —Type Theory: 3 problems (coercion, dependent types, universes)
• —Tactic Sequences: 3 problems (wrong tactics, incorrect ordering)
• —Proof Strategies: 3 problems (wrong high-level approaches)
• —Advanced Type Theory: 1 problems (higher-order reasoning)
• —Baseline: 1 problems (simple for comparison)

Difficulty Distribution

• —Easy: 1 problems
• —Hard: 4 problems
• —Expert: 6 problems

PWM Knowledge Levels

• —W1 (Basic): 1 problems
• —W2 (Intermediate): 3 problems
• —W3 (Advanced): 7 problems

Expected Performance

• —Method A (LLM only): Should struggle with hard/expert problems
• —Method E (LLM + W3): Should handle most problems successfully
• —Clear gradient: Performance should improve from A→B→C→D→E

Dataset Structure

Each example contains:

• —id: Unique problem identifier
• —category: Problem category (typetheory, tacticsequence, proof_strategy, etc.)
• —difficulty: Difficulty level (easy, hard, expert)
• —corrupted_code: Lean code with intentional errors
• —repair_target: Correct version of the code
• —error_info: Detailed error information
• —domain_knowledge_required: List of concepts needed to solve
• —pwm_level: Required Physics World Model knowledge level

Usage

This dataset is designed for NeurIPS experiments demonstrating PWM effectiveness in formal verification tasks.

from datasets import load_dataset

# Load the dataset
dataset = load_dataset("englund/quantum-lean-hard-vvuq-dataset")

# Access train split
train_data = dataset["train"]

# Example usage
for example in train_data:
    print(f"Problem: {example['id']}")
    print(f"Corrupted: {example['corrupted_code']}")
    print(f"Target: {example['repair_target']}")
    print(f"Difficulty: {example['difficulty']}")

Requirements

• —Lean 4 with Mathlib
• —Enhanced diagnostics: set_option diagnostics true
• —Actual compilation verification (RequirementLEAN)

Citation

If you use this dataset, please cite:

@dataset{englund2025quantum,
  title={Quantum Lean Hard VVUQ Dataset},
  author={Englund, Dirk},
  year={2025},
  url={https://huggingface.co/datasets/englund/quantum-lean-hard-vvuq-dataset}
}