Uitvoerbare Functionele Abstracties: Het Afleiden van Generatieve Programma's voor Geavanceerde Wiskundige Problemen

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

Samenvatting

Wetenschappers leiden vaak abstracte procedures af uit specifieke probleemgevallen en gebruiken deze abstracties om nieuwe, gerelateerde gevallen te genereren. Bijvoorbeeld, programma's die de formele regels en eigenschappen van een systeem coderen, zijn nuttig gebleken in velden variërend van RL (procedurele omgevingen) tot natuurkunde (simulatie-engines). Deze programma's kunnen worden gezien als functies die verschillende uitvoer genereren op basis van hun parameterisaties (bijvoorbeeld gridworld-configuratie of initiële fysische condities). We introduceren de term EFA (Executable Functional Abstraction) om dergelijke programma's voor wiskundige problemen aan te duiden. EFA-achtige constructies zijn nuttig gebleken voor wiskundig redeneren als probleemgeneratoren om modellen te stress-testen. Eerdere werkzaamheden waren echter beperkt tot abstracties voor basisschoolwiskunde (waarvan de eenvoudige regels gemakkelijk in programma's kunnen worden gecodeerd), terwijl het genereren van EFA's voor gevorderde wiskunde tot nu toe menselijke engineering vereiste. We onderzoeken de automatische constructie van EFA's voor gevorderde wiskundige problemen. We operationaliseren de taak van het automatisch construeren van EFA's als een programma-synthesetaak en ontwikkelen EFAGen, dat een LLM conditioneert op een startwiskundeprobleem en de stapsgewijze oplossing om kandidaat-EFA-programma's te genereren die trouw zijn aan het gegeneraliseerde probleem en de oplossingsklasse die ten grondslag ligt aan het startprobleem. Bovendien formaliseren we eigenschappen die elke geldige EFA moet bezitten in termen van uitvoerbare unittests, en laten we zien hoe deze tests kunnen worden gebruikt als verifieerbare beloningen om LLM's te trainen om betere schrijvers van EFA's te worden. We demonstreren dat EFA's die door EFAGen zijn geconstrueerd rationeel gedrag vertonen door trouw te blijven aan startproblemen, leerbare probleemvariaties produceren, en dat EFAGen EFA's kan afleiden uit meerdere diverse bronnen van competitieniveau wiskundeproblemen. Ten slotte tonen we downstream toepassingen van modelgeschreven EFA's aan, zoals het vinden van probleemvariaties die moeilijker of gemakkelijker zijn voor een leerling om op te lossen, evenals datageneratie.

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.