# 🧩 ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization

**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 +22.6pp improvement** over the strongest baseline across four formalization benchmarks (miniF2F, ProofNet, Putnam, and AIME 2025). ---

_{Figure: ReForm consistently outperforms Goedel-V2 and Kimina-Autoformalizer on all benchmarks.}

--- ## 💡 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=32768) 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 @misc{chen2025reform, title={ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization}, author={Guoxin Chen and Jing Wu and Xinjie Chen and Wayne Xin Zhao and Ruihua Song and Chengxi Li and Kai Fan and Dayiheng Liu and Minpeng Liao}, year={2025}, eprint={2510.24592}, archivePrefix={arXiv}, primaryClass={cs.CL}, url={https://arxiv.org/abs/2510.24592}, } ```