license: apache-2.0
task_categories:
- text-generation
- question-answering
language: - en
tags: - mathematics
- reasoning
- red-teaming
- formal-verification
- complexity-theory
- synthetic
pretty_name: FORGE-REASON v1
size_categories: - 1K<n<10K
FORGE-REASON v1
Dataset Description
FORGE-REASON is the first open-source dataset of red-teamed mathematical proofs
for fine-tuning LLMs on formal logical reasoning. Each entry contains a triple:
flawed_proof → directive4_critique → corrected_proof
Proofs span four mathematical domains: computational complexity theory, number theory,
cryptography (protocol security), and combinatorics.
Intended Use
- Fine-tuning open-source LLMs (Llama, Mistral, Qwen) on mathematical reasoning
- Training hostile peer-reviewer models (Directive-4 style)
- Benchmarking LLM robustness to subtle logical flaws
- Research on formal verification of natural language proofs
Out-of-Scope Use
- This dataset contains intentionally flawed proofs. Do NOT use flawed_proof entries
as ground-truth mathematics. Always use the corrected_proof field for valid content. - Not suitable for formal theorem provers without human review.
Dataset Statistics
| Split | Entries |
|---|---|
| train | ~80% |
| validation | ~10% |
| test | ~10% |
Domains: complexity, number_theory, cryptography, combinatorics
Difficulty: graduate-level
Flaw types: circular_dependency, domain_restriction, hidden_assumption,
overclaim, missing_base_case, invalid_reduction
Example Entry
{
"id": "forge-reason-00001",
"domain": "complexity",
"difficulty": "graduate",
"flawed_proof": {
"claim": "P = NP via polynomial-time 3-SAT solver",
"proof_text": "Let A be a 3-SAT instance...",
"flaw_type": "circular_dependency",
"flaw_description": "Reduction assumes NP ⊆ P to invoke the oracle"
},
"critique": {
"directive4_report": "Step 3 invokes an NP oracle...",
"identified_flaw_type": "circular_dependency",
"confidence": 0.92,
"findings": ["Oracle invocation at step 3 assumes P=NP"]
},
"correction": {
"corrected_proof": "Restrict to class of bounded-depth circuits...",
"correction_type": "scope_restriction",
"explanation": "The claim is restricted to NC¹ circuits where..."
},
"metadata": {
"z3_validated": false,
"generation_model": "claude-sonnet-4-6",
"critique_model": "claude-sonnet-4-6",
"timestamp": "2026-04-13T00:00:00+00:00",
"tokens_used": 1842
}
}
Contact
Dominik Blain — [email protected]
Inquiries about custom dataset generation, fine-tuning engagements,
or research collaborations welcome.
License
Apache 2.0
Citation
@dataset{forge_reason_v1_2026,
title={FORGE-REASON v1: Synthetic Red-Teamed Mathematical Proofs},
author={Blain, Dominik},
year={2026},
url={https://huggingface.co/datasets/Blainer28/forge-reason-v1}
}