Ten thousand steps of reasoning, every one written down and checked.
deep-taxonomy-10000.py · output · proof · check · try it in the playground
A taxonomy is a tree of categories: a robin is a bird, a bird is an animal, and so on. Here the tree is ten thousand levels deep, and at every level it also splits into two side branches that go nowhere.
We know one thing: an individual, 'ind', is in the top category 'n0'.
Is 'ind' in category 'n10000', at the very bottom? And can the computer
show all ten thousand steps — and have them checked?
This is the deep-taxonomy benchmark, a standard stress test for reasoners. The collection has it at four depths, and this is the largest:
| Example | Levels | Proof steps |
|---|---|---|
| deep-taxonomy-10 | 10 | 11 |
| deep-taxonomy-100 | 100 | 101 |
| deep-taxonomy-1000 | 1000 | 1001 |
| deep-taxonomy-10000 | 10000 | 10001 |
Same shape each time; only the length of the chain changes.
One fact, then three rules per level — 30,000 rules in all:
fact(type('ind', 'n0'))
implied_by(type(X, 'n1'), type(X, 'n0'))
implied_by(type(X, 'i1'), type(X, 'n0'))
implied_by(type(X, 'j1'), type(X, 'n0'))
implied_by(type(X, 'n2'), type(X, 'n1'))
# … and so on, down to
implied_by(type(X, 'n10000'), type(X, 'n9999'))
implied_by(type(X, 'i10000'), type(X, 'n9999'))
implied_by(type(X, 'j10000'), type(X, 'n9999'))
query(type(X, 'n10000'))
Read implied_by(type(X, 'n2'), type(X, 'n1')) as anything in n1 is also in
n2. The i and j rules are the dead-end side branches. The last line asks
the question.
type('ind', 'n10000')
One answer: yes.
peye works backward from the question (implied_by rules are explored only
when a question needs them): to be in n10000, be in n9999; to be in
n9999, be in n9998; … all the way up to the fact we gave. The search is an
explicit machine inside peye, so ten thousand levels deep is no problem.
The proof is a chain of 10,001 steps:
'ind' is in 'n0' — a fact we gave (fact 1).'ind' is in 'n1' — rule 2.'ind' is in 'n2' — rule 5.'ind' is in 'n10000' — rule 29999.Each step names the exact program line it used. The 20,000 side-branch rules never appear: they do not help answer the question.
A separate checker read all 10,001 steps against the program and confirmed that:
Verdict: checked. All 10,001 steps verified, and nothing taken on trust.
The source is about 1.3 MB and its proof about 1.4 MB: a proof records every step it claims.
python -m peye examples/deep-taxonomy-10000.py # the answer
python -m peye --stats examples/deep-taxonomy-10000.py # and its cost
--stats reports "inferences": 10001 — one step per level, plus the fact.
Or open it in the playground.
Change the last line to query(type(X, 'j5000')) and run with --stats
again: the answer is type('ind', 'j5000'), a side branch halfway down,
reached in 5001 steps.
Going from ten levels to ten thousand changes the cost, not the kind of answer. Time, proof size and checking all grow in step with the depth, so a ten-thousand-step argument is just as followable — and just as checkable — as a ten-step one.