xiaolesu/Qwen3-8B-Herald-SFT

Model Overview

The xiaolesu/Qwen3-8B-Herald-SFT is an 8 billion parameter QLoRA fine-tuned model based on Qwen/Qwen3-8B, developed by xiaolesu / Osmosis AI. Its core function is natural-language-to-Lean-4 autoformalization (NL→FL), converting natural language mathematical statements into formal Lean 4 theorem stubs. The model was trained on the FrenzyMath/Herald_statements dataset, comprising 50,000 examples.

Key Capabilities

• Lean 4 Autoformalization: Translates English mathematical statements into Lean 4 theorem signatures, including necessary Mathlib imports and sorry placeholders for proofs.
• Structured Output: Generates output in a specific JSON format (#### {"header": ..., "formal_statement": ...}) designed for easy parsing.
• SFT Cold-Start: Serves as a supervised fine-tuning (SFT) checkpoint, intended to initialize a GRPO (Goal-Oriented Reinforcement Learning with Proof Objectives) reinforcement learning phase.

Intended Use Cases

• Direct Use: Automatically generating a corpus of Lean 4 theorem stubs from informal mathematical texts, competition problems, or research papers.
• Downstream Use: Providing a robust starting point for GRPO training, where a Lean 4 compiler can offer binary reward signals based on type-checking the generated formal statements.

Out-of-Scope

This model is not designed for:

• Writing complete Lean 4 proofs (it only generates theorem stubs).
• Informal mathematical reasoning or problem-solving in natural language.
• Working with Lean 3 or other proof assistants (e.g., Coq, Isabelle).
• General-purpose coding tasks.