Abstractions fonctionnelles exécutables : Inférence de programmes génératifs pour des problèmes mathématiques avancés

Executable Functional Abstractions: Inferring Generative Programs for Advanced Math Problems

April 14, 2025

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

cs.AI

Résumé

Les scientifiques infèrent souvent des procédures abstraites à partir d'instances spécifiques de problèmes et utilisent ces abstractions pour générer de nouvelles instances connexes. Par exemple, les programmes encodant les règles et propriétés formelles d'un système se sont avérés utiles dans des domaines allant de l'apprentissage par renforcement (environnements procéduraux) à la physique (moteurs de simulation). Ces programmes peuvent être vus comme des fonctions qui produisent différentes sorties en fonction de leurs paramétrages (par exemple, la configuration d'un monde en grille ou les conditions physiques initiales). Nous introduisons le terme EFA (Abstraction Fonctionnelle Exécutable) pour désigner de tels programmes dans le contexte des problèmes mathématiques. Des constructions similaires aux EFA se sont révélées utiles pour le raisonnement mathématique en tant que générateurs de problèmes pour tester la robustesse des modèles. Cependant, les travaux antérieurs se sont limités aux abstractions pour les mathématiques de niveau primaire (dont les règles simples sont faciles à encoder dans des programmes), tandis que la génération d'EFA pour les mathématiques avancées a jusqu'à présent nécessité une ingénierie humaine. Nous explorons la construction automatique d'EFA pour des problèmes de mathématiques avancées. Nous formalisons la tâche de construction automatique d'EFA comme une tâche de synthèse de programmes, et développons EFAGen, qui conditionne un modèle de langage (LLM) sur un problème mathématique de départ et sa solution étape par étape pour générer des programmes EFA candidats fidèles à la classe généralisée de problèmes et de solutions sous-jacente au problème de départ. De plus, nous formalisons les propriétés que tout EFA valide doit posséder en termes de tests unitaires exécutables, et montrons comment ces tests peuvent être utilisés comme récompenses vérifiables pour entraîner les LLM à devenir de meilleurs rédacteurs d'EFA. Nous démontrons que les EFA construits par EFAGen se comportent de manière rationnelle en restant fidèles aux problèmes de départ, produisent des variations de problèmes apprenables, et qu'EFAGen peut inférer des EFA à partir de multiples sources diversifiées de problèmes de mathématiques de niveau compétition. Enfin, nous montrons les utilisations en aval des EFA écrits par des modèles, par exemple pour trouver des variations de problèmes plus difficiles ou plus faciles à résoudre pour un apprenant, ainsi que pour la génération de données.

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.