kimina-prover-rrma-sft

Kimina-Prover-7B — RRMA Lean4 SFT Adapter

LoRA adapter fine-tuned on 336 successful Lean 4 proof search traces from the RRMA multi-agent harness.

Base model

AI-MO/Kimina-Prover-Preview-Distill-7B

Training

• Dataset: vincentoh/rrma-lean4-agent-traces (reward=1.0 only)
• Method: 4-bit QLoRA, r=16, alpha=32
• Epochs: 3, max_length: 2048
• Final loss: 0.045, token accuracy: 99.1%
• Hardware: RTX 4070 Ti SUPER 16GB, ~35 min

What it learned

The edit→compile→diagnose→fix loop for Lean 4 proof search on Erdős #741(ii) and #125, all traces verified by hard Lean compiler reward (0/1).

Usage

from peft import PeftModel
from transformers import AutoModelForCausalLM, AutoTokenizer, BitsAndBytesConfig
import torch

bnb = BitsAndBytesConfig(load_in_4bit=True, bnb_4bit_compute_dtype=torch.bfloat16)
base = AutoModelForCausalLM.from_pretrained(
    "AI-MO/Kimina-Prover-Preview-Distill-7B",
    quantization_config=bnb, device_map="auto"
)
model = PeftModel.from_pretrained(base, "vincentoh/kimina-prover-rrma-sft")
tokenizer = AutoTokenizer.from_pretrained("vincentoh/kimina-prover-rrma-sft")