Update README.md

README.md

@@ -4,348 +4,73 @@ license: apache-2.0
 license_link: https://huggingface.co/Qwen/Qwen3-32B/blob/main/LICENSE
 pipeline_tag: text-generation
 ---
+<div align="center">
 
-# Qwen3-32B
-<a href="https://chat.qwen.ai/" target="_blank" style="margin: 2px;">
-    <img alt="Chat" src="https://img.shields.io/badge/%F0%9F%92%9C%EF%B8%8F%20Qwen%20Chat%20-536af5" style="display: inline-block; vertical-align: middle;"/>
-</a>
+# 🧩 ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization
 
-## Qwen3 Highlights
+<a href="https://arxiv.org/pdf/2510.24592"><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>
 
-Qwen3 is the latest generation of large language models in Qwen series, offering a comprehensive suite of dense and mixture-of-experts (MoE) models. Built upon extensive training, Qwen3 delivers groundbreaking advancements in reasoning, instruction-following, agent capabilities, and multilingual support, with the following key features:
+</div>
 
-- **Uniquely support of seamless switching between thinking mode** (for complex logical reasoning, math, and coding) and **non-thinking mode** (for efficient, general-purpose dialogue) **within single model**, ensuring optimal performance across various scenarios.
-- **Significantly enhancement in its reasoning capabilities**, surpassing previous QwQ (in thinking mode) and Qwen2.5 instruct models (in non-thinking mode) on mathematics, code generation, and commonsense logical reasoning.
-- **Superior human preference alignment**, excelling in creative writing, role-playing, multi-turn dialogues, and instruction following, to deliver a more natural, engaging, and immersive conversational experience.
-- **Expertise in agent capabilities**, enabling precise integration with external tools in both thinking and unthinking modes and achieving leading performance among open-source models in complex agent-based tasks.
-- **Support of 100+ languages and dialects** with strong capabilities for **multilingual instruction following** and **translation**.
+**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.
 
-## Model Overview
-
-**Qwen3-32B** has the following features:
-- Type: Causal Language Models
-- Training Stage: Pretraining & Post-training
-- Number of Parameters: 32.8B
-- Number of Paramaters (Non-Embedding): 31.2B
-- Number of Layers: 64
-- Number of Attention Heads (GQA): 64 for Q and 8 for KV
-- Context Length: 32,768 natively and [131,072 tokens with YaRN](#processing-long-texts). 
-
-For more details, including benchmark evaluation, hardware requirements, and inference performance, please refer to our [blog](https://qwenlm.github.io/blog/qwen3/), [GitHub](https://github.com/QwenLM/Qwen3), and [Documentation](https://qwen.readthedocs.io/en/latest/).
-
-## Quickstart
-
-The code of Qwen3 has been in the latest Hugging Face `transformers` and we advise you to use the latest version of `transformers`.
-
-With `transformers<4.51.0`, you will encounter the following error:
-```
-KeyError: 'qwen3'
-```
-
-The following contains a code snippet illustrating how to use the model generate content based on given inputs. 
-```python
-from transformers import AutoModelForCausalLM, AutoTokenizer
-
-model_name = "Qwen/Qwen3-32B"
-
-# load the tokenizer and the model
-tokenizer = AutoTokenizer.from_pretrained(model_name)
-model = AutoModelForCausalLM.from_pretrained(
-    model_name,
-    torch_dtype="auto",
-    device_map="auto"
-)
-
-# prepare the model input
-prompt = "Give me a short introduction to large language model."
-messages = [
-    {"role": "user", "content": prompt}
-]
-text = tokenizer.apply_chat_template(
-    messages,
-    tokenize=False,
-    add_generation_prompt=True,
-    enable_thinking=True # Switches between thinking and non-thinking modes. Default is True.
-)
-model_inputs = tokenizer([text], return_tensors="pt").to(model.device)
-
-# conduct text completion
-generated_ids = model.generate(
-    **model_inputs,
-    max_new_tokens=32768
-)
-output_ids = generated_ids[0][len(model_inputs.input_ids[0]):].tolist() 
-
-# parsing thinking content
-try:
-    # rindex finding 151668 (</think>)
-    index = len(output_ids) - output_ids[::-1].index(151668)
-except ValueError:
-    index = 0
-
-thinking_content = tokenizer.decode(output_ids[:index], skip_special_tokens=True).strip("\n")
-content = tokenizer.decode(output_ids[index:], skip_special_tokens=True).strip("\n")
-
-print("thinking content:", thinking_content)
-print("content:", content)
-```
-
-For deployment, you can use `sglang>=0.4.6.post1` or `vllm>=0.8.5` or to create an OpenAI-compatible API endpoint:
-- SGLang:
-    ```shell
-    python -m sglang.launch_server --model-path Qwen/Qwen3-32B --reasoning-parser qwen3
-    ```
-- vLLM:
-    ```shell
-    vllm serve Qwen/Qwen3-32B --enable-reasoning --reasoning-parser deepseek_r1
-    ```
-
-For local use, applications such as Ollama, LMStudio, MLX-LM, llama.cpp, and KTransformers have also supported Qwen3.
-
-## Switching Between Thinking and Non-Thinking Mode
-
-> [!TIP]
-> The `enable_thinking` switch is also available in APIs created by SGLang and vLLM. 
-> Please refer to our documentation for [SGLang](https://qwen.readthedocs.io/en/latest/deployment/sglang.html#thinking-non-thinking-modes) and [vLLM](https://qwen.readthedocs.io/en/latest/deployment/vllm.html#thinking-non-thinking-modes) users.
-
-### `enable_thinking=True`
-
-By default, Qwen3 has thinking capabilities enabled, similar to QwQ-32B. This means the model will use its reasoning abilities to enhance the quality of generated responses. For example, when explicitly setting `enable_thinking=True` or leaving it as the default value in `tokenizer.apply_chat_template`, the model will engage its thinking mode.
-
-```python
-text = tokenizer.apply_chat_template(
-    messages,
-    tokenize=False,
-    add_generation_prompt=True,
-    enable_thinking=True  # True is the default value for enable_thinking
-)
-```
-
-In this mode, the model will generate think content wrapped in a `<think>...</think>` block, followed by the final response.
-
-> [!NOTE]
-> For thinking mode, use `Temperature=0.6`, `TopP=0.95`, `TopK=20`, and `MinP=0` (the default setting in `generation_config.json`). **DO NOT use greedy decoding**, as it can lead to performance degradation and endless repetitions. For more detailed guidance, please refer to the [Best Practices](#best-practices) section.
-
-
-### `enable_thinking=False`
-
-We provide a hard switch to strictly disable the model's thinking behavior, aligning its functionality with the previous Qwen2.5-Instruct models. This mode is particularly useful in scenarios where disabling thinking is essential for enhancing efficiency.
-
-```python
-text = tokenizer.apply_chat_template(
-    messages,
-    tokenize=False,
-    add_generation_prompt=True,
-    enable_thinking=False  # Setting enable_thinking=False disables thinking mode
-)
-```
-
-In this mode, the model will not generate any think content and will not include a `<think>...</think>` block.
-
-> [!NOTE]
-> For non-thinking mode, we suggest using `Temperature=0.7`, `TopP=0.8`, `TopK=20`, and `MinP=0`. For more detailed guidance, please refer to the [Best Practices](#best-practices) section.
-
-### Advanced Usage: Switching Between Thinking and Non-Thinking Modes via User Input
-
-We provide a soft switch mechanism that allows users to dynamically control the model's behavior when `enable_thinking=True`. Specifically, you can add `/think` and `/no_think` to user prompts or system messages to switch the model's thinking mode from turn to turn. The model will follow the most recent instruction in multi-turn conversations.
-
-Here is an example of a multi-turn conversation:
-
-```python
-from transformers import AutoModelForCausalLM, AutoTokenizer
-
-class QwenChatbot:
-    def __init__(self, model_name="Qwen/Qwen3-32B"):
-        self.tokenizer = AutoTokenizer.from_pretrained(model_name)
-        self.model = AutoModelForCausalLM.from_pretrained(model_name)
-        self.history = []
-
-    def generate_response(self, user_input):
-        messages = self.history + [{"role": "user", "content": user_input}]
-
-        text = self.tokenizer.apply_chat_template(
-            messages,
-            tokenize=False,
-            add_generation_prompt=True
-        )
-
-        inputs = self.tokenizer(text, return_tensors="pt")
-        response_ids = self.model.generate(**inputs, max_new_tokens=32768)[0][len(inputs.input_ids[0]):].tolist()
-        response = self.tokenizer.decode(response_ids, skip_special_tokens=True)
-
-        # Update history
-        self.history.append({"role": "user", "content": user_input})
-        self.history.append({"role": "assistant", "content": response})
+---
 
-        return response
+## 🚀 Highlights
 
-# Example Usage
-if __name__ == "__main__":
-    chatbot = QwenChatbot()
+- 🪞 **Reflective Autoformalization Paradigm**  
+  Turns single-pass translation into an iterative “generate–validate–refine” cycle, allowing the model to autonomously detect and correct semantic errors.
 
-    # First input (without /think or /no_think tags, thinking mode is enabled by default)
-    user_input_1 = "How many r's in strawberries?"
-    print(f"User: {user_input_1}")
-    response_1 = chatbot.generate_response(user_input_1)
-    print(f"Bot: {response_1}")
-    print("----------------------")
+- ⚖️ **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.
 
-    # Second input with /no_think
-    user_input_2 = "Then, how many r's in blueberries? /no_think"
-    print(f"User: {user_input_2}")
-    response_2 = chatbot.generate_response(user_input_2)
-    print(f"Bot: {response_2}") 
-    print("----------------------")
+- 📈 **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).
 
-    # Third input with /think
-    user_input_3 = "Really? /think"
-    print(f"User: {user_input_3}")
-    response_3 = chatbot.generate_response(user_input_3)
-    print(f"Bot: {response_3}")
-```
+---
 
-> [!NOTE]
-> For API compatibility, when `enable_thinking=True`, regardless of whether the user uses `/think` or `/no_think`, the model will always output a block wrapped in `<think>...</think>`. However, the content inside this block may be empty if thinking is disabled.
-> When `enable_thinking=False`, the soft switches are not valid. Regardless of any `/think` or `/no_think` tags input by the user, the model will not generate think content and will not include a `<think>...</think>` block.
+<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>
 
-## Agentic Use
+---
 
-Qwen3 excels in tool calling capabilities. We recommend using [Qwen-Agent](https://github.com/QwenLM/Qwen-Agent) to make the best use of agentic ability of Qwen3. Qwen-Agent encapsulates tool-calling templates and tool-calling parsers internally, greatly reducing coding complexity.
+## 💡 Quick Start
 
-To define the available tools, you can use the MCP configuration file, use the integrated tool of Qwen-Agent, or integrate other tools by yourself.
 ```python
-from qwen_agent.agents import Assistant
-
-# Define LLM
-llm_cfg = {
-    'model': 'Qwen3-32B',
-
-    # Use the endpoint provided by Alibaba Model Studio:
-    # 'model_type': 'qwen_dashscope',
-    # 'api_key': os.getenv('DASHSCOPE_API_KEY'),
-
-    # Use a custom endpoint compatible with OpenAI API:
-    'model_server': 'http://localhost:8000/v1',  # api_base
-    'api_key': 'EMPTY',
-
-    # Other parameters:
-    # 'generate_cfg': {
-    #         # Add: When the response content is `<think>this is the thought</think>this is the answer;
-    #         # Do not add: When the response has been separated by reasoning_content and content.
-    #         'thought_in_content': True,
-    #     },
-}
+from transformers import AutoTokenizer, AutoModelForCausalLM
 
-# Define Tools
-tools = [
-    {'mcpServers': {  # You can specify the MCP configuration file
-            'time': {
-                'command': 'uvx',
-                'args': ['mcp-server-time', '--local-timezone=Asia/Shanghai']
-            },
-            "fetch": {
-                "command": "uvx",
-                "args": ["mcp-server-fetch"]
-            }
-        }
-    },
-  'code_interpreter',  # Built-in tools
-]
+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")
 
-# Define Agent
-bot = Assistant(llm=llm_cfg, function_list=tools)
+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.$"
 
-# Streaming generation
-messages = [{'role': 'user', 'content': 'https://qwenlm.github.io/blog/ Introduce the latest developments of Qwen'}]
-for responses in bot.run(messages=messages):
-    pass
-print(responses)
+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))
 ```
 
-## Processing Long Texts
-
-Qwen3 natively supports context lengths of up to 32,768 tokens. For conversations where the total length (including both input and output) significantly exceeds this limit, we recommend using RoPE scaling techniques to handle long texts effectively. We have validated the model's performance on context lengths of up to 131,072 tokens using the [YaRN](https://arxiv.org/abs/2309.00071) method.
-
-YaRN is currently supported by several inference frameworks, e.g., `transformers` and `llama.cpp` for local use, `vllm` and `sglang` for deployment. In general, there are two approaches to enabling YaRN for supported frameworks:
-
-- Modifying the model files:
-  In the `config.json` file, add the `rope_scaling` fields:
-    ```json
-    {
-        ...,
-        "rope_scaling": {
-            "rope_type": "yarn",
-            "factor": 4.0,
-            "original_max_position_embeddings": 32768
-        }
-    }
-    ```
-  For `llama.cpp`, you need to regenerate the GGUF file after the modification.
-
-- Passing command line arguments:
-
-  For `vllm`, you can use
-    ```shell
-    vllm serve ... --rope-scaling '{"rope_type":"yarn","factor":4.0,"original_max_position_embeddings":32768}' --max-model-len 131072  
-    ```
-
-  For `sglang`, you can use
-    ```shell
-    python -m sglang.launch_server ... --json-model-override-args '{"rope_scaling":{"rope_type":"yarn","factor":4.0,"original_max_position_embeddings":32768}}'
-    ```
-
-  For `llama-server` from `llama.cpp`, you can use
-    ```shell
-    llama-server ... --rope-scaling yarn --rope-scale 4 --yarn-orig-ctx 32768
-    ```
-
-> [!IMPORTANT]
-> If you encounter the following warning
-> ```
-> Unrecognized keys in `rope_scaling` for 'rope_type'='yarn': {'original_max_position_embeddings'}
-> ```
-> please upgrade `transformers>=4.51.0`.
 
-> [!NOTE]
-> All the notable open-source frameworks implement static YaRN, which means the scaling factor remains constant regardless of input length, **potentially impacting performance on shorter texts.**
-> We advise adding the `rope_scaling` configuration only when processing long contexts is required. 
-> It is also recommended to modify the `factor` as needed. For example, if the typical context length for your application is 65,536 tokens, it would be better to set `factor` as 2.0. 
+More Details please refer to our [Github Repo](https://github.com/Chen-GX/ReForm).
 
-> [!NOTE]
-> The default `max_position_embeddings` in `config.json` is set to 40,960. This allocation includes reserving 32,768 tokens for outputs and 8,192 tokens for typical prompts, which is sufficient for most scenarios involving short text processing. If the average context length does not exceed 32,768 tokens, we do not recommend enabling YaRN in this scenario, as it may potentially degrade model performance.
+# 📚 Citation
 
-> [!TIP]
-> The endpoint provided by Alibaba Model Studio supports dynamic YaRN by default and no extra configuration is needed.
+If you find ReForm useful for your research, please cite:
 
-## Best Practices
-
-To achieve optimal performance, we recommend the following settings:
-
-1. **Sampling Parameters**:
-   - For thinking mode (`enable_thinking=True`), use `Temperature=0.6`, `TopP=0.95`, `TopK=20`, and `MinP=0`. **DO NOT use greedy decoding**, as it can lead to performance degradation and endless repetitions.
-   - For non-thinking mode (`enable_thinking=False`), we suggest using `Temperature=0.7`, `TopP=0.8`, `TopK=20`, and `MinP=0`.
-   - For supported frameworks, you can adjust the `presence_penalty` parameter between 0 and 2 to reduce endless repetitions. However, using a higher value may occasionally result in language mixing and a slight decrease in model performance.
-
-2. **Adequate Output Length**: We recommend using an output length of 32,768 tokens for most queries. For benchmarking on highly complex problems, such as those found in math and programming competitions, we suggest setting the max output length to 38,912 tokens. This provides the model with sufficient space to generate detailed and comprehensive responses, thereby enhancing its overall performance.
-
-3. **Standardize Output Format**: We recommend using prompts to standardize model outputs when benchmarking.
-   - **Math Problems**: Include "Please reason step by step, and put your final answer within \boxed{}." in the prompt.
-   - **Multiple-Choice Questions**: Add the following JSON structure to the prompt to standardize responses: "Please show your choice in the `answer` field with only the choice letter, e.g., `"answer": "C"`."
-
-4. **No Thinking Content in History**: In multi-turn conversations, the historical model output should only include the final output part and does not need to include the thinking content. It is implemented in the provided chat template in Jinja2. However, for frameworks that do not directly use the Jinja2 chat template, it is up to the developers to ensure that the best practice is followed.
-
-### Citation
-
-If you find our work helpful, feel free to give us a cite.
-
-```
-@misc{qwen3technicalreport,
-      title={Qwen3 Technical Report}, 
-      author={Qwen Team},
+```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={2505.09388},
+      eprint={2510.24592},
       archivePrefix={arXiv},
       primaryClass={cs.CL},
-      url={https://arxiv.org/abs/2505.09388}, 
+      url={https://arxiv.org/abs/2510.24592}, 
 }
 ```