本文介绍了EFAGen，一种用于自动构建高级数学问题可执行功能抽象（EFA）的系统。EFAs是编码系统形式规则的程序，可根据参数生成不同的输出，类似于物理模拟引擎。EFAGen将EFA的构建任务形式化为程序合成任务，通过LLM生成符合广义问题和解决方案类的EFA程序。该系统通过可执行单元测试来验证EFA的有效性，并展示了EFAGen在生成忠于原始问题的EFA、产生可学习的问题变体以及跨多种数学问题来源推断EFA方面的能力。研究结果表明，EFAGen能够生成用于下游任务的EFA，如寻找对学习者来说更难或更容易的问题变体以及数据生成。

💡 引入了EFA（可执行功能抽象）的概念，它指的是编码数学问题形式规则的程序，类似于物理模拟引擎，可以根据参数生成不同的输出。

⚙️ EFAGen被设计为自动构建高级数学问题的EFA的系统。它将EFA的构建任务转化为程序合成任务，利用大型语言模型（LLM）生成EFA程序。

✅ EFAGen通过可执行单元测试来验证EFA的有效性。这些测试被用作可验证的奖励，以训练LLM更好地编写EFA。

🎯 EFAGen生成的EFA表现出理性行为，忠于原始问题，并产生可学习的问题变体。它能够跨多种数学问题来源推断EFA。

🚀 EFAGen生成的EFA可用于下游任务，例如寻找对学习者来说更难或更容易的问题变体，以及数据生成。

arXiv:2504.09763v1 Announce Type: cross Abstract: 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.