Update README.md
Browse files
README.md
CHANGED
|
@@ -1,7 +1,16 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
# Lean Conjecturer
|
| 2 |
|
| 3 |
This model generates Lean 4 conjectures from given theorem statements.
|
| 4 |
|
|
|
|
|
|
|
| 5 |
|
| 6 |
## Usage
|
| 7 |
|
|
@@ -53,4 +62,4 @@ sampling_params = SamplingParams(
|
|
| 53 |
|
| 54 |
model_outputs = model.generate(model_inputs, sampling_params, use_tqdm=True)
|
| 55 |
print(model_outputs[0].outputs[0].text)
|
| 56 |
-
```
|
|
|
|
| 1 |
+
---
|
| 2 |
+
license: apache-2.0
|
| 3 |
+
language:
|
| 4 |
+
- en
|
| 5 |
+
base_model:
|
| 6 |
+
- deepseek-ai/DeepSeek-Prover-V1.5-SFT
|
| 7 |
+
---
|
| 8 |
# Lean Conjecturer
|
| 9 |
|
| 10 |
This model generates Lean 4 conjectures from given theorem statements.
|
| 11 |
|
| 12 |
+
For more details, please see https://github.com/Slim205/RL-Lean
|
| 13 |
+
|
| 14 |
|
| 15 |
## Usage
|
| 16 |
|
|
|
|
| 62 |
|
| 63 |
model_outputs = model.generate(model_inputs, sampling_params, use_tqdm=True)
|
| 64 |
print(model_outputs[0].outputs[0].text)
|
| 65 |
+
```
|