Create README.md
Browse files
README.md
ADDED
|
@@ -0,0 +1,27 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
---
|
| 2 |
+
license: apache-2.0
|
| 3 |
+
datasets:
|
| 4 |
+
- Kevew/mathlib4_summary_tactic_states
|
| 5 |
+
- Kevew/minif2f-kiminaprover8b-inferenced
|
| 6 |
+
base_model:
|
| 7 |
+
- nvidia/OpenReasoning-Nemotron-7B
|
| 8 |
+
---
|
| 9 |
+
|
| 10 |
+
|
| 11 |
+
# Model Description
|
| 12 |
+
|
| 13 |
+
This model is fine-tuned on tactic states from the Mathlib4 dataset and leverages inference data from MiniF2F Kiminaprover8b. It builds upon the NVIDIA OpenReasoning Nemotron 7B base model.
|
| 14 |
+
|
| 15 |
+
## Performance
|
| 16 |
+
|
| 17 |
+
| task | dataset | metric | value | pass@ |
|
| 18 |
+
|-------------|---------|----------|--------|--------|
|
| 19 |
+
| MiniF2F | MiniF2F benchmark | accuracy | 39.6% | 32 |
|
| 20 |
+
|
| 21 |
+
## Usage
|
| 22 |
+
|
| 23 |
+
You can load the model using the Hugging Face Transformers library and apply it to tasks involving tactic state prediction and theorem proving.
|
| 24 |
+
|
| 25 |
+
---
|
| 26 |
+
|
| 27 |
+
For more details, check out the datasets and base model referenced above.
|