yuiseki/geo-triples-tokyo23

geo-triples-tokyo23

510,616 spatial triples, 483,922 text rows and 8,890 evaluation questions, computed from two frozen, openly-licensed sources by an oracle with no model and no network in the loop. Same input and same versions, same Parquet, byte for byte.

Three things are kept apart throughout, in the data and in this card. YuisekinGeoSPARQL observes: it reads a DE-9IM matrix off two published geometries. LeanGeospatial certifies: it proves what a matrix entails and what the RCC8 composition table allows. This repository derives: it turns the two into triples and sentences. A row says which of the three it is, and never borrows one's confidence for another.

Nothing here was generated by a language model. Every sentence is a template from src/vocab.py filled with two names, and which template applies is decided by a DE-9IM matrix computed from geometry.

from datasets import load_dataset

triples = load_dataset("yuiseki/geo-triples-tokyo23", "triples", split="train")
cpt     = load_dataset("yuiseki/geo-triples-tokyo23", "cpt", split="train")
probe   = load_dataset("yuiseki/geo-triples-tokyo23", "probe", split="train")

Where it comes from

tokyo23-poi is one feature per Wikidata id: 3,740 mapped as areas, 3,485 as points, and 63 mapped both ways where the area is kept. The 23 wards' own ids are excluded, because a ward is also a place node at its centre and would otherwise be a place inside itself.

12,142 features make 147,416,022 ordered pairs. 24,114,442 of them are formed and 51,436 of those are not disjoint. The places are compared against the wards and against nothing else: 7,265 places against each other is a different dataset with a different cost, and the question they were added for is which ward a place is in.

A pair that was formed and is absent is disjoint, and how that is spelled depends on the kinds: FF2FF1212 for two areas, FF0FFF212 for a point against an area. A pair that was never formed is absent for a different reason and says nothing. The oracle's manifest carries both the table and the list of which layers were compared.

The oracle is YuisekinGeoSPARQL, which loads the sources into Apache Jena Fuseki 6.2.0 and compares GEOS through shapely against JTS inside Jena, pair by pair, for all eight Simple Features predicates. Two implementations of one standard agreeing is evidence; one agreeing with itself is not.

The triples subset

346,256 rows: 126,208 true and 220,048 false.

One row per observed pair per predicate, so eight rows per pair, 293,552 in all. The predicates that hold are true and the rest are false, and the truth of all eight comes from one matrix, which is in the de9im column of every row. Negatives are chosen this way so that no sampling rule can be argued with: nothing was selected, and a reader who disagrees with a false has the evidence in the same row.

More than one Simple Features predicate holds of a pair. Two equal areas are sfEquals, sfIntersects, sfWithin and sfContains at once. The exclusive reading is the rcc8 column beside them, where exactly one of eight relations holds.

Not for every pair, though. RCC8 is a calculus of regions, and a place mapped as a node is a point, so 6,898 rows have an empty rcc8 and their Simple Features columns are the whole reading. The kinds are columns for the same reason: sfOverlaps needs both operands to have the same dimension, and sfCrosses needs them to differ in a fixed argument order.

What is proved, and what is only observed

All 510,616 rows are certified, and it is worth being exact about what that does and does not cover.

What is proved is the step from a matrix to a predicate. Given matrix FF2F11212 over two areas, LeanGeospatial derives sfTouches and refutes the other seven; the verdicts for all 22 matrices this data produces, 176 in all, are vendored in vendor/de9im_sf_verdicts.tsv with the revision that produced them. The build reads that file and stops if a verdict disagrees with what the oracle read. None does. For a composed row, what is proved is the cell: EC x NTPPi entails DC and nothing else, in the table table_eq_published shows equal to the machine-checked one.

The kinds are part of the question. sfCrosses between an area and a point is not one of the cases SFA lists, and the prover refuses it even though the matrix of a ward holding a point matches the pattern perfectly well. Asking without the kinds would have shipped every ward crossing every place inside it.

What is not proved is the matrix itself. That two geometries relate as FF2F11212 is a measurement made by GEOS, checked against JTS, on vertices that Natural Earth and OpenStreetMap published. No theorem covers it, and the certification column does not claim otherwise. Nor is the RCC8 label of a composed row's premises proved: those are observations that the proved cell was applied to.

Lean is not a dependency of the build. Regenerating the verdicts needs it; reading them does not, which is why they are a vendored file rather than a step.

True triples, by predicate

This is lopsided and the shape is worth reading before using it.

sfDisjoint is 45% of all true triples and every single one is a deduction. No observed row is disjoint, because the oracle only writes pairs that are not. sfCrosses is never true, because SFA gives it no area/area case at all and every feature here is an area; it stays in the table as eight thousand honest negatives rather than being dropped.

The rcc8 column over the 51,436 observed pairs: EC 26,906, NTPP 5,134, NTPPi 5,134, PO 3,140, TPP 2,083, TPPi 2,083, EQ 58, and 6,898 with none because a point is not a region.

Composed rows, and which cells they use

99,128 rows have derivation = composition. They are not extra observations: for each, two known relations through the feature in via_id left the composition table with exactly one possible relation, and that is what the row records. Cells where the table leaves several entail nothing and produce no row. At most one row is kept per ordered pair, since a pair reachable through many intermediates would otherwise repeat itself.

Coverage of the 64 cells is very uneven, and assuming otherwise would be the easiest mistake to make with this subset. Four cells are used, in two converse pairs:

91% of them are one shape of argument: a country borders another country, that country contains a state, therefore the first country and that state do not meet. The two NTPP cells are what the places brought, and they are the interesting ones: a place is in a ward, the ward is in a country, therefore the place is in that country.

9,326 rows are conclusions about pairs the oracle never formed. The places are compared against the wards only, so nothing measured Sensoji against Japan; the composition table settles it anyway, and those rows carry an empty de9im rather than a matrix nobody read. They are the rows that reach past what was measured, which is what a composition table is for.

Anyone wanting broad coverage of RCC8 composition should generate it from the prover requests instead, where 27 of the 64 cells are exercised; see below.

The composition table is vendored from LeanGeospatial, whose theorem table_eq_published shows its machine-checked table agrees with the published one on all 64 cells. The build stops if any composed row contradicts what the oracle observed. None does.

The cpt subset

483,922 rows, 82,510,457 characters. One row per true triple per form.

The text is layered, and each layer takes the triple as its input:

a triple -> an N-Triples line, for every true triple -> a sentence, only where both features have a label in that language

The N-Triples form is unconditional, which is the point: the coverage gap is a missing ja row beside a present ntriples row, visible by counting, rather than a choice made silently during the build. The IRIs are the ones the oracle's published graphs use.

<https://yuiseki.net/geosparql/tokyo23/ward-3554304> <http://www.opengis.net/ont/geosparql#sfTouches> <https://yuiseki.net/geosparql/tokyo23/ward-1758947> .

Shinagawa borders Ota.
品川区は大田区と接している。

A composed row carries all three statements, in all three forms, because a conclusion on its own is indistinguishable from one more observation:

Afghanistan borders People's Republic of China. People's Republic of China contains Qinghai. Therefore Afghanistan and Qinghai do not meet.
アフガニスタンは中華人民共和国と接している。中華人民共和国は青海省を含む。したがってアフガニスタンと青海省は接していない。

Why the three forms do not have the same number of rows

202,116 N-Triples lines, 150,666 Japanese sentences, 131,140 English ones.

51,436 true triples are sfIntersects, which holds of every observed pair and says almost nothing. Along with sfCrosses it is kept in the triples table and in the N-Triples form and is never spoken, because a corpus full of "A and B intersect" teaches a model to produce filler. That accounts for the whole gap in Japanese but 14 rows.

Those 14 involve one of seven Natural Earth features that carry no label in any language: the _99_ remainder polygons of Anguilla, Antarctica, Colombia, Kiribati, Mexico, Russia and Venezuela.

The English gap is 19,540, and it is a fact about OpenStreetMap rather than about this build: a place in Tokyo usually carries name:ja and often carries no name:en. A feature with no label in a language gets no sentence in that language, rather than a romanisation passed off as that language, which is why this is the one dataset here where Japanese is the larger half.

How a place is worded

A point is not contained in a ward the way a smaller area is, so the two predicates that can hold between a point and an area have wording of their own.

浅草寺は台東区にある。            Sensō-ji is in Taito.
台東区には浅草寺がある。          Taito has Sensō-ji.
高千穂大学は杉並区に含まれる。     Takachiho University is within Suginami.

The third is an area, so it keeps the area wording. Everything else involving a point is left unspoken rather than worded by analogy: a point on a ward boundary does touch it, and saying so takes a sentence about boundaries that nobody asked for.

Two things the sentences will say that read oddly

520 true rows name the same thing on both sides, giving sentences like "Aruba contains Aruba." and "アルバはアルバを含む。". Natural Earth's admin-0 and admin-1 layers both carry a feature for a country that has one state, and they are distinct features with the same label. The N-Triples form distinguishes them by IRI; the sentence cannot.

40.7% of ne-admin1 features are not geometrically within the country they name. The median outside_ratio is zero: this is the same border drawn twice, independently, with the vertices landing in slightly different places, not a geographic fact. Five states differ by more than 10% and all five are islands or a divided country: Coral Sea Islands, Alo, Niuas, Nicosia, Pohnpei.

Those pairs are PO, so the sentence says they overlap without either containing the other. That reading is kept, unchanged, because the whole dataset records what the two published geometries say rather than what a person knows about the world, and outside_ratio is in the row so a reader can tell a real overlap from a sliver. Anyone who wants the geographical reading should use the oracle's normalized column instead of rewording these.

The probe subset

8,854 questions, 8,847 of them answerable in Japanese. Which parent does this place have, at each level of the hierarchy the sources describe.

Every answer in this subset is stated in `cpt`. It measures whether training put these facts into a model, not whether the model generalises to places outside the corpus. A number from it is a recall number and should be reported as one. The set is here, rather than in a separate repository, because pretending to independence it does not have would be worse than saying this: it comes from the same triples, the same revisions and the same digest as everything else, so there is one thing to pin.

The parent comes from the layers, not from the geometry. Natural Earth's admin-0 and admin-1 draw the same coastline twice and the vertices disagree, so only 21 of Japan's 47 prefectures are geometrically within Japan while all 4,596 states resolve by attribute. A probe built on sfWithin would be scoring a model against that artefact. 686 of these rows are PO for exactly that reason.

A child that meets two parents is dropped, which is why 17 wards are asked about and not 23: six of them touch Chiba as well as Tokyo.

A child whose name does not pick it out is dropped too. 21 of the places are called 天祖神社 and they are in different wards, so "which ward is 天祖神社 in" has 21 answers and any one of them scores a model on a coin toss. The same rule removes 185 states that share a name with another state. Dropped rather than disambiguated: a name plus a ward would be a question containing its own answer.

36 questions contained their own answer and are gone. 千代田 is a place inside 千代田区, and Aruba is a country whose one state is also called Aruba. Matched on the label rather than on the relation, because the country cases are EQ and the ward cases are not, so an RCC8 filter catches one kind and leaves the other.

For scale, 120 questions per level with three worked examples in front of each, asked as a completion rather than through a chat template:

Three things are worth reading off that table. ward-in-state is saturated at both sizes and should be read as a sanity check rather than as a score: there are 16 questions and the answer to every one of them is 東京都.

place-in-ward is nowhere near saturated at 35B, which is where there is room to move.

And the language gap reverses between levels. Countries are easier to name in English; places in Tokyo are easier to name in Japanese, by 8 points at 35B and by 12 at 0.6B. That is the same fact as the name:en gap above, seen from the other side.

The protocol matters more than it looks. Asked cold, a base model continues the question instead of answering it; wrapped in the chat template it ships with, it does the same. Both read as 0% and neither is about geography.

What this is for, and what is not known about it

The target it was built against is a model that cannot answer "which prefecture is Matsuyama in": 2.0% on gemma-3-270m against 83.6% on a 35B model. Small models do not carry administrative geography, and a fine-tune teaches the shape of an answer rather than the geography, so the model writes a well-formed place that does not exist.

The place-in-ward level is the closest this dataset gets to that failure. 7,265 named places in Tokyo, each in exactly one ward, in a corpus that says so in three forms.

N-Triples text teaches IRI patterns and the shape of a GeoSPARQL statement. Whether that transfers to a Japanese question asked in ordinary words is an open question. It has not been measured here, and the card would rather say so than imply either answer. That is also why all three forms sit in one table with a form column: they can be weighted, or one of them dropped, without rebuilding anything.

Reproducing it

The code that builds this is at yuiseki/geo-triples-tokyo23.

git clone https://github.com/yuiseki/geo-triples-tokyo23
git clone https://github.com/yuiseki/YuisekinGeoSPARQL
cd YuisekinGeoSPARQL
docker compose up --build

cd ../geo-triples-tokyo23
python3 src/build.py \
    --relations ../YuisekinGeoSPARQL/data/relations.tsv \
    --oracle    ../YuisekinGeoSPARQL/data/manifest.json \
    --out data
python3 -m pytest

data/manifest.json records the digests:

The oracle is run without --normalize snap. That flag adds three columns this build does not read, and nothing else, but it changes the digest of relations.tsv that the manifest records as the input.

Two builds of the same input produce identical bytes, and the test suite demonstrates it by running the build twice in separate processes, one of them with a randomised hash seed, and comparing. Parquet bytes belong to the writer as much as to the data, so the digests above hold for pyarrow 20.0.0 with zstd, which the manifest also records. The build refuses to run if the oracle's manifest does not describe the files on disk.

Prover requests, and regenerating the certificates

src/prover_requests.py turns the oracle's relations.tsv into the JSON Lines that LeanGeospatial's prover reads, so a composition claim can be checked against a machine-checked table rather than against this repository.

python3 src/prover_requests.py \
    --relations ../YuisekinGeoSPARQL/data/relations.tsv \
    --out data/prover/triples.jsonl \
    --claims-out data/prover/claims.jsonl --limit 0

lean-geospatial-prover < data/prover/triples.jsonl > verdicts.jsonl

src/certify.py does the claims half of this and keeps the answers:

python3 src/certify.py \
    --relations ../YuisekinGeoSPARQL/data/relations.tsv \
    --prover ../LeanGeospatial/.lake/build/bin/lean-geospatial-prover \
    --lean ../LeanGeospatial

It rewrites vendor/de9im_sf_verdicts.tsv, which is what fills the certification column, and refuses to write a file whose verdicts contradict the oracle.

699,002 triples and 176 distinct matrix-and-kinds-and-claim pairs. Over the full set, the table allows the observed relation 646,290 times, allows only one and it is the observed one 52,712 times, exercises 27 of the 64 cells, and contradicts nothing. These files are not published as part of the dataset; they are a check, and they are large.

Licence

ODbL-1.0. The sentences too.

The licence of the result is the strictest of the sources loaded, and share-alike is contagious: one ODbL source makes the whole derived database ODbL whatever else is in it. A sentence here is an extraction from OpenStreetMap geometry, not a description of it, so a corpus containing these sentences is a Derivative Database and carries ODbL.

(c) OpenStreetMap contributors, available under the Open Database License. https://www.openstreetmap.org/copyright

Made with Natural Earth. Free vector and raster map data @ naturalearthdata.com

See ATTRIBUTION.md, which sets out the ODbL position in full and says why it matters when mixing sources. The code in src/ and tests/ is MIT.