Fix citation and paper title
Browse files
README.md
CHANGED
|
@@ -12,7 +12,7 @@ base_model: Qwen/Qwen3-8B
|
|
| 12 |
|
| 13 |
# Goedel-Code-Prover-8B
|
| 14 |
|
| 15 |
-
**Paper:** [Goedel-
|
| 16 |
**Code:** [https://github.com/goedelcodeprover/Goedel-Code-Prover](https://github.com/goedelcodeprover/Goedel-Code-Prover)
|
| 17 |
|
| 18 |
Goedel-Code-Prover-8B is a Lean 4 proof generation model specialized in **proof decomposition** for code correctness verification. Given a formal specification in Lean 4, it decomposes the proof into smaller lemmas and proves the target theorem by combining them.
|
|
@@ -65,9 +65,13 @@ Formal Problem:
|
|
| 65 |
## Citation
|
| 66 |
|
| 67 |
```bibtex
|
| 68 |
-
@
|
| 69 |
-
|
| 70 |
-
|
| 71 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
| 72 |
}
|
| 73 |
```
|
|
|
|
| 12 |
|
| 13 |
# Goedel-Code-Prover-8B
|
| 14 |
|
| 15 |
+
**Paper:** [Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification](https://arxiv.org/abs/2603.19329)
|
| 16 |
**Code:** [https://github.com/goedelcodeprover/Goedel-Code-Prover](https://github.com/goedelcodeprover/Goedel-Code-Prover)
|
| 17 |
|
| 18 |
Goedel-Code-Prover-8B is a Lean 4 proof generation model specialized in **proof decomposition** for code correctness verification. Given a formal specification in Lean 4, it decomposes the proof into smaller lemmas and proves the target theorem by combining them.
|
|
|
|
| 65 |
## Citation
|
| 66 |
|
| 67 |
```bibtex
|
| 68 |
+
@misc{li2026goedelcodeproverhierarchicalproofsearch,
|
| 69 |
+
title={Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification},
|
| 70 |
+
author={Zenan Li and Ziran Yang and Deyuan and He and Haoyu Zhao and Andrew Zhao and Shange Tang and Kaiyu Yang and Aarti Gupta and Zhendong Su and Chi Jin},
|
| 71 |
+
year={2026},
|
| 72 |
+
eprint={2603.19329},
|
| 73 |
+
archivePrefix={arXiv},
|
| 74 |
+
primaryClass={cs.SE},
|
| 75 |
+
url={https://arxiv.org/abs/2603.19329},
|
| 76 |
}
|
| 77 |
```
|