Astrazioni Funzionali Eseguibili: Inferire Programmi Generativi per Problemi Matematici Avanzati

Executable Functional Abstractions: Inferring Generative Programs for Advanced Math Problems

April 14, 2025

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

cs.AI

Abstract

Gli scienziati spesso deducono procedure astratte da istanze specifiche di problemi e utilizzano queste astrazioni per generare nuove istanze correlate. Ad esempio, i programmi che codificano le regole formali e le proprietà di un sistema si sono rivelati utili in campi che vanno dall'RL (ambienti procedurali) alla fisica (motori di simulazione). Questi programmi possono essere visti come funzioni che producono output diversi in base alle loro parametrizzazioni (ad esempio, la configurazione di un gridworld o le condizioni fisiche iniziali). Introduciamo il termine EFA (Executable Functional Abstraction) per denotare tali programmi per problemi matematici. Costrutti simili agli EFA si sono dimostrati utili per il ragionamento matematico come generatori di problemi per testare i modelli. Tuttavia, il lavoro precedente si è limitato ad astrazioni per la matematica di livello scolastico (le cui regole semplici sono facili da codificare nei programmi), mentre la generazione di EFA per la matematica avanzata ha finora richiesto l'intervento umano. Esploriamo la costruzione automatica di EFA per problemi di matematica avanzata. Operazionalizziamo il compito di costruire automaticamente EFA come un compito di sintesi di programmi e sviluppiamo EFAGen, che condiziona un LLM su un problema matematico iniziale e la sua soluzione passo-passo per generare programmi EFA candidati che siano fedeli al problema generalizzato e alla classe di soluzioni sottostante al problema iniziale. Inoltre, formalizziamo le proprietà che qualsiasi EFA valido deve possedere in termini di test unitari eseguibili e mostriamo come i test possano essere utilizzati come ricompense verificabili per addestrare gli LLM a diventare migliori scrittori di EFA. Dimostriamo che gli EFA costruiti da EFAGen si comportano razionalmente rimanendo fedeli ai problemi iniziali, producono variazioni di problemi apprendibili e che EFAGen può dedurre EFA da molteplici fonti diverse di problemi matematici di livello competitivo. Infine, mostriamo gli usi a valle degli EFA scritti dai modelli, ad esempio trovare variazioni di problemi che sono più difficili o più facili da risolvere per un apprendente, nonché la generazione di dati.

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.