Abstrações Funcionais Executáveis: Inferindo Programas Gerativos para Problemas Avançados de Matemática

Executable Functional Abstractions: Inferring Generative Programs for Advanced Math Problems

April 14, 2025

Autores: Zaid Khan, Elias Stengel-Eskin, Archiki Prasad, Jaemin Cho, Mohit Bansal

cs.AI

Resumo

Cientistas frequentemente inferem procedimentos abstratos a partir de instâncias específicas de problemas e usam essas abstrações para gerar novas instâncias relacionadas. Por exemplo, programas que codificam as regras e propriedades formais de um sistema têm sido úteis em áreas que vão desde RL (ambientes procedurais) até física (motores de simulação). Esses programas podem ser vistos como funções que executam para diferentes saídas com base em suas parametrizações (por exemplo, configuração de gridworld ou condições físicas iniciais). Introduzimos o termo EFA (Abstração Funcional Executável) para denotar tais programas para problemas matemáticos. Construções semelhantes a EFAs têm se mostrado úteis para raciocínio matemático como geradores de problemas para testar modelos. No entanto, trabalhos anteriores se limitaram a abstrações para matemática do ensino fundamental (cujas regras simples são fáceis de codificar em programas), enquanto a geração de EFAs para matemática avançada até agora exigiu engenharia humana. Exploramos a construção automática de EFAs para problemas matemáticos avançados. Operacionalizamos a tarefa de construir EFAs automaticamente como uma tarefa de síntese de programas e desenvolvemos o EFAGen, que condiciona um LLM em um problema matemático inicial e sua solução passo a passo para gerar programas EFA candidatos que são fiéis ao problema generalizado e à classe de solução subjacente ao problema inicial. Além disso, formalizamos propriedades que qualquer EFA válido deve possuir em termos de testes unitários executáveis e mostramos como os testes podem ser usados como recompensas verificáveis para treinar LLMs a se tornarem melhores escritores de EFAs. Demonstramos que EFAs construídos pelo EFAGen se comportam racionalmente ao permanecerem fiéis aos problemas iniciais, produzem variações de problemas aprendíveis e que o EFAGen pode inferir EFAs em múltiplas fontes diversas de problemas matemáticos de nível competitivo. Por fim, mostramos usos subsequentes de EFAs escritos por modelos, como encontrar variações de problemas que são mais difíceis ou mais fáceis para um aprendiz resolver, bem como geração de dados.

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.