Views
No views yet
1from vllm import LLM, SamplingParams
2from transformers import AutoTokenizer
3model_name = "AI-MO/Kimina-Prover-72B"
4model = LLM(
5 model=model_name,
6 tensor_parallel_size=8, # Should have 8 GPUs on this node
7 max_model_len=131072,
8 )
9tokenizer = AutoTokenizer.from_pretrained(model_name, trust_remote_code=True)
10problem = "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?"
11formal_statement = """import Mathlib
12import Aesop
13set_option maxHeartbeats 0
14open BigOperators Real Nat Topology Rat
15/-- 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.-/
16theorem mathd_algebra_478 (b h v : ℝ) (h₀ : 0 < b ∧ 0 < h ∧ 0 < v) (h₁ : v = 1 / 3 * (b * h))
17 (h₂ : b = 30) (h₃ : h = 13 / 2) : v = 65 := by
18"""
19prompt = "Think about and solve the following problem step by step in Lean 4."
20prompt += f"\n# Problem:{problem}"""
21prompt += f"\n# Formal statement:\n```lean4\n{formal_statement}\n```\n"
22messages = [
23 {"role": "system", "content": "You are an expert in mathematics and proving theorems in Lean 4."},
24 {"role": "user", "content": prompt}
25]
26text = tokenizer.apply_chat_template(
27 messages,
28 tokenize=False,
29 add_generation_prompt=True
30)
31sampling_params = SamplingParams(temperature=0.6, top_p=0.95, max_tokens=8096)
32output = model.generate(text, sampling_params=sampling_params)
33output_text = output[0].outputs[0].text
34print(output_text)