GenesisGeo is a neuro-symbolic system that proves geometry theorems by combining a symbolic deduction engine (DDARN) with a neural language model. It is a full-stack reproduction and extension of AlphaGeometry, built on top of Newclid/DDAR.
Highlights:
- Synthetic data generation pipeline producing 3 million unique geometry problems with proof traces
- Enhanced DDARN engine with 120x speedup over the original implementation
- Neuro-symbolic prover fine-tuned from Qwen3-VL-2B
| Benchmark | Score |
|---|---|
| IMO-AG-30 | 29/30 |
| IMO-95 | 63/95 |
| HAGeo-409 | 278/409 |
git clone https://github.com/ZJUVAI/GenesisGeo.git
cd GenesisGeo
uv venv
source .venv/bin/activate
uv sync --extra fullGenerate synthetic geometry problems with proof traces:
python src/newclid/generation/pipeline.py \
--n_clauses 10 \
--n_samples 1000000 \
--n_threads 20 \
--aux_only 2 \
--seed_cache| Parameter | Default | Description |
|---|---|---|
--n_clauses |
15 |
Max number of construction clauses per problem |
--n_samples |
10000 |
Total number of problems to generate |
--n_threads |
10 |
Number of parallel Ray workers |
--timeout |
3600 |
Per-task timeout in seconds |
--max_level |
500 |
Maximum DDAR search depth |
--base_seed |
42 |
Base random seed for generation |
--log_level |
info |
Logging level (debug, info, warning, error) |
--construction_config |
None |
Path to JSON config for construction sets and sampler steps |
--seed_cache |
off |
Enable seed cache to skip seeds without real auxiliary points |
| Parameter | Default | Description |
|---|---|---|
--add_auxiliary / --no-add_auxiliary |
enabled |
Whether to add auxiliary points during generation |
--max_auxiliary_points |
2 |
Maximum auxiliary points per problem |
--aux_only |
0 |
Data filter: 0 = all, 1 = include non-aux at 0.1 prob, 2 = aux-only |
| Parameter | Default | Description |
|---|---|---|
--dir |
./datasets |
Output directory |
--img |
0 |
Image mode: 0 = none, 1 = annotated only, 2 = plain only, 3 = both |
--direct_png / --no-direct_png |
enabled |
Save PNG directly or keep the legacy svg -> png pipeline |
--img_pixels |
512 |
Output image width in pixels |
--prune / --no-prune |
enabled |
Prune clauses to keep only the deepest clause chain |
--remove_coords |
off |
Remove coordinate information from output |
--clear |
off |
Clear old dataset files before generation |
bash scripts/train_lm.shbash scripts/train_vlm.shNote: Update dataset paths, checkpoint directories, output paths, and
CUDA_VISIBLE_DEVICESin the scripts before running.
Start a vLLM OpenAI-compatible server for the checkpoint first:
python scripts/launch_vllm_server.py \
--model_name /path/to/checkpoint \
--host 127.0.0.1 \
--port 8000 \
--gpu_ids 0,1,2,3python scripts/evaluation.py \
--agent qwen3_text \
--problems_path benchmarks/dev_imo.txt \
--vllm_base_url http://127.0.0.1:8000 \
--think false \
--decoding_size 32 \
--beam_size 512 \
--search_depth 4 \
--ray_num_cpus 40 \
--timeout 3600Use --think true to start the text model with <think> and extract the generated <aux> block instead of forcing the next point name. The VL agent starts directly from <aux> for Qwen3-VL-Instruct checkpoints.
python scripts/evaluation.py \
--agent qwen3_vl \
--problems_path benchmarks/imo_95.txt \
--vllm_base_url http://127.0.0.1:8000 \
--decoding_size 32 \
--beam_size 512 \
--search_depth 4 \
--ray_num_cpus 40 \
--timeout 3600| File | Description |
|---|---|
benchmarks/imo_ag_30.txt |
IMO-AG-30 (30 problems) |
benchmarks/imo_95.txt |
IMO-95 (95 problems) |
benchmarks/hageo_409.txt |
HAGeo-409 (409 problems) |
benchmarks/jgex_ag_231.txt |
JGEX-AG-231 (231 problems) |
benchmarks/dev_imo.txt |
Small IMO development subset |
benchmarks/dev_jgex.txt |
Small JGEX development subset |
benchmarks/examples.txt |
Mixed example and debugging problems |
benchmarks/larger_imo_eval.txt |
Extended IMO-style evaluation set |
benchmarks/testing_minimal_rules.txt |
Minimal regression checks for individual rules |
GenesisGeo/
├── src/newclid/ # Main source code
│ ├── __main__.py # CLI entry point
│ ├── api.py # GeometricSolver interface
│ ├── proof.py # Proof state management
│ ├── agent/ # Reasoning agents
│ │ ├── ddarn.py # DDARN symbolic engine
│ │ ├── base.py # Shared neural-guided search logic
│ │ └── vllm.py # vLLM text and vision-language agents
│ ├── evaluation/ # vLLM evaluation runtime and trace helpers
│ │ ├── search_runtime.py # Search DSL, DDAR tasks, beam utilities
│ │ └── search_trace.py # Evaluation trace recording
│ ├── generation/ # Data generation pipeline
│ │ ├── pipeline.py # ProblemPipeline orchestrator
│ │ ├── sampler.py # Geometry construction sampling
│ │ ├── worker.py # Per-problem processing
│ │ ├── writer.py # Data writing & image rendering
│ │ ├── filter.py # Goal filtering
│ │ ├── point_naming.py # Point naming management
│ │ ├── constructions.py # Construction type constants
│ │ ├── statistics.py # Generation statistics
│ │ └── auxiliary/ # Auxiliary point discovery
│ ├── DDAR/ # C++ symbolic engine
│ ├── dependencies/ # Dependency graph management
│ ├── formulations/ # Problem representations
│ ├── numerical/ # Numerical geometry
│ ├── algebraic_reasoning/ # Algebraic reasoning
│ ├── predicates/ # Geometry predicates
│ └── proof_scout/ # Theorem discovery and rule reduction
├── scripts/ # Training, evaluation, and data utilities
│ ├── train_lm.sh # Text SFT training
│ ├── train_vlm.sh # VLM SFT training
│ ├── launch_vllm_server.py # Managed vLLM gateway launcher
│ └── evaluation.py # vLLM evaluation CLI
├── tests/ # Test suite
├── benchmarks/ # Benchmark problem sets
└── docs/ # Documentation
- AlphaGeometry — the original neuro-symbolic geometry prover
- Newclid — the DDAR symbolic engine
- Qwen — base language models
- ms-swift — training framework
@article{zhu2025genesisgeo,
title={GenesisGeo: Technical Report},
author={Zhu, Minfeng and Wang, Zi and Ji, Sizhe and Du, Zhengtong and Tai, Shengqiang and Ke, Junming and Deng, Xiao and Yin, Zanlang and Huang, Xiuqi and Wang, Heyu and Chen, Wei},
journal={arXiv preprint arXiv:2509.21896},
year={2025}
}