search

FormalGeo / Datasets

Dataset Annotation Tools and Dataset Release for formal Euclidean plane geometry problems.
MIT License
7 stars 3 forks source link

evaluation problems (e.g., value(object)) #1

Open zyh2022github opened 1 month ago

zyh2022github commented 1 month ago

Hello！ I found that almost all Formal7k-v1 problems are evaluation problems (e.g., value(object)), is it because the solver FGPS can only solve evaluation problems

BitSecret commented 2 weeks ago

This is because the data source for formalgeo7k consists entirely of numerical problems. FormalGeo unifies relational and numerical problem-solving goals. You can use "Relation" to represent relational problem-solving goals, such as "Relation(RightTriangle(ABC))".

BitSecret commented 2 weeks ago

We will be open-sourcing the dataset formalgeo7k-v2 soon. This dataset corrects some annotation errors from formalgeo7k-v1 and includes newly annotated images. Based on formalgeo7k-v2, the expanded dataset formalgeo30k balances relational and numerical problem-solving goals.