将大模型推理过程编译为符号求解器,实现高效零调用程序合成。
ReaComp: Compiling LLM Reasoning into Symbolic Solvers for Efficient Program Synthesis

- 从少量推理轨迹中生成可复用的符号求解器,无需运行大模型即可求解。
- 在硬任务上准确率达84.7%,比依赖大模型的方案高16.3个百分点,且零推理成本。
- 可零样本迁移至语言学任务,恢复合理音变规则,适合需要高效可靠求解的场景。
大模型虽能解决程序合成任务,但在需大规模组合搜索的难题上效率低、不可靠。本文基于少量推理轨迹,利用编码智能体将其编译为约束式领域特定语言(DSL)上的可复用符号求解器。这些求解器在测试时无需调用大模型,表现强劲:符号求解器集成在PBEBench-Lite上达91.3%准确率,在PBEBench-Hard上达84.7%,超越使用大模型测试时扩展的方案(+16.3个百分点),且无大模型推理开销。它们还与大模型搜索互补,使PBEBench-Hard准确率从68.4%提升至85.8%,同时减少78%的令牌消耗;在神经符号混合设置下,SLR-Bench硬层级准确率从34.4%升至58.0%。相比直接以编码智能体为单例求解器,所诱导的求解器更符合帕累托最优,一次性构建成本可分摊于多次零令牌执行。多数求解器零样本迁移到真实历史语言学任务——预测自然语言音变——通过集成达到80.1%准确率,并恢复部分合理语言规则。结果表明,推理轨迹可被编译为通用符号求解器,既能独立解决多类任务,又可增强大模型在困难案例中的表现,提供一种可扩展的通用求解器生成路径。代码与数据已公开供复现。
原文摘要 · Abstract (English)
LLMs can solve program synthesis tasks but remain inefficient and unreliable on hard instances requiring large combinatorial search. Given a small set of reasoning traces, we use coding agents to compile them into reusable symbolic program synthesizers over constrained DSLs. The resulting solvers require no LLM calls at test time and are strong standalone systems: symbolic solver ensembles reach 91.3% accuracy on PBEBench-Lite and 84.7% on PBEBench-Hard, outperforming LLMs with test-time scaling for the latter by +16.3 percentage points at zero LLM inference cost. They also complement LLM search, improving PBEBench-Hard accuracy from 68.4% to 85.8% while reducing reported token usage by 78%, and raising SLR-Bench hard-tier accuracy from 34.4% to 58.0% in a neuro-symbolic hybrid setting. Compared to directly using coding agents as per-instance solvers, induced solvers are substantially more Pareto-efficient, amortizing a small one-time construction cost over many zero-token executions. Finally, most solvers transfer zero-shot to a real historical linguistics task - predicting sound changes in natural language data - reaching 80.1% accuracy under ensembling and recovering some plausible linguistic rules. Together, these results show that reasoning traces can be compiled into reusable symbolic solvers that solve many tasks directly, complement LLM inference on hard cases, and provide a scalable route to domain-general solver induction. We release code and data for reproducibility.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。