AI-MO/Kimina-Prover-Distill-8B is an 8 billion parameter theorem proving model developed by Project Numina and Kimi teams. This model is a distillation of the larger Kimina-Prover-72B, trained using large-scale reinforcement learning. It specializes in competition-style problem solving within Lean 4, achieving 77.86% accuracy with Pass@32 on the MiniF2F-test benchmark. Its primary strength lies in formal mathematics and automated theorem proving.
Loading preview...
Model tree for
AI-MO/Kimina-Prover-Distill-8BMost commonly used values from Featherless users
temperature
This setting influences the sampling randomness. Lower values make the model more deterministic; higher values introduce randomness. Zero is greedy sampling.
top_p
This setting controls the cumulative probability of considered top tokens. Must be in (0, 1]. Set to 1 to consider all tokens.
top_k
This limits the number of top tokens to consider. Set to -1 to consider all tokens.
frequency_penalty
This setting penalizes new tokens based on their frequency in the generated text. Values > 0 encourage new tokens; < 0 encourages repetition.
presence_penalty
This setting penalizes new tokens based on their presence in the generated text so far. Values > 0 encourage new tokens; < 0 encourages repetition.
repetition_penalty
This setting penalizes new tokens based on their appearance in the prompt and generated text. Values > 1 encourage new tokens; < 1 encourages repetition.
min_p
This setting representing the minimum probability for a token to be considered relative to the most likely token. Must be in [0, 1]. Set to 0 to disable.