Recoleta
GitHub
来源笔记

ReaComp: Compiling LLM Reasoning into Symbolic Solvers for Efficient Program Synthesis

作者
Atharva Naik, Yash Mathur, Prakam, Carolyn Rose, David Mortensen
来源
arXiv
发布日期
栏目
Software Intelligence
Program SynthesisCode IntelligenceLLM ReasoningSymbolic SolversNeuro Symbolic AI
打开 arXivMarkdown 源文件

摘要

ReaComp把少量 LLM 推理轨迹转成可复用的符号程序合成器，用于基于示例的程序合成和逻辑规则合成。生成的求解器在测试时不需要 LLM 调用，能处理很多任务，并在困难样例上提升 LLM 兜底时的准确率和 token 用量。

问题

  • LLM 可以解决程序合成任务，但困难实例需要很多采样或迭代步骤，这会提高 token 成本，也增加失败风险。
  • 对于无结构的 LLM 搜索，长的组合程序很难处理；论文报告说，随着解的长度增加，会出现循环、反复尝试和更低的准确率。
  • 这会影响代码智能和自动化软件生产，因为当需要解决很多相似的合成任务时，重复做 LLM 推理的成本很高。

方法

  • ReaComp 先在每个基准上收集大约 100 条 LLM 推理轨迹，并在任务难度以及成功或失败之间保持平衡。
  • 一个编码代理，例如 Claude Code 或带 OpenHands 的 Qwen，读取这些轨迹，并编写一个基于受限 DSL 的独立 Python 符号求解器。
  • 求解器直接搜索程序候选，并用验证器挑出与示例匹配的候选。
  • 在测试时，先运行符号求解器。如果它解出任务，就不需要 LLM 调用；否则系统回退到 LLM Best-of-K 或直接反馈搜索。
  • 构建成本只付一次，然后可以在很多任务上复用。

结果

  • 在 PBEBench-Lite 上，All Symbolic 求解器集成的准确率达到 91.3%，测试时 LLM token 为 0；相比之下，BoK 的准确率是 93.8%，但用了 68.0M token。BoK + All Symbolic 达到 93.9%，用了 43.5M token，token 用量减少 36%。
  • 在 PBEBench-Hard 上，All Symbolic 的准确率达到 84.7%，测试时 LLM token 为 0，比 BoK 的 68.4% 高出 16.3 个百分点。BoK + All Symbolic 达到 85.8%，用了 71.6M token，而 BoK 用了 332.1M token，减少 78%。
  • 在 SLR-Bench 上，CC 符号求解器在 hard-tier 上的准确率是 46.8%，测试时 LLM token 为 0；论文报告的 o3 是 45%，GPT-5 是 46%。DF + CC 的 hard-tier 准确率达到 58.0%，整体准确率达到 86.6%。
  • 最好的 SLR 混合方案 DF + CC + QO 的整体准确率达到 86.7%，用了 138.8M token，成本为 $16.19；论文报告的 o3 是 77.8%，成本为 $207.24。
  • 不使用推理轨迹的消融结果在 PBEBench-Hard 上差很多：使用 CoT 轨迹时准确率是 74.7%，没有 CoT 轨迹时降到 24.8%。
  • 在历史语言学迁移案例中，求解器集成在 3,077 对原始语言-后代语言对上零样本达到 80.1% 准确率。

Link