Abstract
Scientists often infer abstract procedures from specific instances ofproblems and use the abstractions to generate new, related instances. Forexample, programs encoding the formal rules and properties of a system havebeen useful in fields ranging from reinforcement learning (proceduralenvironments) to physics (simulation engines). These programs can be seen asfunctions which execute to different outputs based on their parameterizations(e.g., gridworld configuration or initial physical conditions). We introducethe term EFA (Executable Functional Abstraction) to denote such programs formath problems. EFA-like constructs have been shown to be useful formathematical reasoning as problem generators for stress-testing models.However, prior work has been limited to automatically constructing abstractionsfor grade-school math (whose simple rules are easy to encode in programs),while generating EFAs for advanced math has thus far required humanengineering. We explore the automatic construction of EFAs for advancedmathematics problems by developing EFAGen, which operationalizes the task ofautomatically inferring an EFA for a given seed problem and solution as aprogram synthesis task. We first formalize the properties of any valid EFA asexecutable unit tests. Using execution feedback from the unit tests, we searchover candidate programs sampled from a LLM to find EFA programs that arefaithful to the generalized problem and solution class underlying the seedproblem. We then apply the tests as a reward signal, training LLMs to becomebetter writers of EFAs. We show that EFAs inferred by EFAGen are faithful tothe seed problems, produce learnable problem variations, and that EFAGen caninfer EFAs across diverse sources of competition-level math problems. Finally,we show uses of model-written EFAs e.g., finding harder/easier problemvariants, as well as data generation.