imbue2025/RWKV-7-Prover-1.5b

Model Card: RWKV-7 Prover 1.5B

1. Model Summary

RWKV-7 Prover 1.5B is a model fine-tuned on Lean 4 formal mathematical statement data using State Tuning, based on the RWKV-7-World-1.5B base model. This model is designed to enhance the understanding of Lean 4 syntax, specifically for the generation and completion of mathematical proposition statements.

• Architecture: RWKV-7 (Linear Attention)
• Parameters: 1.5 Billion
• Fine-tuning Method: State Tuning
• Training Date: 2026-02-02
• Context Length: 4096 tokens

2. Training Data

The model was trained on a specially curated Lean dataset. Partial data synthesis was performed using Gemini-3-flash as the teacher model.

• Data Format: JSONL (Instruction-following)
• Main Content: Lean 4 theorem statements, definitions, and related mathematical descriptions.
• Pre-processing: Tokenized using RWKVTokenizer and converted into binary .bin and .idx formats for efficient training.

3. Training Hyperparameters

• Epochs: 10
• Batch Size: 25 iterations per epoch (with gradient accumulation)
• Learning Rate: 1e-5
• Precision: bfloat16
• Final Loss: ~1.09

4. Usage

Inference Code Example

from rwkv.model import RWKV
from rwkv.utils import PIPELINE, PIPELINE_ARGS

# Load the model
model = RWKV(model='/path/to/rwkv7-prover-1.5b-merged.pth', strategy='cuda bf16')
pipeline = PIPELINE(model, "rwkv_vocab_v20230424")

instruction = "Translate the following mathematical statement into Lean 4:"
input_content = "There are infinitely many primes."
ctx = f"Instruction: {instruction}\n\nInput: {input_content}\n\nResponse:"

def my_print(s):
    print(s, end='', flush=True)

# Generate response
pipeline.generate(ctx, token_count=200, args=PIPELINE_ARGS(
    top_k=50, top_p=0.7, temperature=1.0, stop_token_ids=[0]), callback=my_print)

5. Limitations & Bias

• Proof Generation: This model is primarily optimized for proposition statements. Its ability to derive complex proof steps (Tactics) may still be limited by the base model.
• Hallucination: The model may generate Lean code that is syntactically correct but logically incorrect.
• Version Constraints: Specifically targeted at Lean 4; it may not be compatible with Lean 3.

6. Citation & Acknowledgements

• RWKV Architecture: Special thanks to BlinkDL for developing the RWKV series of models.
• Fine-tuning Tools: Developed using the RWKV-PEFT framework.