альфа геометри - решаем егэ по цене репетитора
В чем идея: вообще то есть механические(ака без идейные) способы считать геому. Можно перестроить все в векторный space и вытащить все координаты, а дальше приходит вычмат и считает все.
Авторы с эти особо не спорят, ну решает и решает, численные калькуляторы, так а что это блять такое????
Как решить ((((любую))))) геометрию числено?
Любой учащийся в МАТшколах-тех вузах знает что такое wolfram alpha - это такой тул для решения любого примерно любого матана. Минусы: он очень часто забивает пытаться решать что то аналитически и хуярит какие то фантастические ответы полученные численно. CPU goes brrr, математики не нужны(NO)????
Возьмем для примера спинно мозговое ЕГЭ проверяющее жив ли решающий.
Вообще за последние пару лет вольфрам сильно обновился, там теперь и NLP ввод есть и решения пишутся нормальные(почти всегда)
Как же решается геома? довольно просто
AUTOMATED DEDUCTION IN REAL GEOMETRY(2011)
прикиньте ебала алармистов в 2011 если бы они ну не знаю, не были бы хайпожорами?
Идея такая: любая геометрия задается координатами
А если мы можем задать координаты то мы можем систему уравнений которая задает эту задачу
Собственно дальше идет метод ВУ для решения систем уравнений, он предназначен для ВычМаша, поэтому ну он не оч интуитивный для человека)
Он использует псевдоделение, работает это примерно так:
Этот метод позволит нам упростить систему до приведения ее к треугольному виду который мы можем решить. И да, это может работать ОЧЕНЬ быстро особенно на GPU. условно можно делать 300i t/s и это даже не вставая со стула первая попавшаяся репа.
https://scholarworks.umt.edu/cgi/viewcontent.cgi?article=1034&context=tme
Спойлер: такая схема решает 10/30 задач IMO(в 2006 году)
правда тут есть два нюанса: авторы альфа геометри забивают ссылаться на конкретную кодовую базу, а еще буквально пишут
because these methods often have large time and memory complexity, especially when processing IMO-sized problems, we report their result by assigning success to any problem that can be decided within 48 h using one of their existing implementations17
Я покопался на гите и нашел только https://github.com/jyfliu/Goq
Geometry proofs are very mechanical in nature — they don't require much creativity. The vast majority of geometry problems, even at the Olympiad level, can be solved in the following manner: Construct these templates, apply these 7 theorems in this order, these points lie in the following configuration of which we know this property about, etc. Both humans and computers are not restricted in the techniques they know, but rather by the number of templates and theorems they have memorized. And computers are a lot better at memorization than humans.
Согласен с автором полностью. Возможно перепишу(или кто то из студентов) его кодовую базу на jax и обсудим почему LM не очень то и нужны в вычматах.
Inter-GPS: Interpretable Geometry Problem Solving with Formal Language and Symbolic Reasoning
wait это что, alpha geometry?? из 2021??? и alpha geometry ее не упоминает???
В чем смысл - у нас есть парсер решения в правильный формат(у DeepMind его нет, им похуй они так чувствуют), а затем маленький трансформер придумывает теорему куда подставляются чиселки, а затем машина считает их.
Офк Human baseline тут не бьется(и не может, модель на 12м параметров)
А чо такого сделали deepmind?
Э, навалили компьюта и добавили построитель доп построений(сорри за каламбур) на LM которую обучили на синте.
А что такое Symbolic engine? По сути такой же метод ВУ только сложнее, теперь они используют не просто псевдоделение, но и еще различные геометрические/алгебраические законы и переставляя их продвигается по решению преобразуя их по примерно таким правилам:
К слову с помощью него же и генерируют огромный датасет решенный авторсолвером для обучения LM(100m) и кормят в LM, а затем дотюнивают на 9m cэплов на доп построяниях)))
По сути LM служит как выбор когда строить доп построение, а когда нет для Symbolic engine.
Сама по себе альфа геометри и безе LM показывает неплохие результаты на основе эвристик и symbol engine(cм Without Pretraining)
У авторов очень специфичный сетап для рана, почему то 4v100(почему не 8h100) или их TPU я не знаю, а авторам слегка похуй на обьяснения.
Вывод?
Если очень хочется можно и LM заставить решать IMO(нет, это полный бред, symbolic engines тащат)
