Update README.md
Browse files
README.md
CHANGED
|
@@ -25,18 +25,22 @@ text = "theorem mathd_numbertheory_3 : (∑ x in Finset.range 10, (x + 1) ^ 2) %
|
|
| 25 |
model_inputs = [get_prompt(text)]
|
| 26 |
|
| 27 |
print(model_inputs[0])
|
|
|
|
| 28 |
|
| 29 |
-
|
| 30 |
-
|
| 31 |
|
|
|
|
| 32 |
<theorem>
|
| 33 |
theorem mathd_numbertheory_3 : (∑ x in Finset.range 10, (x + 1) ^ 2) % 10 = 5 := by
|
| 34 |
</theorem>
|
| 35 |
<conjecture>
|
| 36 |
theorem mathd_numbertheory_24 : ∑ k in Finset.range 11, k ^ 2 = 385 := by
|
| 37 |
</conjecture>
|
|
|
|
|
|
|
|
|
|
| 38 |
|
| 39 |
-
|
| 40 |
model = LLM(model=model_name, seed=1, trust_remote_code=True, swap_space=8, tensor_parallel_size=1, max_model_len=4096)
|
| 41 |
|
| 42 |
sampling_params = SamplingParams(
|
|
@@ -48,5 +52,4 @@ sampling_params = SamplingParams(
|
|
| 48 |
|
| 49 |
model_outputs = model.generate(model_inputs, sampling_params, use_tqdm=True)
|
| 50 |
print(model_outputs[0].outputs[0].text)
|
| 51 |
-
|
| 52 |
-
|
|
|
|
| 25 |
model_inputs = [get_prompt(text)]
|
| 26 |
|
| 27 |
print(model_inputs[0])
|
| 28 |
+
```
|
| 29 |
|
| 30 |
+
Example output:
|
|
|
|
| 31 |
|
| 32 |
+
```lean4
|
| 33 |
<theorem>
|
| 34 |
theorem mathd_numbertheory_3 : (∑ x in Finset.range 10, (x + 1) ^ 2) % 10 = 5 := by
|
| 35 |
</theorem>
|
| 36 |
<conjecture>
|
| 37 |
theorem mathd_numbertheory_24 : ∑ k in Finset.range 11, k ^ 2 = 385 := by
|
| 38 |
</conjecture>
|
| 39 |
+
```
|
| 40 |
+
|
| 41 |
+
## Inference
|
| 42 |
|
| 43 |
+
```python
|
| 44 |
model = LLM(model=model_name, seed=1, trust_remote_code=True, swap_space=8, tensor_parallel_size=1, max_model_len=4096)
|
| 45 |
|
| 46 |
sampling_params = SamplingParams(
|
|
|
|
| 52 |
|
| 53 |
model_outputs = model.generate(model_inputs, sampling_params, use_tqdm=True)
|
| 54 |
print(model_outputs[0].outputs[0].text)
|
| 55 |
+
```
|
|
|