OpenBMB/MathForm

OpenBMB/MathForm

Language: Python

License: Apache-2.0

Stars: 1

Forks: 0

Open issues: 0

Created: 2026-08-14T02:58:25Z

Pushed: 2026-08-17T05:28:16Z

Default branch: main

Fork: no

Archived: no

README:

Figure 1: Overview of the MathForm data construction and training pipeline. The system combines Mathlib knowledge retrieval, compilation and semantic verification, and iterative refinement to generate reliable formal data, followed by trajectory reconstruction and training of MathForm-8B.

📖 Introduction

We introduce MathForm, an autoformalization framework that combines knowledge retrieval from Mathlib with verification-guided iterative refinement. MathForm retrieves relevant definitions and existing formalizations before generation, then uses compiler diagnostics and semantic-consistency feedback to refine generated Lean statements.

Using this framework, we construct **FormalVerse**, a verified Lean 4 dataset covering diverse mathematical domains and sources. We also train **MathForm-8B** with supervised fine-tuning followed by reinforcement learning using Lean compilation and semantic-consistency feedback. The released code supports the data construction pipeline and autoformalizer evaluation.

Figure 2: Macro-average Pass@8 (%) across FormalMATH-Lite, ProverBench, CombiBench, FATE-M, FATE-H, and FATE-X among specialized autoformalizers. MathForm-8B achieves the strongest overall performance within this category despite its smaller model size.

News

• `[2026.08.17]`: MathForm paper, code, data and model are released. 🔥🔥🔥

📁 Repository Structure

src/ Data construction pipeline
evaluation/ Evaluation pipeline and benchmark files
kimina-lean-server/ Lean compilation server source
assets/ Figures used in this README
requirements.txt Python dependencies

🛠️ Quick Start

Installation

1. Clone the repository:

git clone https://github.com/OpenBMB/MathForm.git
cd MathForm

2. Install the Python dependencies:

pip install -r requirements.txt

The experiments use Lean 4.21.0.

Start Kimina Lean Server

The evaluation and data-construction pipelines require a running Kimina Lean Server for compilation checks.

cd kimina-lean-server
cp .env.template .env
bash setup.sh
pip install -r requirements.txt
pip install .
prisma generate
python -m server

The default endpoint is http://localhost:8000.

Run Data Construction

The input is a JSONL file containing a natural-language statement in a field such as statement or informal_statement.

cd src
API_URL=https://api.example.com/v1/chat/completions \
API_KEY="$API_KEY" \
BASE_MODEL_NAME=[GENERATION_MODEL] \
JUDGE_MODEL_NAME=[JUDGE_MODEL] \
LEAN_SERVER_URL=http://localhost:8000 \
bash run.sh path/to/input.jsonl output/run

Start Lean Explore with run_leanexp_server.sh and add:

LEAN_EXPLORE_URL=http://localhost:9000

The generated files include success.jsonl, failed.jsonl, and pipeline.log. Successful samples can be normalized and filtered with:

python postprocess.py normalize \
--input output/run/success.jsonl \
--output output/run/normalized.jsonl
python postprocess.py filter \
--input output/run/normalized.jsonl \
--output output/run/filtered.jsonl

Run Evaluation

The default evaluation uses the benchmark files under evaluation/benchmarks/.

cd evaluation
EVAL_API_BASE_URL=https://api.example.com/v1 \
EVAL_API_MODEL=[EVALUATION_MODEL] \
JUDGE_API_BASE_URL=https://api.example.com/v1 \
JUDGE_API_MODEL=[JUDGE_MODEL] \
API_KEY="$API_KEY" \
bash run.sh

Results are written to evaluation/output/:

predictions.jsonl Generated Lean candidates
results.jsonl Compilation and judge results
results.compile.jsonl Compilation cache
results.summary.json Pass@k summary

To evaluate another benchmark or change the number of samples, set DATASET_PATHS or NUM_SAMPLES before running run.sh.

🔎 Citation

If you find this repository useful, please cite our paper:

@misc{pu2026mathformscalingmathematicalautoformalization,
title={MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement},
author={Lushi Pu and Weiming Zhang and Xinheng Xie and Zixuan Fu and Bingxiang He and Hengyu Zhao and Hongya Lyu and Xin Li and Jie Zhou and Yudong Wang},
year={2026},
eprint={2608.14221},
archivePrefix={arXiv},
primaryClass={cs.AI},
url={https://arxiv.org/abs/2608.14221},
}

🤝 Acknowledgement

This repository builds on the following open-source projects:

• Kimina Lean Server for Lean compilation checks.
• Lean Explore for retrieval.

The evaluation uses the following benchmarks:

• FormalMATH-Lite
• ProverBench
• CombiBench
• FATE-M
• FATE-H
• FATE-X

Part of the informal problems used to build FormalVerse are drawn from the following open collections:

• Lean-Workbook
• NuminaMath
• DeepMath
• DeepTheorem
• AceReason-Math
• OpenR1-Math
• Principia-Collection

We thank the authors and contributors of these projects.

📜 License

This project is licensed under the Apache License 2.0. The bundled third-party components retain their original license and attribution notices.