Skip to content
Preprint

ClosureBench: A Constructive Benchmark for Compositional Graph Reasoning

Aug 2026 · 0 citations · 29 references
Computer Science

TL;DR

ClosureBench is introduced, a constructive benchmark for compositional graph-relational reasoning with programmatically verified ground truth with programmatically verified ground truth: each task's reference answer is computed by executing a program in the Ein tensor-logic language, ensuring machine-verified correctness.

Abstract

We introduce ClosureBench, a constructive benchmark for compositional graph-relational reasoning with programmatically verified ground truth. Unlike fixed-test-set benchmarks vulnerable to data contamination, ClosureBench generates instances on demand: each task's reference answer is computed by executing a program in the Ein tensor-logic language, ensuring machine-verified correctness. The benchmark spans 26 task categories at three compositional levels (L1-L3), with difficulty controlled along three independent axes: graph size, edge density, and query depth. We evaluate models from 1.5B open weights to frontier systems (o3, GPT-4.1, Gemini 2.5, Claude Sonnet 4) and report three findings. First, because the benchmark can always supply fresh instances, it measures memorisation directly: a model fine-tuned on a fixed test set shows a 19.3 percentage-point gap between its accuracy on seen and on fresh instances, which a static test set cannot reveal. We scope this to supervised fine-tuning on answer pairs, not pretraining contamination. Second, accuracy falls as graph size and query depth increase, and the two interact: models misread the graph from its natural-language description and then reason correctly over the wrong graph, so even the strongest frontier model degrades from atomic to compositional queries. This bottleneck is a property of the reasoning rather than the input format: it persists when the graph is given as a JSON edge list or an adjacency matrix instead of prose. Third, a 4B model fine-tuned to emit executable programs rather than answers stays nearly flat across compositional levels and approaches frontier accuracy (94.3% on held-out instances) at a fraction of the token cost. This holds for two program targets, Ein and Python+NetworkX, so it is a property of verified program synthesis rather than of one language.

View source

Similar papers

Preprint Jul 2026

ArbiGraph: Arbitrarily Scalable Verifiable Task Graphs for Evaluating Context Management

ARBIGRAPH is introduced, a benchmark generator for evaluating whether tool-assisted language agents can retain, update, compose, and discard task-relevant context across extended reasoning workflows, and shows that ARBIGRAPH exposes failures that are not visible from single-task evaluation alone.

Pavel Golikov, E. Opryshko, Gennady Pekhimenko et al. · 0 citations
Preprint Jul 2026

ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers

ITPEval is presented, the first benchmark for evaluating automated formal proof translation across four major ITPs (Lean 4, Rocq, Isabelle, and HOL Light), spanning two distinct logical foundations and itpeval, a unified multi-ITP verification infrastructure with state-isolated warm backends that preserve per-artifact native checking semantics.

Jiayi Wu, Robert Joseph George, Anima Anandkumar · 0 citations
Preprint Aug 2026

Evidence-Carrying Validation for Knowledge Graphs

This work presents an evidence-carrying validation interface: every selected node-shape check returns either a satisfaction trace or failure witness, and shows how programs combine passing and failing evidence to diagnose missing information and guide repair.

Gabe Fierro · 0 citations
Conference Open access 2026

From Trajectories to Graphs: Contract-Checked Editing for Verifier-Guided LLM Reasoning

Inference-time search can substantially improve LLM reasoning when tasks admit deterministic verification, but existing methods largely refine single trajectories and lack a reliable mechanism for composing partial solutions across candidates. We propose contract-checked graph editing : represent each candidate as an interface-typed reasoning DAG and validate every nontrivial edit with a deterministic structural gate (acyclicity, namespace closure, schema validity, terminal constraints) before invoking the verifier. The gate certifies runnability only and emits auditable rejection reasons; semantic correctness is determined solely by the verifier. Instantiated in Genetic Inference Search (GIS) with Qwen2.5-32B-Instruct under strictly matched token budgets (8K tokens), contract-checked grafting increases verifier-runnable recombination from 41.2% to 92.8% and improves accuracy over rStar (+6.1 on MATH, +9.1 on MATH L5) while using 42% fewer verifier calls. The same operators transfer across outer loops (beam, best-first, MCTS) and to structured generation and code, outperforming execution-guided beam search on Spider (+2.8) and improving multi-file code generation on HumanEval-MF (+9.2).

Rui Li, Shuang Cao · 2 citations