MGQL turns graph-query semantics into an executable test oracle

A benchmark can tell you whether two result tables match. It is much less good at telling you whether the query that produced them was well formed under the language standard—or whether the evaluator silently implemented a different interpretation. The OOPSLA 2026 paper MGQL attacks that layer for ISO Graph Query Language (GQL), turning a substantial read-only fragment of the standard into executable, machine-checked semantics.

That distinction matters for future natural-language-to-graph-query evaluation. GQL was standardized as ISO/IEC 39075 in 2024, but the paper says its semantics span more than 600 pages of prose. MGQL formalizes graph resolution, pattern matching, filtering, projection and composite queries over multiple graphs. Its type system tracks graph-scoped schema refinements, nullability, heterogeneous unions and list-valued bindings from quantified paths. The authors prove that well-formed queries, when evaluation completes, produce results conforming to their statically assigned schemas.

What was actually tested

The accompanying artifact is unusually auditable. Its README reports about 23,700 lines of Lean 4 across 14 modules, with no dependency beyond core Lean. It declares zero sorry placeholders and zero user-defined axioms; named results depend only on Lean’s standard propext, Classical.choice and Quot.sound axioms.

The executable suite contains 350 native_decide assertions: 276 unit assertions, 32 assertions across 30 worked examples, and 42 LDBC integration assertions. Its benchmark command runs six LDBC Social Network Benchmark Interactive v2 queries—IS1, IS3, IS4, IS5, IC8 and IC2—against a 20-node, 20-edge graph. The artifact says the executable semantics returns the expected result counts, the certified checker accepts all six queries, and the big-step evaluator agrees with the small-step engine.

Those are conformance checks, not a claim that MGQL covers real production scale. Six queries on a tiny graph do not measure throughput, robustness to generated syntax, or model accuracy. They show that the formal rules are executable and that selected query shapes pass through both evaluation engines and the certified type checker.

How to use it in a benchmark

A serious text-to-GQL suite should separate three outcomes:

1. Static validity: does the generated query type-check against the declared graph schema?
2. Semantic conformance: does execution follow the supported GQL rules for nulls, bags, paths and composite queries?
3. Task correctness: does the final result answer the natural-language request?

MGQL can support the first two layers for its formalized fragment; it does not replace the third. It also should not be advertised as a complete GQL oracle: the paper explicitly describes a substantial read-only fragment, not the entire standard.

That boundary is the useful result. Instead of collapsing parser acceptance, language conformance and answer accuracy into one pass/fail number, benchmark authors now have an executable reference point for testing the query semantics themselves.