Update README.md

README.md

@@ -1,3 +1,74 @@
----
-license: apache-2.0
----
+---
+license: apache-2.0
+language:
+- en
+base_model:
+- Qwen/Qwen3-8B
+---
+<div align="center">
+
+# 🧩 ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization
+
+<a href="https://arxiv.org/pdf/2502.06205"><img src="https://img.shields.io/badge/Paper-arXiv-d63031?logo=arxiv&logoColor=white"></a>
+<a href="https://huggingface.co/collections/GuoxinChen/reform"><img src="https://img.shields.io/badge/%F0%9F%A4%97%20Hugging%20Face-Models-0984e3"></a>
+<a href="https://github.com/Chen-GX/ReForm"><img src="https://img.shields.io/badge/GitHub-ReForm-black?logo=github"></a>
+
+</div>
+
+**ReForm** is a reflective **Autoformalization** framework that enables large language models to *generate → verify → refine* formal mathematical statements in an integrated self-corrective loop. 
+It introduces **Prospective Bounded Sequence Optimization (PBSO)** — a novel reinforcement learning algorithm designed for heterogeneous rewards at different sequence positions — enabling stable, reflective training and substantial gains in semantic fidelity.
+
+---
+
+## 🚀 Highlights
+
+- 🪞 **Reflective Autoformalization Paradigm**  
+  Turns single-pass translation into an iterative “generate–validate–refine” cycle, allowing the model to autonomously detect and correct semantic errors.
+
+- ⚖️ **Prospective Bounded Sequence Optimization (PBSO)**  
+  A reinforcement learning algorithm with position-specific rewards for both task accuracy and critique quality, ensuring stable and interpretable optimization.
+
+- 📈 **State-of-the-art Semantic Consistency**  
+  ReForm achieves an **average +17.2pp improvement** over the strongest baseline across four formalization benchmarks (miniF2F, ProofNet, Putnam, and AIME 2025).
+
+---
+
+<div align="center">
+  <img src="https://github.com/Chen-GX/ReForm/raw/main/images/benchmark_comparison.png" width="100%">
+  <br>
+  <sub><b>Figure:</b> ReForm consistently outperforms Goedel-V2 and Kimina-Autoformalizer on all benchmarks.</sub>
+</div>
+
+---
+
+## 💡 Quick Start
+
+```python
+from transformers import AutoTokenizer, AutoModelForCausalLM
+
+model_name = "GuoxinChen/ReForm-8B"  # or "GuoxinChen/ReForm-32B"
+tokenizer = AutoTokenizer.from_pretrained(model_name)
+model = AutoModelForCausalLM.from_pretrained(model_name, torch_dtype="auto", device_map="auto")
+
+prompt = "Think step by step to translate the mathematical problem in natural language to Lean 4, and verify the consistency.\nLet $a_1, a_2,\\cdots, a_n$ be real constants, $x$ a real variable, and $f(x)=\\cos(a_1+x)+\\frac{1}{2}\\cos(a_2+x)+\\frac{1}{4}\\cos(a_3+x)+\\cdots+\\frac{1}{2^{n-1}}\\cos(a_n+x).$ Given that $f(x_1)=f(x_2)=0,$ prove that $x_2-x_1=m\\pi$ for some integer $m.$"
+
+inputs = tokenizer(prompt, return_tensors="pt").to(model.device)
+outputs = model.generate(**inputs, max_new_tokens=512)
+print(tokenizer.decode(outputs[0], skip_special_tokens=True))
+```
+
+
+More Details please refer to our [Github Repo](https://github.com/Chen-GX/ReForm).
+
+# 📚 Citation
+
+If you find ReForm useful for your research, please cite:
+
+```bibtex
+@article{chen2025reform,
+  title={ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization},
+  author={Chen, Guoxin and Wu, Jing and Chen, Xinjie and Zhao, Wayne Xin and Song, Ruihua and Li, Chengxi and Fan, Kai and Liu, Dayiheng and Liao, Minpeng},
+  journal={arXiv preprint arXiv:2502.06205},
+  year={2025}
+}
+```