Ausführbare funktionale Abstraktionen: Inferenz generativer Programme für fortgeschrittene mathematische Probleme

Executable Functional Abstractions: Inferring Generative Programs for Advanced Math Problems

April 14, 2025

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

cs.AI

Zusammenfassung

Wissenschaftler leiten oft abstrakte Verfahren aus spezifischen Problemfällen ab und verwenden diese Abstraktionen, um neue, verwandte Fälle zu generieren. Beispielsweise haben Programme, die die formalen Regeln und Eigenschaften eines Systems kodieren, in Bereichen wie RL (prozedurale Umgebungen) bis hin zur Physik (Simulations-Engines) nützlich erwiesen. Diese Programme können als Funktionen betrachtet werden, die basierend auf ihren Parametrisierungen (z. B. Gridworld-Konfiguration oder anfängliche physikalische Bedingungen) zu unterschiedlichen Ausgaben führen. Wir führen den Begriff EFA (Executable Functional Abstraction) ein, um solche Programme für mathematische Probleme zu bezeichnen. Ähnliche Konstrukte wie EFA haben sich als nützlich für mathematisches Denken erwiesen, insbesondere als Problemgeneratoren, um Modelle zu testen. Bisherige Arbeiten beschränkten sich jedoch auf Abstraktionen für Grundschulmathematik (deren einfache Regeln sich leicht in Programmen kodieren lassen), während die Generierung von EFAs für fortgeschrittene Mathematik bisher menschliche Ingenieurskunst erforderte. Wir untersuchen die automatische Konstruktion von EFAs für fortgeschrittene mathematische Probleme. Wir operationalisieren die Aufgabe der automatischen Konstruktion von EFAs als eine Programmsynthese-Aufgabe und entwickeln EFAGen, das ein LLM auf ein Ausgangsproblem und dessen schrittweise Lösung konditioniert, um Kandidaten für EFA-Programme zu generieren, die der verallgemeinerten Problem- und Lösungsklasse des Ausgangsproblems treu bleiben. Darüber hinaus formalisieren wir Eigenschaften, die jedes gültige EFA besitzen muss, in Form von ausführbaren Unit-Tests und zeigen, wie diese Tests als verifizierbare Belohnungen verwendet werden können, um LLMs darin zu trainieren, bessere EFA-Autoren zu werden. Wir demonstrieren, dass von EFAGen konstruierte EFAs rational agieren, indem sie den Ausgangsproblemen treu bleiben, lernbare Problemvariationen erzeugen und dass EFAGen EFAs aus mehreren diversen Quellen von Wettbewerbsmathematikproblemen ableiten kann. Schließlich zeigen wir nachgelagerte Anwendungen von modellgeschriebenen EFAs, z. B. das Finden von Problemvariationen, die für einen Lernenden schwieriger oder einfacher zu lösen sind, sowie die Datengenerierung.

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.