PaperlayerView exact revision on arXiv

Source-linked AI summary

DatalogBench: Evaluating Large Language Models on Text-to-Datalog Synthesis

Yuan Li, Hanyun Jiang, Guowei Tian, Chengpeng Wang, Peisen Yao

arXiv:2609.37233v1cs.PLcs.AI

TL;DR

Datalog programs are hard to write, and existing synthesizers require users to specify intent with input–output examples; text-to-Datalog synthesis from natural language has not been systematically evaluated. DATALOGBENCH evaluates generated programs on held-out inputs, finding direct prompting peaks at 68.4% exact match while coding agents eliminate nearly all compile failures but leave recursive semantic errors. The benchmark identifies recursive reasoning and decomposition as open challenges for current LLMs and agents.

  • Problem

    Datalog synthesis from natural language has not been systematically evaluated, while existing synthesizers require input–output examples that are neither natural nor easy to produce.

    Source: §1 · p. 1

  • Method

    DATALOGBENCH evaluates 136 text-to-Datalog tasks with execution on held-out variants against an oracle validated by mutation analysis.

    Source: §1 · p. 2

  • Results

    Direct prompting peaks at 68.4% exact match; coding agents nearly eliminate compile failures, but remaining errors are mostly semantic and concentrated in recursive tasks.

    Source: §1 · p. 2

  • Takeaways & Limitations

    Recursive reasoning and decomposition remain open challenges for current LLMs and coding agents.

    Source: §1 · p. 2, §7 · p. 9

    The study targets the Soufflé dialect alone and does not measure how far its findings transfer.

    Source: §7 · p. 9

Abstract

from arXiv · show

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.

1 INTRODUCTION

Datalog synthesis is difficult to specify through input–output examples, and text-to-Datalog synthesis from natural language has not been systematically evaluated. DATALOGBENCH evaluates this task with held-out execution, finding that direct prompting remains error-prone and coding agents leave recursive reasoning and decomposition as challenges.

1 INTRODUCTION

  • DATALOGBENCH contains 136 tasks from four reasoning domains and evaluates six LLMs across four prompting configurations, plus two coding agents.Tasks pair a natural-language question with relation signatures and held-out evaluation variants.Source: §1 · p. 2
  • 68.4% is the peak exact match under direct prompting; coding agents solve up to 83.8%.Relation descriptions and an input–output example help only modestly and not for every model.Source: §1 · p. 2
  • Most direct-prompting failures occur at compile time when invented auxiliary predicates are undeclared or inconsistently typed; agents nearly eliminate compile failures, leaving mainly recursive semantic errors.Supplying missing declarations alone recovers only a small share of exact match.Source: §1 · p. 2
  • The execution-based protocol grades programs on held-out variants, reports compile pass and exact match separately, and validates its oracle by mutation analysis.Source: §1 · p. 2

2 RELATED WORK

Prior Datalog synthesis and inductive logic programming largely take input–output examples as specifications, while existing LLM-related work does not benchmark whether natural-language-generated Datalog computes intended relations. Code-generation and text-to-SQL benchmarks offer related evaluation lessons but do not target Datalog’s distinctive demands.

2 RELATED WORK

  • Datalog synthesis and inductive logic programming use input–output examples, often with language biases or templates; LLMs have also steered symbolic search or written queries for code localization [Albarghouthi et al., 2017; Si et al., 2018; 2019; Bembenek et al., 2023; Raghothaman et al., 2020; Thakkar et al., 2021; Mendelson et al., 2021; Cropper & Morel, 2021; Cropper & Dumanˇci´c, 2022; Muggleton et al., 2015; Cerna & Cropper, 2024; Barke et al., 2024; Xu et al., 2026].The code-localization work scores localization accuracy rather than whether the generated Datalog computes intended relations.Source: §2 · p. 2
  • Code-generation benchmarks show that weak tests can overestimate correctness, while Datalog evaluation must also separate compile failures from semantic errors [Chen et al., 2021; Liu et al., 2023].DATALOGBENCH adopts mutation analysis to validate its oracle.Source: §2 · pp. 2–3
  • Text-to-SQL benchmarks emphasize schema grounding, joins, aggregation, and value use, but rarely require recursion or named auxiliary predicates, the demands DATALOGBENCH measures [Lei et al., 2025].Source: §2 · p. 3

3 PRELIMINARIES

Datalog programs derive output relations by repeatedly applying rules to reach a least fixed point, with recursion expressing iteration over potentially unbounded paths. DATALOGBENCH frames synthesis as producing a candidate from a question and schema, then grading it on held-out evaluation variants.

3 PRELIMINARIES

  • A Datalog program applies rules over input facts until reaching a least fixed point; recursion occurs when the predicate dependency graph contains a cycle.The Reachable rules compute transitive closure, which cannot be expressed by a fixed number of joins when paths may be arbitrarily long.Source: §3 · p. 3
  • Datalog synthesis demands correct recursive base cases and inductive steps, invented and typed auxiliary predicates, and static checks for bindings, types, and stratification.A compile rejection means the program never reaches the data, distinguishing compile failures from semantic errors.Source: §3 · p. 3
  • Each task provides a natural-language question, input/output relation signatures, and optionally relation descriptions; a candidate may introduce auxiliary predicates.Demonstration instances are separate from evaluation variants used to compute scores.Source: §3 · p. 3
  • Figure 1 depicts a question-and-signatures prompt followed by Soufflé execution on held-out variants, comparing candidate outputs with expected facts.The evaluation variants are disjoint from the demonstration instance.Source: Figure 1 · p. 4, §3 · p. 4

4 DATALOGBENCH

DATALOGBENCH collects and normalizes tasks from public artifacts, verifies their reference outputs, and annotates them with questions and relation descriptions. Its 136 tasks cover substantial structural variation, and its execution oracle is tested with mutations while remaining bounded in what those tests establish.

4.1 BENCHMARK CONSTRUCTION

  • The four construction phases collect artifact tasks, normalize relations and input facts, verify reference outputs under Soufflé, and annotate tasks with questions and descriptions.Questions must name every output relation and make quantifiers explicit; auxiliary predicates are omitted from specifications for models to invent.Source: §4.1 · pp. 4–5

4.2 BENCHMARK STATISTICS

  • 78 of 136 tasks are recursive and 59 introduce an auxiliary predicate; the benchmark spans four domains with differing structural profiles.The domain sizes are 47 program-analysis, 33 graph-analytics, 29 formal-reasoning, and 27 knowledge-discovery tasks.Source: §4.2 · p. 5, Table 1 · p. 5

4.3 BENCHMARK VALIDATION

  • Held-out variants score programs separately from the demonstration instance, so fitting the demonstration earns credit only when unseen inputs also produce intended relations.Both coding agents have candidates that fail this held-out test.Source: §4.3 · p. 5
  • The evaluation variants distinguish 1,877 of 1,948 rule-deletion, body-atom-deletion, and join-variable-rebinding mutants (96.4%), but this does not prove equivalence to the reference.The mutation tests do not alter negation, aggregate functions, or grouping scope; all 71 surviving mutants are certified equivalent.Source: §4.3 · p. 5

5 EVALUATION

The evaluation compares direct prompting and coding agents under defined prompt settings, then scores programs using compile and held-out execution checks. A declaration-repair metric separately diagnoses errors caused by omitted auxiliary declarations.

5.1 EXPERIMENTAL SETUP

  • Direct prompting varies relation descriptions and demonstration examples, while coding agents receive up to four turns with execution feedback and file and shell tools.Six LLMs are evaluated; each agent is compared with the Direct cell for its paired model.Source: §5.1 · p. 6
  • Task-paired comparisons use 95% percentile-bootstrap intervals over 10,000 resamples and two-sided sign-flip tests.Each Direct cell and agent ran once.Source: §5.1 · p. 6

5.2 EVALUATION METRICS

  • Compile Pass measures whether a program passes static checks, while Exact Match requires it to run and match the reference on every held-out variant.Both metrics are task averages; the benchmark reports them separately.Source: §5.2 · p. 6
  • EX† credits a program that becomes exact after omitted auxiliary declarations are synthesized from its rules, without changing any rule.It is diagnostic; raw EX remains the primary measure of the submitted program.Source: §5.2 · p. 6
  • Figure 3 compares exact match with and without an input–output example under each schema.Source: Figure 3 · p. 7

6 RESULTS

Coding agents outperform their matched direct-prompting cells, but recursion and auxiliary-predicate demands remain difficult. Direct prompting is often rejected at compile time, while the agents’ remaining errors are mostly semantic.

6.1 DIRECT PROMPTING

  • 68.4% EX is the best Direct-cell result; across six models, zero-shot EX averages 49.0% with signatures and 51.0% with descriptions.The best result is Claude Opus 5 with descriptions and one input–output example.Source: §6.1 · p. 7
  • Descriptions add approximately 2.0 points on average, and an example adds over 3.5 points, but neither change yields a reliable general gain.Only one of 12 within-model schema contrasts is significant; none of the 12 example contrasts is significant. Figure 3 presents exact match by schema and example condition.Source: §6.1 · p. 7, Figure 4 · p. 8

6.2 CODING AGENTS

  • 82.4% EX for Codex versus 55.9% for GPT 5.6 Sol, and 83.8% for CC versus 52.2% for Claude Opus 5.These are paired gains of 26.5 and 31.6 points, respectively; Table 3 covers agents using signatures, no example, and up to four turns.Source: §6.2 · p. 7, Table 3 · p. 8
  • For the 47 tasks requiring both recursion and auxiliary predicates, exact match reaches 68.1% for Codex and 74.5% for CC, below 97.8% on the 46 tasks requiring neither.Figure 4 traces exact match from each model’s Direct cell to its agent by reference structure.Source: Figure 4 · p. 8, §6.2 · p. 8

6.3 FAILURE MODE ANALYSIS

  • 31.7% of Direct programs fail to compile, and 15.9% compile but compute the wrong relations; incomplete predicate invention is the largest compile-failure group at 44.1%.Inferring omitted declarations makes 160 of 261 undefined-auxiliary cases exact, adding 4.9 points to mean EX.Source: §6.3 · p. 8
  • Exact match is lower on recursive and auxiliary-predicate tasks, and the two demands remain distinct; auxiliary predicates mainly raise compile failures, while recursion adds semantic errors.On tasks with both demands, exact match is 10.6%–44.7%, versus 71.7%–84.8% when neither is required.Source: §6.3 · pp. 8–9
  • Agents reduce compile failures from 31 to 3 for Codex and from 33 to 0 for CC, but most remaining compiled-but-wrong programs are on recursive tasks.The paper suggests focusing model- or search-based repair on base cases, inductive bindings, and auxiliary predicates; held-out evaluation remains necessary because demonstration-instance correctness can overfit.Source: §6.3 · p. 9

7 CONCLUSION

The paper introduces DATALOGBENCH, an execution-based benchmark for text-to-Datalog synthesis, and finds that coding agents address compile failures more effectively than semantic errors. Recursive reasoning and decomposition remain open challenges, within a study bounded by its dialect, oracle, and agent setting.

7 CONCLUSION

  • DATALOGBENCH contains text-to-Datalog tasks in the Soufflé dialect and uses an execution oracle validated by mutation analysis.Source: §7 · p. 9
  • Direct prompting remains unreliable, while relation descriptions and input–output examples have modest, model-dependent effects.Source: §7 · p. 9
  • Coding agents nearly eliminate compile failures, but their remaining errors are mostly semantic and concentrated in recursive tasks.Tasks combining recursion with auxiliary predicates remain harder.Source: §7 · p. 9
  • The study tests only Soufflé, does not establish oracle completeness, and does not separate the contributions of agent tooling and execution feedback.Source: §7 · p. 9

AI USE STATEMENT

The authors describe how language models were used in the work and distinguish that use from benchmark construction and evaluation.

AI USE STATEMENT

  • No benchmark content was generated by an LLM; authors wrote the questions and relation descriptions, and reference programs came from upstream artifacts or the authors.Source: AI USE STATEMENT · p. 9
  • LLMs assisted with grammar editing and language polishing, while coding agents wrote analysis and plotting scripts from measurements supplied by the authors.Source: AI USE STATEMENT · p. 9
  • Every reported number comes from running the released evaluation pipeline.Source: AI USE STATEMENT · p. 9

ETHICS STATEMENT

The benchmark uses public research artifacts and open-source tools under their stated licenses, with GenSynth referenced as an unmodified submodule despite its repository declaring no license. Its data and evaluation setup exclude personal data and constrain generated programs and agents to scratch environments.

ETHICS STATEMENT

  • The benchmark derives tasks from Soufflé, EGS, CodeFuse-Query, and GenSynth artifacts, using each under its stated license except that GenSynth declares no license.GenSynth is referenced as an unmodified submodule, with task specifications derived from its published benchmark files.Source: ETHICS STATEMENT · p. 9
  • The benchmark contains only synthetic relational facts and program-analysis fixtures, with no personal data, user-generated content, or material about identifiable individuals.Authors wrote all questions, relation descriptions, and annotations; no crowdworkers were involved.Source: ETHICS STATEMENT · p. 10
  • Generated programs run in scratch directories; agents cannot access the benchmark tree or reference programs, and their network access is limited to the model endpoint.No generated program writes outside its scratch directory.Source: ETHICS STATEMENT · p. 10

REPRODUCIBILITY STATEMENT

The supplementary materials document the benchmark formalism, prompts, evaluated systems, runtime controls, and setup choices, while releasing scripts and configurations to support reproduction. They also describe annotation checks and boundaries on the experimental setting.

REPRODUCIBILITY STATEMENT

  • The benchmark, prompts, harness, scoring scripts, and analysis scripts are released, alongside scripts to regenerate structural statistics and derived figures.The statement records experiment settings, metrics, prompt templates, evaluated systems, agent configurations, and patches for building symbolic baselines.Source: REPRODUCIBILITY STATEMENT · p. 10

A DATALOG FORMALISM AND THE INDUCTIVE SYNTHESIS PROBLEM

  • A synthesis problem specifies input and output relation signatures, input facts, and positive and negative output examples; DATALOGBENCH instead grades exact output equality on every evaluation variant.The formalism also describes Datalog rules, variable safety, recursion, and stratified evaluation.Source: A DATALOG FORMALISM AND THE INDUCTIVE… · pp. 14–15

B PROMPT TEMPLATES

  • The prompt templates vary domain-knowledge notes, relation descriptions, and demonstration examples, and require generated output in Soufflé Datalog format.Agent feedback uses the demonstration instance only; evaluation variants are not run until the candidate is frozen.Source: B PROMPT TEMPLATES · pp. 15–16

C.1 MODEL INVENTORY; C.2 REQUEST CONTRACTS AND RUNTIME

  • Six LLMs receive the same untuned prompt template, and candidate programs are compiled and executed with Soufflé 2.5 under a 30-second timeout.The model inventory includes two DeepSeek Flash modes on the same underlying model; the reasoning toggle makes them a controlled ablation.Source: Table 4 · p. 16, §C.1 · pp. 16–17, §C.2 · p. 17

C.2 REQUEST CONTRACTS AND RUNTIME; C.3 SETTINGS AND REPRODUCIBILITY

  • The agent environment pins CLI and Soufflé versions, isolates reference programs, and verifies that reference files are unreadable and external URLs fail to resolve.The benchmark and complete experiment run matrix are released; hosted model outputs are reproducible only while providers continue serving recorded builds.Source: §C.2 · p. 17, §C.3 · p. 17

C.4 SETUP DETAILS OMITTED FROM THE MAIN TEXT

  • Each task has one demonstration instance, which cannot establish how the prompting effect scales with more examples; knowledge notes provide vocabulary but not program structure.Retrieval is disabled because public upstream artifacts include reference programs; clients whose retrieval cannot be disabled are outside this setting.Source: §C.4 · pp. 17–18

C.5 ANNOTATION QUALITY CONTROL

  • Annotation checks align questions and relation descriptions with reference-program semantics, standardize relation roles, and retain only tasks whose oracle outputs match execution.Datalog-experienced co-authors resolved disagreements, revising ambiguous questions or excluding tasks when ambiguity could not be removed without exposing implementation details.Source: §C.5 · p. 18

C.6 CONTAMINATION ANALYSIS

The contamination analysis finds little evidence that upstream program-name recall explains measured performance, but cannot rule out recall of algorithms under renamed predicates. The accompanying construction details describe curation, normalization, and checks used to validate benchmark tasks.

C.6 CONTAMINATION ANALYSIS

  • Renaming relations and regenerating facts constrain verbatim copying, but do not block recall of algorithms; exposure remains harder to exclude for idiosyncratic targets.Standard constructions such as transitive closure are treated as ordinary competence, while recall of specific pointer-analysis or parsing algorithms cannot be excluded.Source: §C.6 · p. 18
  • 52.2% exact match on 25 CodeFuse-Query tasks compares with 51.7% on the other 111 tasks, a 0.5-point gap opposite the predicted contamination direction but weak evidence either way.CodeFuse-Query tasks had Gödel, not Datalog, source programs; differences in domain and provenance limit this comparison.Source: §C.6 · pp. 18–19
  • The scan flags 622 of 3,531 generated programs for upstream-only predicate names, but inspection finds none to be evidence of recall.The scan detects only recall that surfaces as a name, so structural recall under renamed predicates may go unnoticed.Source: §C.6 · p. 19

D BENCHMARK CONSTRUCTION IN DETAIL

  • Tasks were curated from existing artifacts, sanitized to remove complex types and non-core language components, and supplemented with manually authored Datalog references or translations from Gödel where needed.Questions and relation annotations were authored and revised to make intended relations explicit when multiple interpretations were plausible.Source: D BENCHMARK CONSTRUCTION IN DETAIL · pp. 19, 21
  • The benchmark retains tasks with symbol types for opaque identities and number types where arithmetic, aggregation, or order-sensitive semantics require them.After retyping, each reference program had to continue matching its oracle on all evaluation variants.Source: D BENCHMARK CONSTRUCTION IN DETAIL · p. 20
  • All 136 reference programs execute within 30 seconds and match expected outputs across retained input-output examples; continuous checks also report no unreachable rules or ungraded output relations.The reference programs were validated on 247 evaluation variants, in addition to one ungraded demonstration instance per task.Source: D BENCHMARK CONSTRUCTION IN DETAIL · p. 20

E BENCHMARK STATISTICS IN DETAIL

This section details DatalogBench’s task structure, scoring, oracle validation, reproducibility limits, and representative failure modes, including a taxonomy of Direct compile failures and guidance to interpret results by structural properties and domain.

E BENCHMARK STATISTICS IN DETAIL

  • 78 of 136 tasks (57.4%) are recursive, while reference programs average 5.1 rules (median 3), and all are stratified.Negation appears in 34 tasks and aggregation in 22; programs average 1.5 strata, up to 5. First-variant inputs have heavy-tailed sizes: mean input/output tuples are 82/1,517 versus medians of 10/5, and the long tail is retained to test realistic scaling. The four domains differ structurally: formal reasoning and graph analytics are most recursive, while knowledge discovery has the lowest recursion rate and predicate invention; graph analytics has large recursive components, deeper stratification, and more aggregation.Source: E BENCHMARK STATISTICS IN DETAIL · pp. 21–23
  • The two difficulty axes correlate at ρ = +0.333, yet formal reasoning combines longer programs with lighter specifications while program analysis has heavier specification load on shorter programs.Program complexity and specification load use separate mean-percentile ranks because a composite would confound them; both are structural proxies, not calibrated difficulty scales. Only 31.8% of tasks needing a schema-absent domain fact are solved, versus 56.3% for the rest, but the small labeled groups and complexity-confounded gaps prevent attributing the difference to the label. Domain labels mark origin rather than difficulty, so results are also sliced by structural property.Source: E BENCHMARK STATISTICS IN DETAIL · pp. 22–23

F METRIC DEFINITIONS

  • Exact match requires compilation and correct outputs on every evaluation variant; tuple-level precision, recall, and F1 provide partial credit, while negative exclusion is reported only for compiling candidates on tasks with negatives.A timeout counts as compilation success but yields no output on that variant. Tuple metrics are macro-averaged over tasks; negative exclusion uses mined tuples from semantic mutants, and non-compiling candidates are excluded rather than treated as perfect exclusions.Source: F METRIC DEFINITIONS · pp. 23–24

G.1 CHECKS AND MUTATION ANALYSIS

  • 1,877 of 1,948 mutants are distinguished by the evaluation variants (96.4%); after all 71 survivors are certified equivalent, the adjusted score is 100%.The raw score is retained as the conservative headline: three mutation operators cannot cover every error class, and their result does not establish separation from arbitrary incorrect programs. Eleven CI invariants pass; on TwoSAT, extra input-construction strategies kill no additional mutants when only the verdict is scored, while existing inputs kill all mutants when the contradiction set is also scored.Source: §G.1 · p. 25

G.2 ADJUDICATING RAW SURVIVORS

  • Variant 0, the canonical evaluation instance, kills 1,676 mutants, and 111 additional variants kill 201 more; targeted variants can eliminate an entire family of near-miss programs.The adjusted 100% score establishes no gap for these operators, but does not prove equivalence for arbitrary programs or error classes the operators never generate.Source: §G.2 · p. 26

H CODE, ENVIRONMENT, AND MODEL PROVENANCE

  • A single setup script builds pinned symbolic baselines, and evaluation uses Soufflé 2.5 with Python 3.10 under a 30-second per-execution timeout on CPU-only infrastructure.The script applies committed patches idempotently and skips tools with missing prerequisites; model inference uses hosted APIs, while Soufflé execution is local.Source: §H.1 · p. 26, §H.2 · p. 26

H.3 MODEL ACCESS AND VERSION PROVENANCE

  • Model provenance is observable but not fully reproducible: hosted identifiers are recorded, while coding-agent pipelines report only requested model names and later runs may reach different builds.The two DeepSeek Flash arms returned the same served identifier across 1,088 calls and differed by the explicit thinking field; local symbolic baselines and Soufflé evaluation remain deterministic given the released code.Source: §H.3 · p. 27

I WHAT THE FAILURES LOOK LIKE

  • Examples show both a compound compile failure from an undeclared, unsafe auxiliary predicate and a semantic error caused by transposing a built-in’s arguments.In the Bigram example, declaring Adjacent alone would not fix the unbound variable in negation; the library-predicate example otherwise matches the reference’s joins, variables, and output.Source: I WHAT THE FAILURES LOOK LIKE · pp. 27–28
  • 15 of 37 generated calls across three tasks transpose match or contains arguments, across four models and all four prompt settings.The logic can be right while the standard-library calling convention is wrong; such a program may compile but return an empty relation.Source: I WHAT THE FAILURES LOOK LIKE · p. 28
  • The ShortestEdges example derives 2 tuples instead of 1,603 after dropping the atom that grounds the minimum per node.Without that atom, the grouped aggregate becomes a global minimum, although the generated rule reads plausibly in English.Source: I WHAT THE FAILURES LOOK LIKE · p. 28
  • Traffic fails in 23 of 24 Direct cells when the model omits one crash-rule orientation; RevSameGen overgenerates, with near-perfect recall and about half precision.The two errors reflect opposite assumptions about symmetry: Crashable is treated as symmetric, while RevSameGen is made symmetric despite the specification.Source: I WHAT THE FAILURES LOOK LIKE · pp. 28–29

J COMPILE-FAILURE TAXONOMY

  • The taxonomy groups 1,036 Direct compile failures across 24 cells by the rejected statement and error message, with Table 8 presenting the cause classes.Type-inference failures count as predicate invention only when the rejected rule defines a relation outside the schema; otherwise they count as typing. Compiling programs that time out are excluded, and a sample of each class was checked by hand.Source: J COMPILE-FAILURE TAXONOMY · p. 29, Table 8 · p. 29

K STRUCTURAL ANALYSIS OF FAILURES

Structural difficulty clusters around recursion and auxiliary-predicate decomposition, with the largest exact-match gap on tasks requiring both. Domain rankings vary by model, while example-driven synthesizers and coding agents provide complementary comparisons that require careful interpretation.

K STRUCTURAL ANALYSIS OF FAILURES

  • Recursive-task exact match ranges from 17.9% to 47.4%, versus 60.3%–81.0% on non-recursive tasks; errors concern base cases, inductive steps, and variable bindings.Generated dependency graphs usually include recursion when the reference does, so omitting recursion alone does not explain the gap.Source: K STRUCTURAL ANALYSIS OF FAILURES · p. 29

L PER-DOMAIN MODEL PERFORMANCE

  • Formal reasoning is usually the weakest domain slice, but rankings vary across models; Gemini with descriptions is an exception.Table 9 reports the domain breakdown; the analysis uses structural properties rather than domain labels as a difficulty scale.Source: Table 9 · p. 30, L PER-DOMAIN MODEL PERFORMANCE · p. 30

K STRUCTURAL ANALYSIS OF FAILURES

  • 59 of 136 reference programs introduce auxiliary predicates, and exact match on those tasks ranges from 11.9% to 49.2%, versus 54.5%–71.4% when none are needed.The task groups overlap with recursion; candidate-invention counts are not interpreted causally because malformed programs are excluded from structural parsing.Source: K STRUCTURAL ANALYSIS OF FAILURES · p. 30
  • Exact match falls to 10.6%–44.7% on tasks requiring both recursion and auxiliary predicates, versus 71.7%–84.8% on tasks requiring neither.These task sets overlap substantially, and the comparison is observational rather than causal.Source: K STRUCTURAL ANALYSIS OF FAILURES · p. 30

M SYMBOLIC SYNTHESIS FROM EXAMPLES

  • EGS solves 49 tasks, 47 of which at least one Direct configuration also solves; aggregate results do not establish that example-guided search outperforms LLM synthesis.The tools receive examples but no question, while models receive the question and schema but not the search space; ProSynth is limited to rule width 2.Source: Table 10 · p. 31, M SYMBOLIC SYNTHESIS FROM EXAMPLES · p. 31

N AGENT TURN-BY-TURN DETAIL

  • Agent exact matches accumulate mainly on the second turn, when execution feedback first appears, and the curve flattens after the third; recursive tasks dominate gains beyond declaration repair.The split is observational, and a longer turn budget was not tested.Source: N AGENT TURN-BY-TURN DETAIL · pp. 31–32

O LIMITATIONS IN DETAIL

The benchmark and agent results have bounded scope: they target Soufflé, finite evaluation variants cannot prove program equivalence, and agent gains cannot be attributed to feedback alone. The implications favor checked LLM assistance and complementary symbolic methods over autonomous synthesis.

O LIMITATIONS IN DETAIL

  • DATALOGBENCH evaluates only Soufflé; findings’ transfer to other Datalog dialects is unmeasured, and programs counted incorrect here may be well-formed elsewhere.Other engines differ in typing, aggregation, and negation.Source: O LIMITATIONS IN DETAIL · p. 32
  • Agreement on finite variants does not prove equivalence; mutation analysis distinguishes 1,877 of 1,948 mutants, but its operators omit negation, aggregates, and grouping scope.The authors therefore bound the score’s scope to errors in monotone rules and join bindings.Source: O LIMITATIONS IN DETAIL · p. 32
  • Because agents receive execution feedback and a scaffold together, the study cannot separate how much each contributes to their gains.The scaffold includes a persistent session, file access, and a shell.Source: O LIMITATIONS IN DETAIL · p. 32

P IMPLICATIONS

  • LLMs are framed as drafting assistants rather than autonomous synthesizers; generated programs still require executable checks and human review.The proposed workflow pairs model-generated sketches with symbolic validation, while practitioners are advised to test representative inputs and compare outputs against an independent oracle.Source: P IMPLICATIONS · p. 33
Loading 2609.37233v1…