vincentoh

kimina-prover-rrma-sft

Deploy Dedicated

Dedicated Endpoints

Run this model inference on single tenant GPU with unmatched speed and reliability at scale.

Learn more

Container

Run this model inference with full control and performance in your environment.

Learn more

Get help setting up a custom Dedicated Endpoints.

Talk with our engineer to get a quote for reserved GPU instances with discounts.

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

python
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")