Update README.md
Browse files
README.md
CHANGED
|
@@ -8,6 +8,11 @@ This is the formalizer for translating infromal math problem into formal stateme
|
|
| 8 |
Different from all previous open-source formalizers, this formalizer has the ability to think before generating the lean4 statements, which significantly increases the acurracy of the translation.
|
| 9 |
In our internal evaluation, we test the performance of formalizers on a eval set containing 300 informal statements from Omni-MATH. Kimina-formalizer-8B successfully translates 161/300 statements, while Goedel-Formalizer-V2-32B success in 228 statements.
|
| 10 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 11 |
Here is an example code to use this formalizer:
|
| 12 |
|
| 13 |
```
|
|
|
|
| 8 |
Different from all previous open-source formalizers, this formalizer has the ability to think before generating the lean4 statements, which significantly increases the acurracy of the translation.
|
| 9 |
In our internal evaluation, we test the performance of formalizers on a eval set containing 300 informal statements from Omni-MATH. Kimina-formalizer-8B successfully translates 161/300 statements, while Goedel-Formalizer-V2-32B success in 228 statements.
|
| 10 |
|
| 11 |
+
| Model | Formalization Success Rate |
|
| 12 |
+
|----------|----------|
|
| 13 |
+
| Kimina-formalizer-8B | 161/300 |
|
| 14 |
+
| Goedel-Formalizer-V2-32B | 226/300 |
|
| 15 |
+
|
| 16 |
Here is an example code to use this formalizer:
|
| 17 |
|
| 18 |
```
|