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.
Performance
task
dataset
metric
value
pass@
MiniF2F
MiniF2F benchmark
accuracy
39.6%
32
Usage
You can load the model using the Hugging Face Transformers library and apply it to tasks involving tactic state prediction and theorem proving.
For more details, check out the datasets and base model referenced above.
