DatalogBench: Evaluating Large Language Models on Text-to-Datalog Synthesis
作者: Yuan Li, Hanyun Jiang, Guowei Tian, Chengpeng Wang, Peisen Yao
分类: cs.PL, cs.AI
发布日期: 2026-09-29
备注: 33 pages
💡 一句话要点
提出DatalogBench以评估大语言模型在文本到Datalog合成中的表现
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: Datalog合成 大语言模型 程序分析 自动化推理 文本到Datalog
📋 核心要点
- 现有的Datalog合成方法需要用户提供输入输出示例，限制了其使用的灵活性和效率。
- 论文提出DatalogBench基准，通过自然语言问题直接合成Datalog程序，评估大语言模型的能力。
- 实验结果显示，最好的模型在合成任务上的精确匹配率达到68.4%，并且两个编码代理的成功率高达83.8%。
📝 摘要（中文）
Datalog是程序分析等推理任务的基础，但其程序编写困难。现有合成器虽然能自动化此任务，但需要用户提供输入输出示例。大语言模型（LLMs）提供了更自然的路径，即从自然语言问题进行文本到Datalog的合成，但其效果尚未系统评估。我们提出DatalogBench，这是一个由136个文本到Datalog合成任务组成的基准，任务来源于现有的Datalog相关文献。合成的程序通过在保留输入上执行并与经过变异分析验证的oracle进行比较来评分。在六个LLMs和四种提示配置下，精确匹配率最高达到68.4%。在直接提示下，大多数失败发生在编译时，通常是因为模型发明了未声明或类型不一致的辅助谓词。两个编码代理的成功率达到83.8%，几乎消除了所有此类失败，剩下的主要是集中在递归任务的语义错误。因此，DatalogBench识别出递归推理和分解是当前LLMs和代理的开放挑战，并提供了一个可靠的、基于执行的评估标准。
🔬 方法详解
问题定义：本论文旨在解决大语言模型在文本到Datalog合成中的表现评估问题。现有方法依赖用户提供示例，限制了灵活性和准确性。
核心思路：通过构建DatalogBench基准，直接从自然语言问题生成Datalog程序，提供一种更自然的合成方式，并通过执行验证合成结果的正确性。
技术框架：DatalogBench包含136个合成任务，使用六个大语言模型和四种提示配置进行评估。合成程序通过在保留输入上执行并与oracle进行比较来评分。
关键创新：DatalogBench的创新在于其基于执行的评分机制，能够有效识别模型在合成过程中的失败原因，特别是递归推理和辅助谓词的处理。
关键设计：实验中采用了多种提示配置，评估模型在不同条件下的表现，并通过变异分析验证oracle的准确性。
🖼️ 关键图片
📊 实验亮点
实验结果显示，最佳模型在合成任务上的精确匹配率达到68.4%，而两个编码代理的成功率高达83.8%。这些结果表明，DatalogBench能够有效识别和减少合成过程中的失败，尤其是在递归任务中。
🎯 应用场景
DatalogBench的研究成果可广泛应用于程序分析、自动化推理和智能问答系统等领域。通过提高大语言模型在Datalog合成中的表现，能够推动智能系统在复杂推理任务中的应用，提升其在实际场景中的有效性和可靠性。
📄 摘要（原文）
Datalog underpins reasoning tasks such as program analysis, but its programs are hard to write. Existing synthesizers automate this task but require users to state their intent as input-output examples. Large language models (LLMs) suggest a more natural route, text-to-Datalog synthesis from a natural-language question, yet how well they do so has not been systematically evaluated. We present DatalogBench, a benchmark of 136 text-to-Datalog synthesis tasks curated from existing Datalog-based artifacts. Synthesized programs are graded by execution on held-out inputs against an oracle validated by mutation analysis. Across six LLMs and four prompting configurations, exact match peaks at 68.4%, and relation descriptions or an input-output example have only modest, model-dependent effects. Under direct prompting, most failures occur at compile time, typically because a model invents auxiliary predicates that it never declares or types consistently. Two coding agents reach up to 83.8% and eliminate nearly all such failures, leaving mostly semantic errors concentrated in recursive tasks. DatalogBench thus identifies recursive reasoning and decomposition as open challenges for current LLMs and agents, and offers a reliable, execution-grounded measure of both.