ZJUVAI/GenesisGeo
ZJUVAI/GenesisGeo is a 0.8 billion parameter language model, built upon the Qwen3-0.6B-Base architecture, specialized in automated geometric theorem proving. It is fine-tuned to propose auxiliary constructions for challenging geometry problems, forming the core of the GenesisGeo neuro-symbolic system. Trained on 21.8 million synthetic geometric theorems, it demonstrates strong performance in geometric reasoning tasks, achieving 24/30 problems solved on the IMO-AG-30 benchmark.
Loading preview...
GenesisGeo Model Overview
ZJUVAI/GenesisGeo is a specialized 0.8 billion parameter language model, based on the Qwen3-0.6B-Base architecture, designed for automated geometric theorem proving. Its primary function is to propose auxiliary constructions, which are crucial steps in solving complex geometry problems. This model is a core component of the GenesisGeo neuro-symbolic system, which aims to reproduce the AlphaGeometry framework.
Key Capabilities & Training
- Specialized Geometric Reasoning: Focuses exclusively on generating auxiliary points and constructions for geometric proofs.
- Neuro-Symbolic Integration: Designed to operate within a larger neuro-symbolic reasoning loop, enhancing its problem-solving capacity.
- Large-Scale Synthetic Training: Developed using a massive GenesisGeo Dataset comprising 21.8 million synthetically generated geometric theorems.
Performance
When integrated into the neuro-symbolic system, GenesisGeo demonstrates robust performance:
- IMO-AG-30 Benchmark: Solves 24 out of 30 problems on the challenging IMO-AG-30 benchmark, closely matching the original AlphaGeometry's performance (25/30).
Use Cases
This model is ideal for research and applications requiring advanced geometric reasoning, particularly in automated proof generation and educational tools for geometry.