Abstracciones Funcionales Ejecutables: Inferencia de Programas Generativos para Problemas Matemáticos Avanzados

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

Resumen

Los científicos a menudo infieren procedimientos abstractos a partir de instancias específicas de problemas y utilizan estas abstracciones para generar nuevas instancias relacionadas. Por ejemplo, los programas que codifican las reglas y propiedades formales de un sistema han sido útiles en campos que van desde el aprendizaje por refuerzo (entornos procedimentales) hasta la física (motores de simulación). Estos programas pueden verse como funciones que se ejecutan para producir diferentes salidas según sus parametrizaciones (por ejemplo, la configuración de un gridworld o las condiciones físicas iniciales). Introducimos el término EFA (Abstracción Funcional Ejecutable) para denotar tales programas en problemas matemáticos. Se ha demostrado que construcciones similares a los EFA son útiles para el razonamiento matemático como generadores de problemas para probar modelos. Sin embargo, trabajos previos se han limitado a abstracciones para matemáticas de nivel escolar (cuyas reglas simples son fáciles de codificar en programas), mientras que la generación de EFAs para matemáticas avanzadas hasta ahora ha requerido ingeniería humana. Exploramos la construcción automática de EFAs para problemas matemáticos avanzados. Operacionalizamos la tarea de construir EFAs automáticamente como una tarea de síntesis de programas y desarrollamos EFAGen, que condiciona un modelo de lenguaje grande (LLM) en un problema matemático inicial y su solución paso a paso para generar programas EFA candidatos que sean fieles al problema generalizado y a la clase de solución subyacente al problema inicial. Además, formalizamos las propiedades que cualquier EFA válido debe poseer en términos de pruebas unitarias ejecutables, y mostramos cómo estas pruebas pueden usarse como recompensas verificables para entrenar LLMs para que se conviertan en mejores escritores de EFAs. Demostramos que los EFAs construidos por EFAGen se comportan de manera racional al mantenerse fieles a los problemas iniciales, producen variaciones de problemas aprendibles, y que EFAGen puede inferir EFAs a partir de múltiples fuentes diversas de problemas matemáticos de nivel competitivo. Finalmente, mostramos usos posteriores de los EFAs escritos por modelos, como encontrar variaciones de problemas que sean más difíciles o más fáciles de resolver para un aprendiz, así como la generación de datos.

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.