Исполняемые функциональные абстракции: вывод генеративных программ для сложных математических задач

Executable Functional Abstractions: Inferring Generative Programs for Advanced Math Problems

April 14, 2025

Авторы: Zaid Khan, Elias Stengel-Eskin, Archiki Prasad, Jaemin Cho, Mohit Bansal

cs.AI

Аннотация

Ученые часто выводят абстрактные процедуры из конкретных примеров задач и используют эти абстракции для создания новых, связанных примеров. Например, программы, кодирующие формальные правила и свойства системы, оказались полезными в различных областях — от обучения с подкреплением (процедурные среды) до физики (движки симуляции). Эти программы можно рассматривать как функции, которые выполняются с разными результатами в зависимости от их параметризации (например, конфигурация gridworld или начальные физические условия). Мы вводим термин EFA (Executable Functional Abstraction, Исполняемая Функциональная Абстракция) для обозначения таких программ в контексте математических задач. Конструкции, подобные EFA, уже показали свою полезность для математических рассуждений в качестве генераторов задач для стресс-тестирования моделей. Однако предыдущие работы ограничивались абстракциями для школьной математики (чьи простые правила легко кодировать в программах), тогда как создание EFA для сложной математики до сих пор требовало ручной разработки. Мы исследуем автоматическое создание EFA для сложных математических задач. Мы формулируем задачу автоматического построения EFA как задачу синтеза программ и разрабатываем EFAGen, который использует LLM (языковую модель) для генерации кандидатов в EFA на основе исходной математической задачи и её пошагового решения, сохраняя верность обобщенной задаче и классу решений, лежащих в основе исходной задачи. Кроме того, мы формализуем свойства, которыми должна обладать любая корректная EFA, в виде исполняемых модульных тестов, и показываем, как эти тесты можно использовать в качестве проверяемых наград для обучения LLM, чтобы они лучше писали EFA. Мы демонстрируем, что EFA, созданные EFAGen, ведут себя рационально, оставаясь верными исходным задачам, генерируют вариации задач, пригодные для обучения, и что EFAGen способен выводить EFA из множества разнообразных источников задач уровня математических соревнований. Наконец, мы показываем практическое применение EFA, написанных моделями, например, для поиска вариаций задач, которые сложнее или проще для решения обучающимся, а также для генерации данных.

English

Scientists often infer abstract procedures from specific instances of problems and use the abstractions to generate new, related instances. For example, programs encoding the formal rules and properties of a system have been useful in fields ranging from RL (procedural environments) to physics (simulation engines). These programs can be seen as functions which execute to different outputs based on their parameterizations (e.g., gridworld configuration or initial physical conditions). We introduce the term EFA (Executable Functional Abstraction) to denote such programs for math problems. EFA-like constructs have been shown to be useful for math reasoning as problem generators for stress-testing models. However, prior work has been limited to abstractions for grade-school math (whose simple rules are easy to encode in programs), while generating EFAs for advanced math has thus far required human engineering. We explore the automatic construction of EFAs for advanced math problems. We operationalize the task of automatically constructing EFAs as a program synthesis task, and develop EFAGen, which conditions an LLM on a seed math problem and its step-by-step solution to generate candidate EFA programs that are faithful to the generalized problem and solution class underlying the seed problem. Furthermore, we formalize properties any valid EFA must possess in terms of executable unit tests, and show how the tests can be used as verifiable rewards to train LLMs to become better writers of EFAs. We demonstrate that EFAs constructed by EFAGen behave rationally by remaining faithful to seed problems, produce learnable problem variations, and that EFAGen can infer EFAs across multiple diverse sources of competition-level math problems. Finally, we show downstream uses of model-written EFAs e.g. finding problem variations that are harder or easier for a learner to solve, as well as data generation.