Posted by GuyHaworth (Profile) on February 02, 2003 at 22:48:43:
In Reply to: Mathematical Proof of Tablebase Accuracy posted by Mike Hood on February 02, 2003 at 21:41:03:
It's an interesting queston and one that I posed in 1969 about programs
generally. It turned out to be about 30 years too early to be asking such
questions.
Ken Thompson's Turing_Award lecture of some years ago points up the
difficulties. He did so by talking about how he could insert 'his own code' at
any level of the computing system architecture ... compiler, linker, loader etc.
Even if you prove the computation correct at one level, you are taking as
axiomatic that the system 'up to that level' is correct in principle and will
function correctly in practice.
In the particular case of the EGT-computations, one can prove mathematically
that there is a finite-step, terminating algorithm for producing the EGT.
Curiously, I have never seen this proof in the most general terms which would
admit a variety of definitions of depth.
But, did the computations faithfully execute the algorithm. Not always. The
only way to check the results is to compare them with those of an independent,
second-source ... not as easy as it sounds.
The same principle applies whenever the results are not self-evidently correct:
Mersenne Number computations in GIMPS, Proofs of the 4CC, ...
Re EGTs, mistakes have still happened at generation time and runtime:
1) Most recently, FEG missed inhering shallow wins from subgames (e.g. KNNK)
Fortunately, Marc Bourzutschky tripped over an incorrect EGT-value
A self-consistency check would have found the error, but was not run.
[ Now the bug has been corrected .. and notified to all. ]
2) Files have been corrupted after being verified correct.
Stray neutrons - who knows? MD5SUM-checks (or equivalent) spot this.
My chess-engine spots corrupt files on initialisation: no idea how.
3) Underpromotions have occasionally been ignored or forgotten
That's a case of unwittingly changing the rules of the game.
4) Access-software for the EGT has occasionally been corrupt
So the EGT is ok, but the wrong result is returned nevertheless
A checkers game was lost in 2002 this way: see ICGA_J v25.3 (Sept)
In practice, EGT results have been checked, not always end-to-end, by these
means:
1) list of max-depth positions have been 2nd-sourced (for the same metric)
2) lists of mzugs (regardless of metric) have been second-sourced
3) where 'Nalimov-style' DTC(onversion) EGTs have been produced two ways
they have been compared at the binary level
4) different EGTs should show the same wins, draws and losses
an API to the EGTs is always helpful to facilitate this
Given the above list, you might well choose not to resign, even if the computer
says "mate in N".
However, given the way the Nalimov DTM EGTs are produced, I personally have more
confidence in their correctness than in a lot of other software on which my life
depends < put your own list here >.
Even so, there is probably still one dodgy (KBPKN) stats file on Rob's site - no
doubt a victim of a file-management error years ago. But that's a derived
result, and I'm the KBPKN EGT itself is fine.
g