Автор: Денис Аветисян
Новая система InternGeometry демонстрирует успехи в решении сложных геометрических задач, приближаясь к уровню олимпиадных чемпионов.
Разработанный агент сочетает в себе обучение с подкреплением, символьный движок и методику повышения сложности для достижения высокого уровня в интерактивном доказательстве теорем.
Несмотря на успехи больших языковых моделей в решении математических задач, автоматическое доказательство геометрических теорем олимпиадного уровня остается сложной задачей, требующей продвинутых эвристик. В работе ‘Achieving Olympia-Level Geometry Large Language Model Agent via Complexity Boosting Reinforcement Learning’ представлен InternGeometry — агент на базе LLM, достигающий уровня медалистов на Международной математической олимпиаде благодаря итеративному построению вспомогательных построений, верификации с помощью символьного движка и обучению с усилением, основанному на постепенном увеличении сложности задач. InternGeometry решает 44 из 50 задач (2000-2024 гг.) с использованием всего 13 тысяч примеров, что значительно меньше, чем у существующих систем, и даже способен предлагать новые подходы к решению. Возможно ли создание полностью автономных систем доказательства теорем, способных не только решать, но и открывать новые математические истины?
В поисках геометрической истины: вызов автоматизированного доказательства
Автоматизированное доказательство теорем, особенно в геометрии, требует выполнения сложной цепи логических выводов, охватывающей множество последовательных шагов. В отличие от задач, требующих единого вычисления, геометрические доказательства часто подразумевают построение сложных аргументов, где каждый вывод зависит от предыдущих, и где необходимо учитывать различные конфигурации и случаи. Такой процесс требует не просто манипулирования символами или числами, но и понимания геометрических принципов, а также способности адаптироваться к изменяющимся условиям. Например, доказательство теоремы о пересечении медиан может потребовать рассмотрения различных треугольников и использования аксиом геометрии, таких как равенство углов или сторон, для установления необходимой связи. Сложность заключается не только в количестве шагов, но и в необходимости выбора правильной стратегии доказательства из множества возможных путей, что делает задачу особенно трудной для современных систем искусственного интеллекта.
Традиционные методы автоматического доказательства теорем в геометрии сталкиваются с серьезной проблемой — комбинаторным взрывом. Даже в задачах умеренной сложности, количество возможных вариантов развития рассуждений и проверок быстро растет экспоненциально. Например, при анализе пересечения нескольких линий или окружностей, число потенциальных точек и отрезков, которые необходимо рассмотреть, может достигать огромных значений. Это приводит к тому, что алгоритмы, работающие последовательным перебором, становятся непрактичными, требуя неприемлемо больших вычислительных ресурсов и времени. Попытки оптимизации путем применения эвристик и сокращений часто оказываются недостаточными для решения задач, требующих глубокого и многошагового логического вывода, особенно в контексте соревнований, таких как Международная Математическая Олимпиада, где требуется не только найти решение, но и сделать это эффективно.
Решение геометрических задач олимпиадного уровня, таких как те, что встречаются на Международной математической олимпиаде (IMO), представляет собой сложную задачу для современных систем искусственного интеллекта. Эти задачи требуют не просто применения известных теорем и формул, но и глубокого дедуктивного мышления, способности выявлять скрытые связи и строить сложные логические цепочки доказательств. В отличие от задач, решаемых с помощью численных методов или шаблонного поиска, олимпиадная геометрия требует понимания геометрических принципов и умения применять их в нестандартных ситуациях. Автоматизация этого процесса сталкивается с трудностями, связанными с необходимостью эффективного перебора возможных стратегий доказательства и избежания ложных путей, что требует разработки принципиально новых алгоритмов и методов представления геометрических знаний. Успешное решение подобных задач демонстрирует не просто вычислительную мощность, а подлинный интеллект, способный к абстрактному мышлению и творческому решению проблем.
InternGeometry: LLM-агент для геометрических доказательств
InternGeometry представляет собой агента на основе большой языковой модели (LLM), использующего возможности InternThinker-32B для решения сложных геометрических задач. В его архитектуре LLM выступает в качестве основного решателя, способного анализировать геометрические условия, разрабатывать стратегии доказательства и генерировать последовательность логических шагов. InternThinker-32B, будучи моделью с 32 миллиардами параметров, обеспечивает достаточную вычислительную мощность и способность к рассуждениям, необходимые для обработки сложных геометрических конструкций и выполнения необходимых вычислений, таких как определение длин отрезков, углов и площадей, для построения корректных доказательств. Агент предназначен для автоматизации процесса решения геометрических задач, представляя собой инструмент для проверки и генерации геометрических доказательств.
В процессе решения геометрических задач агент InternGeometry активно использует метод вспомогательного построения, являющийся фундаментальной техникой в геометрии. Этот метод заключается в добавлении к исходной фигуре дополнительных элементов — точек, прямых, окружностей и т.д. — с целью упрощения анализа и выявления скрытых связей между элементами. Вспомогательное построение позволяет трансформировать сложную задачу в более простую, используя известные геометрические теоремы и аксиомы, например, построение параллельных или перпендикулярных линий, или проведение биссектрис и медиан, что существенно облегчает поиск решения и построение строгого, пошагового доказательства. Использование этого метода позволяет агенту эффективно справляться с задачами, требующими нестандартного подхода и анализа сложных геометрических конфигураций.
В отличие от систем, основанных на простом поиске или угадывании решений, InternGeometry строит строгие, пошаговые доказательства геометрических задач. Процесс доказательства включает в себя последовательное применение аксиом, теорем и логических выводов для перехода от заданных условий к конечному утверждению. Агент стремится к формальной корректности, то есть каждое утверждение в доказательстве должно быть обосновано и вытекать из предыдущих шагов или известных геометрических принципов. Это обеспечивает верифицируемость и надежность полученного решения, в отличие от систем, выдающих ответ без объяснения процесса его получения или с неполной логической цепочкой.
InternGeometry-DDAR: Двигатель дедуктивной верификации
InternGeometry-DDAR выполняет роль движка верификации, обеспечивая логическую корректность каждого вывода, сделанного агентом. В процессе работы система проверяет последовательность шагов, гарантируя, что каждый вывод является логическим следствием исходных посылок и ранее установленных фактов. Это достигается путем формального представления геометрических утверждений и применения правил логического вывода для подтверждения их истинности. В случае обнаружения логической ошибки или противоречия, система сигнализирует о невозможности дальнейшего вывода, предотвращая распространение некорректной информации и обеспечивая надежность принимаемых решений.
InternGeometry-DDAR использует возможности открытого программного обеспечения Newclid, реализуя методы дедуктивных баз данных и исключения Гаусса для обеспечения строгой аналитической точности. Дедуктивные базы данных позволяют системе формально представлять геометрические аксиомы и правила, а затем применять их для вывода новых фактов. Исключение Гаусса, как метод решения систем линейных уравнений, применяется для вычисления неизвестных длин, углов и соотношений, возникающих в процессе геометрических доказательств. Данный подход позволяет проводить верификацию каждого шага доказательства и гарантирует логическую корректность получаемых результатов, используя математический аппарат для строгого анализа геометрических отношений, например, решение системы уравнений вида $Ax = b$ для определения координат точек или длин отрезков.
Система InternGeometry-DDAR обеспечивает последовательное расширение исходных посылок и отслеживание углов, длин и отношений между ними. Этот процесс осуществляется путем применения правил дедукции к известным фактам, что позволяет агенту выводить новые утверждения на основе существующих. Отслеживание включает в себя применение математических операций, таких как вычисление $sin$, $cos$ и пропорциональных соотношений, для установления зависимостей между геометрическими элементами. В конечном итоге, система стремится к достижению доказанного заключения, которое логически следует из начальных посылок и промежуточных выводов.
Усиление производительности посредством обучения с подкреплением Complexity Boosting
Для обучения InternGeometry используется метод обучения с подкреплением Complexity Boosting (CBRL), который предполагает последовательное усложнение задач. Изначально агент тренируется на простых геометрических задачах, а по мере улучшения его производительности, сложность генерируемых проблем увеличивается. Такой подход позволяет агенту постепенно осваивать необходимые навыки решения геометрических задач, избегая ситуаций, когда агент сталкивается со слишком сложными задачами на ранних этапах обучения. CBRL обеспечивает контролируемое обучение, фокусируясь на постепенном наращивании компетенций агента и повышении его способности к решению более сложных задач, что способствует достижению высокой производительности.
Для целенаправленного развития навыков решения геометрических задач используется конвейер синтеза данных Complexity Boosting Reinforcement Learning (CBRL). Данный конвейер генерирует синтетические задачи по геометрии с контролируемым уровнем сложности, позволяя постепенно усложнять обучение агента. Уровень сложности определяется параметрами, такими как количество элементов, сложность логических зависимостей между ними и требуемое количество шагов для доказательства. Это позволяет агенту осваивать базовые навыки решения задач, прежде чем переходить к более сложным конфигурациям, обеспечивая эффективное и последовательное обучение.
Эффективность обучения агента InternGeometry обеспечивается тщательно разработанной функцией вознаграждения. Вознаграждение начисляется за каждый корректный логический вывод, сделанный в процессе решения геометрической задачи, и увеличивается по мере продвижения к полному доказательству. Численное значение вознаграждения пропорционально сложности сделанного вывода и его вкладу в завершение доказательства. Отсутствие вознаграждения за неверные шаги или неполные доказательства способствует обучению агента избегать ошибок и стремиться к полным и обоснованным решениям. Структура функции вознаграждения также учитывает $n$ — количество шагов в доказательстве, стимулируя агента находить наиболее оптимальные и лаконичные решения.
За горизонтом текущих методов: путь к продвинутым рассуждениям
Исследование демонстрирует, что InternGeometry достигает производительности, сравнимой и превосходящей передовые методы, такие как AlphaGeometry и SeedGeometry. В ходе тестирования система успешно решила 44 из 50 задач Международной математической олимпиады (IMO), что превышает средний балл золотых медалистов, составляющий 40.9. Этот результат подчеркивает значительный прогресс в области искусственного интеллекта, способного к сложным геометрическим рассуждениям, и свидетельствует о потенциале InternGeometry как нового эталона в данной области. Превосходство над существующими системами подтверждает эффективность предложенного подхода и открывает перспективы для дальнейшего развития интеллектуальных агентов, способных решать задачи, требующие глубокого логического анализа и творческого подхода.
Исследовательская работа продемонстрировала выдающиеся результаты в решении сложных геометрических задач, представленных на Международной математической олимпиаде (IMO). Система InternGeometry успешно решила 44 из 50 задач олимпиады, что превзошло средний балл золотых медалистов, составляющий 40.9. Этот показатель свидетельствует о значительном прогрессе в области искусственного интеллекта и его способности к решению задач, требующих высокого уровня абстрактного мышления и логических рассуждений. Достижение указывает на потенциал системы не только в математике, но и в других областях, требующих сложных аналитических способностей.
Исследование продемонстрировало, что InternGeometry превосходит существующие системы решения геометрических задач, такие как AlphaGeometry2 и SeedGeometry, подтверждая тем самым свой более высокий уровень рассуждений. В ходе тестирования, агент InternGeometry успешно решил 44 из 50 задач Международной математической олимпиады (IMO), что превышает средний балл золотых медалистов, составляющий 40.9. Этот результат указывает на способность системы не просто воспроизводить известные решения, но и применять логические умозаключения для преодоления сложных геометрических задач, что делает InternGeometry перспективным шагом к созданию универсальных систем искусственного интеллекта, способных решать широкий спектр задач, выходящих за рамки математики.
Примечательно, что InternGeometry достигла выдающихся результатов, требуя значительно меньшего объема обучающих данных. Для достижения сопоставимой и превосходящей производительности, система использовала всего 13 тысяч примеров, что составляет лишь 0,004% от объема данных, использованных AlphaGeometry2, и 0,006% от объема данных SeedGeometry. Этот факт подчеркивает эффективность разработанного подхода к обучению и указывает на потенциал для создания более экономичных и масштабируемых систем искусственного интеллекта, способных к сложным рассуждениям. Способность InternGeometry к эффективному обучению с ограниченным количеством данных открывает новые возможности для применения в областях, где сбор больших объемов размеченных данных затруднен или невозможен.
Способность агента поддерживать длительное взаимодействие, обеспечиваемая динамической памятью, оказалась ключевым фактором в решении сложных задач. В отличие от традиционных подходов, где информация быстро теряется при обработке сложных проблем, InternGeometry использует механизм динамической памяти для сохранения и использования контекста на протяжении всего процесса рассуждения. Это позволяет агенту учитывать предыдущие шаги и выводы, эффективно строить логические цепочки и избегать тупиковых ситуаций. Подобный подход к организации информации, напоминающий человеческое мышление, позволил InternGeometry успешно справляться с задачами, требующими многоступенчатых рассуждений и учета большого объема данных, значительно превосходя результаты, достигнутые другими современными системами искусственного интеллекта в области геометрии.
Данная работа представляет собой значительный шаг вперед в создании универсальных систем рассуждений, способных решать задачи не только в математике, но и в других областях знаний. Достижения, продемонстрированные InternGeometry, указывают на возможность построения искусственного интеллекта, превосходящего существующие модели в сложности решаемых задач и эффективности использования данных. Способность агента к долгосрочному взаимодействию и динамическому управлению памятью открывает перспективы для разработки систем, способных к глубокому анализу и поиску решений в самых разнообразных областях, от научных исследований до инженерного проектирования и решения сложных практических задач. Результаты подтверждают, что создание систем, способных к обобщению знаний и адаптации к новым условиям, — вполне достижимая цель, и InternGeometry является важным шагом на пути к созданию искусственного интеллекта общего назначения.
Исследование, представленное в данной работе, демонстрирует, как InternGeometry, опираясь на обучение с подкреплением и симбиоз с символьными движками, достигает впечатляющих результатов в решении геометрических задач. Подобный подход напоминает о неизбежности сложности в любой системе. Бертранд Рассел некогда заметил: «Чем больше я узнаю, тем больше я понимаю, что ничего не знаю». Эта мудрость перекликается с концепцией complexity boosting, где каждый шаг к решению, каждая новая архитектурная деталь, одновременно открывает новые возможности и порождает новые потенциальные точки отказа. В конечном счете, порядок, созданный InternGeometry, — это лишь временный кэш между неизбежными сбоями, закономерность, присущая любой развивающейся экосистеме.
Куда же дальше?
Представленная работа, словно росток, пробившийся сквозь гранит формальной логики, демонстрирует потенциал LLM-агентов в решении задач, требующих не просто знаний, но и последовательного, многошагового рассуждения. Однако, не стоит обольщаться иллюзией «достижения олимпийского уровня». Каждый успешно доказанный признак — лишь временное затишье перед неизбежным проявлением скрытых слабостей архитектуры. Ведь система — не инструмент, а экосистема, и её устойчивость определяется не количеством решенных задач, а способностью адаптироваться к новым, неожиданным вызовам.
Настоящая работа открывает путь к исследованию не просто более сложных теорем, но и к пониманию границ применимости подобных систем. Следующим этапом, вероятно, станет не увеличение вычислительных мощностей или усложнение алгоритмов обучения, а поиск способов интеграции с другими, принципиально иными подходами к решению задач. Символьные движки и LLM — лишь два полюса одного целого. Истинный прогресс наступит, когда удастся создать систему, способную органично объединить сильные стороны обоих подходов.
Не стоит забывать и о том, что каждая попытка рефакторинга начинается как молитва и заканчивается покаянием. Чем сложнее система, тем больше вероятность возникновения непредсказуемых ошибок. И когда система снова даст сбой, не стоит искать виноватых. Она просто взрослеет.
Оригинал статьи: https://arxiv.org/pdf/2512.10534.pdf
Связаться с автором: https://www.linkedin.com/in/avetisyan/
Смотрите также:
- LLM: математика — предел возможностей.
- Квантовые схемы без лишних шагов: обучение с подкреплением для оптимизации вычислений
- Квантовый горизонт: Облачные вычисления нового поколения
- Восполняя пробелы в знаниях: Как языковые модели учатся делать выводы
- Вариационные и полувариационные неравенства: от теории к практике
- Точность фазовой оценки: адаптивный подход превосходит стандартный
- Модель Motif 2 12.7B: Новый взгляд на эффективные языковые модели
- Взгляд в будущее видео: ускорение генерации с помощью LiteAttention
- Квантовый прыжок в будущее: юмористический взгляд на недавние квантовые приключения!
- Уменьшение глубины квантовых схем: новый путь к устойчивым алгоритмам
2025-12-12 13:47