Add model card
Browse files
README.md
ADDED
|
@@ -0,0 +1,20 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
---
|
| 2 |
+
language:
|
| 3 |
+
- en
|
| 4 |
+
license: apache-2.0
|
| 5 |
+
tags:
|
| 6 |
+
- lean4
|
| 7 |
+
- theorem-proving
|
| 8 |
+
- verification
|
| 9 |
+
base_model: Qwen/Qwen3-8B
|
| 10 |
+
---
|
| 11 |
+
|
| 12 |
+
# Goedel-Verifier-Preview-8B
|
| 13 |
+
|
| 14 |
+
A Lean 4 code verification model fine-tuned from Qwen3-8B through supervised fine-tuning and reinforcement learning with online proof checking.
|
| 15 |
+
|
| 16 |
+
## Model Details
|
| 17 |
+
|
| 18 |
+
- **Base model:** Qwen3-8B
|
| 19 |
+
- **Training:** SFT on decomposition and proof completion trajectories, followed by GRPO with online Lean 4 verification rewards
|
| 20 |
+
- **Use case:** Verifying Lean 4 proof attempts for code correctness specifications
|