GenesisGeo-2B
This model is specialized in automated geometric theorem proving, capable of proposing auxiliary constructions to solve challenging geometry problems. It forms the neural component of the GenesisGeo project—a neuro-symbolic system that combines a vision-language model with the DDAR symbolic deduction engine.
It is built upon Qwen3-VL-2B-Instruct and trained on synthetic geometry data for predicting auxiliary constructions from formal problem statements, with or without diagrams.
Model Description
- Architecture: Vision-language model
- Base Model: Qwen3-VL-2B-Instruct
- Training Data: One million synthetic multimodal geometry records for pretraining, followed by auxiliary construction data for supervised fine-tuning
- Training: Pretraining on complete solution records containing formal problems, diagrams, auxiliary constructions, and proof traces; supervised fine-tuning for auxiliary construction prediction with and without diagrams
- Fine-tuning: The vision encoder is frozen, while the language model and visual aligner are trained
- Purpose: Proposing auxiliary constructions in geometric proofs within a neuro-symbolic reasoning loop
Performance
The integrated GenesisGeo neuro-symbolic system achieves the following paper-reported results, also listed in the GitHub README:
| Variant | IMO-30 | IMO-95 | HAGeo-409 |
|---|---|---|---|
| Text | 28/30 | 59/95 | 270/409 |
| Vision + Text | 29/30 | 63/95 | 278/409 |
Paper-reported results with a 32 × 512 × 4 search budget and a 60-minute time limit per problem. These results measure the complete system, including symbolic deduction and proof search.
Usage
Input and output
The model takes a formal geometry problem in the predicate DSL, enclosed in <problem>...</problem>, optionally accompanied by a diagram. It predicts auxiliary constructions in an <aux>...</aux> block.
Use the problem serialization and prompting implemented in the GenesisGeo repository. Generated constructions are checked by the symbolic deduction engine as part of the complete proof-search system.
For proof search and benchmark evaluation, follow the evaluation instructions in the GenesisGeo repository.
License
Apache License 2.0. The model is derived from Qwen3-VL-2B-Instruct.