Kimina-Prover-Preview-Distill-7B

image/png

Kimina-Prover-Preview-Distill-7B 是由 Project Numina 与 Kimi 团队联合研发的定理证明模型，专注于 Lean 4 中的竞赛风格解题能力。该模型是 Kimina-Prover-Preview 的蒸馏版本，后者是通过大规模强化学习训练而成的模型。在同等模型规模和计算资源条件下，它在 MiniF2F-test 测试集上取得了最先进（SOTA）的结果；发布时，在计算资源有限的情况下，它在 PutnamBench 排行榜上位列第一。

使用 vLLM 快速开始

您可以通过 vLLM 轻松进行推理：

from vllm import LLM, SamplingParams
from transformers import AutoTokenizer

model_name = "AI-MO/Kimina-Prover-Preview-Distill-7B"
model = LLM(model_name)

tokenizer = AutoTokenizer.from_pretrained(model_name, trust_remote_code=True)

problem = "The volume of a cone is given by the formula $V = \frac{1}{3}Bh$, where $B$ is the area of the base and $h$ is the height. The area of the base of a cone is 30 square units, and its height is 6.5 units. What is the number of cubic units in its volume?"

formal_statement = """import Mathlib
import Aesop

set_option maxHeartbeats 0

open BigOperators Real Nat Topology Rat

/-- The volume of a cone is given by the formula $V = \frac{1}{3}Bh$, where $B$ is the area of the base and $h$ is the height. The area of the base of a cone is 30 square units, and its height is 6.5 units. What is the number of cubic units in its volume? Show that it is 65.-/
theorem mathd_algebra_478 (b h v : ℝ) (h₀ : 0 < b ∧ 0 < h ∧ 0 < v) (h₁ : v = 1 / 3 * (b * h))
    (h₂ : b = 30) (h₃ : h = 13 / 2) : v = 65 := by
"""

prompt = "Think about and solve the following problem step by step in Lean 4."
prompt += f"\n# Problem:{problem}"""
prompt += f"\n# Formal statement:\n```lean4\n{formal_statement}\n```\n"

messages = [
    {"role": "system", "content": "You are an expert in mathematics and Lean 4."},
    {"role": "user", "content": prompt}
]

text = tokenizer.apply_chat_template(
    messages,
    tokenize=False,
    add_generation_prompt=True
)

sampling_params = SamplingParams(temperature=0.6, top_p=0.95, max_tokens=8096)
output = model.generate(text, sampling_params=sampling_params)
output_text = output[0].outputs[0].text
print(output_text)

引用

如果您发现我们的工作对您有所帮助，您可以引用我们的论文：https://github.com/MoonshotAI/Kimina-Prover-Preview

Kimina-Prover-Preview-Distill-7B

使用 vLLM 快速开始

您可以通过 vLLM 轻松进行推理：

from vllm import LLM, SamplingParams
from transformers import AutoTokenizer

model_name = "AI-MO/Kimina-Prover-Preview-Distill-7B"
model = LLM(model_name)

tokenizer = AutoTokenizer.from_pretrained(model_name, trust_remote_code=True)

problem = "The volume of a cone is given by the formula $V = \frac{1}{3}Bh$, where $B$ is the area of the base and $h$ is the height. The area of the base of a cone is 30 square units, and its height is 6.5 units. What is the number of cubic units in its volume?"

formal_statement = """import Mathlib
import Aesop

set_option maxHeartbeats 0

open BigOperators Real Nat Topology Rat

/-- The volume of a cone is given by the formula $V = \frac{1}{3}Bh$, where $B$ is the area of the base and $h$ is the height. The area of the base of a cone is 30 square units, and its height is 6.5 units. What is the number of cubic units in its volume? Show that it is 65.-/
theorem mathd_algebra_478 (b h v : ℝ) (h₀ : 0 < b ∧ 0 < h ∧ 0 < v) (h₁ : v = 1 / 3 * (b * h))
    (h₂ : b = 30) (h₃ : h = 13 / 2) : v = 65 := by
"""

prompt = "Think about and solve the following problem step by step in Lean 4."
prompt += f"\n# Problem:{problem}"""
prompt += f"\n# Formal statement:\n```lean4\n{formal_statement}\n```\n"

messages = [
    {"role": "system", "content": "You are an expert in mathematics and Lean 4."},
    {"role": "user", "content": prompt}
]

text = tokenizer.apply_chat_template(
    messages,
    tokenize=False,
    add_generation_prompt=True
)

sampling_params = SamplingParams(temperature=0.6, top_p=0.95, max_tokens=8096)
output = model.generate(text, sampling_params=sampling_params)
output_text = output[0].outputs[0].text
print(output_text)