Subject: brute-force vs. intuition [was: NY Times (10 Dec) report on Larry Wos's achievement]
From: Bill Dubuque <[email-masked]>
Date: 16 Dec 1996 16:17:38 -0500
Newsgroups: sci.math

The following old post of mine on brute-force vs. intuition is relevant.
Nothing new needs to be said -- even in light of the recent automated 
proof of Robbins conjecture.
 
		    The Beauty of Chess is Skin Deep
		but the Beauty of Math is Infinitely Deep

Summary: some thoughts on intuition vs. brute-force in chess and math,
motivated by recent discussion of intelligence in chess in the newsgroup 
comp.ai.philosophy (after the ACM Challenge: Deep Blue vs. Kasparov).

 >From: Drew McDermott <[email-masked]>
 >Newsgroups: comp.ai.philosophy
 >Subject: Deep Blue and Intelligence
 >Date: Mon, 19 Feb 1996 12:37:20 -0500
 >
 >The New York Times ran a post-mortem of the Deep-Blue-Kasparov chess 
 >match today, quoting various notables (Simon, Searle, Hofstadter, 
 >Gelernter, and others) on the question of whether the machine was 
 >"really" intelligent.  Simon said it was, but the consensus among most 
 >of the others was that Deep Blue's relative success merely indicated 
 >that chess, contrary to expectation, requires no intelligence. ...

I conjecture that optimal chess play is essentially random and 
of complexity far transcending human comprehension. I base this
conjecture on recent detailed analyses of endgame strategies made
possible via the construction of gigabytes of endgame databases.
These databases supply exact game-theoretic values (win/loss/draw)
and optimal move sequences for small-men endgames (e.g. Ken
Thompson distributes CD's for five-men endgames). Such perfect
information has motivated a reanalysis of the classical
human-derived endgame strategies with a surprising result that
optimal play often violates human heuristics and further may be
so complex in general that it is beyond the grasp of mere mortals.
Grandmasters have had severe difficulties playing against these
endgame databases.  Optimal play is so complex that in one case 
a recognized endgame expert (Roycroft) was able to comprehend a
certain endgame database only with enormous effort and the aid
of automated inductive-learning algorithms [Her] [Kop] [Mic].
See the Appendix below for an example of such complexity.
If the endgame holds such complexity then human comprehension of
optimal middlegame (and entire game) strategy is surely hopeless.

Such results seem to indicate that chess is random from a resource-
based Kolmogorov complexity point of view; i.e. probably it is not
possible to abstract from optimal play some structured general
strategy because deep tactics may produce exceptions to all human 
comprehensible plans and strategies -- a huge endgame database itself 
may be the shortest possible description of the optimal strategy.

If this turns out to be true, then human strategies will only be
useful against humans -- deeper searching programs will be able to
refute shallow human strategies. I think that we have already
begun to see some of this in the recent ACM match between
Kasparov and Deep Brute. In the long run it may prove impossible
for humans to comprehend the deep random variations that chess
programs compute as optimal. There may be no flowing themes, just
random forced tactical considerations that stem from deep
searches -- perhaps the beauty of human chess lies only skin deep.

It is important to keep in mind that such brute-force game tree
searching fails miserably once one turns attention to games with
bushier trees, e.g. the game of Go (cf. [Nie] for an excellent 
survey on exhaustive search). Human ingenuity still reigns supreme
navigating bushlands in these combinatorially exploding jungles

The same holds true of brute-force tree searching in many other
domains, e.g. theorem proving in mathematics. For example,
recently there has been a flurry of research applying effective
techniques in algebra towards proving elementary theorems in
geometry [Kap]. Thus we now know algorithms that automatically
decide the truth of theorems in elementary Euclidean geometry of
the sort one encounters in high-school, e.g. Appolonius' Circle
Theorem (cf. Appendix below). Such proofs proceed by brute force
calculation instead of geometric intuition, lemmas, analogies,
and all the other techniques that are the common arsenal of the
geometer. Do such algorithms herald the death of geometry?  Of
course not, for such algorithms provide absolutely no insight
whatsoever into the structure of a proof -- they churn and grind
and leave us with a solitary bit of truth just as the chess
endgame database leaves us with a win/lose/draw result but no hint
whatsoever of any plan or strategy. But the importance of a proof
or chess game lies much deeper than its result: it may herald the
discovery of a new idea with widespread application or it might
be a prototypical illustration of a general theme, etc -- the
possible utilities are endless. The importance of Wiles proof of
Fermat's Last Theorem stems not from its truth value but rather
from the application of its methods to the Taniyama-Weil
conjecture and its consequent role in the Langlands program --
a major research theme in contemporary mathematics. On the other
hand, the brute-force proof of the four-color theorem contributes
merely a single bit of information to mathematical knowledge.

As another mathematical example I mention a theorem of Jacobson: 
a ring is commutative if for every element x there is an integer
n > 1 such that x^n = x. Although this theorem may be proved
automatically for small n by existing brute-force equational
completion-based theorem provers, the general case is thought to
be far out of reach [BL,KZ]. Jacobson's marvelous proof is an easy
corollary of his deep structure theory for rings, a structure
theory which is a prime example of the modern axiomatic method
and structuralistic trend in twentieth-century mathematics. Such
deep and beautiful triumphs of human ingenuity will never be the
result of pure brute-force, no matter how Deep the Brute. The
beauty of chess may lie only skin deep but the beauty of math
transcends even transfinite mechanical depths (as we know from
the deep work of Goedel, Turing, and Feferman [Fe1] [Fe2] [Fe3]).
Long live ingenuity!

-Bill Dubuque

Appendix

"With the relatively small queen-versus-rook ending it is not impossible
that a human could eventually understand, explain and perhaps even
master for his own use the bizarre intricacies of machine play. But
only a small step up the ladder of complexity, to queen and pawn (on
g7) versus queen, is sufficient to exceed such a possibility.
Komissarchik and Futer [1974] built an exhaustive database for this
ending. A computed minimax-optimal strategy takes the white king on a
labored and mysterious journey, circumnavigating the board more than
once, before the preconditions for safe pawn promotion are finally
established. Figure 15.3 from Komissarchik and Futer [KF] 1974 is
reproduced below. Roycroft comments on "... the white king's contorted
peregrinations throughout the solutions full length". Qualified
students of this result believe that human insight into the detailed
rationale is unlikely to be attainable [Roy] 1986."

					--excerpted from [Mic], p. 247	

          Figure 15.3: A king's labored and mysterious journey.

+-----------------------------------------------------------------------+
|        |        |        |        |        |        |        |        |
|        |     -------     |        |        |        |   -----------+  |
|        |   /    |    \   |    |\  |        |        |    \   |     |  |
|        | /      |      \ |    |  \|        |        |      \ |     |  |
|--------/--------+--------\----|---+\-------+--------+--------\-----|--|
|      / |        |        | \  |   |  \     |        |        | \   |  |
|    /   |        |        |   \|   |   |    |        |   WP   | /   |  |
|    \   |        |        |        |   |    |    |\  |        /     |  |
|      \ |        |        |        |   \    |    |  \|      / |     |  |
|--------\--------+--------+--------+-----\--+----|---+\---/---+-----|--|
|        | \      |        |   -------------\------------\---+ |     |  |
|   ---------\    |        |  WK    |        |\   |   | +-- -|-|-----+  |
|    \   |        |        | start  |        |  \  \  | |    | |/|      |
|      \ |        |        |        |   --------\ \  \| |    |/| |      |
|--------\--------+--------+--------+---|----+----\-\--\|---/|-+-|------|
|        | \      |        |        |   |    |      \ \ |\/  | | |      |
|        |   |    |        |        |   |    |        \      +---+      |
|        |   |    |        |        |    \   |        | \      |        |
|        |   |    |        |        |      \ |        |  /     |        |
|--------+---|----+--------+--------+--------\--------+/-------+--------|
|        |   |    |        |        |        | \     /|        |        |
|        |   |    |        |        |        |   \ /  |        |        |
|        |   \    |        |        |        |   / \  |        |        |
|        |     \  |        |        |        |   |   \|        |        |
|--------+-------\+--------+--------+--------+---|----+\-------+--------|
|        |        |\ WK end|        |        |   |    |  \     |        |
|        |        |  \ \   |        |        |   |    |    \   |        |
|        |        |    \ \ |        |        |   |    |      \------    |
|        |        |      \ \        |        |   |    |        |  /     |
|--------+--------+--------\-\------+--------+---|----+--------+/-------|
|        |        |        | \ \    |        |   |    |       /|        |
|        |        |        |   \ \-----\     |   |    |     /  |        |
|        |        |        |     \  |    \   |   /    |   /    |        |
|        |        |        |       \|      \ | /      | /      |        |
|--------+--------+--------+--------+\-------/--------/--------+--------|
|        |        |        |        |  \   / | \    / |        |        |
|        |        |        |        |    /   |   \/   |        |        |
|        |        |        |        |        |        |        |        |
|        |        |        |        |        |        |        |        |
+-----------------------------------------------------------------------+

APPOLONIUS' CIRCLE THEOREM: The altitude pedal of the hypotenuse of
a right-angled triangle and the midpoints of the three sides of the
triangle lie on a circle; i.e. in the figure below, the pedal point
H lies on the circle determined by the midpoints EFG.

       B (0,b)  #
                #  # 
                #     #
                #        #  H (h,j)
                #           *    
                #      *    #  #   *
                #  *       #      # 
                #         #          #  F (f,i)
       G (0,g)  *        #              *
                #       #                  #
              * #      #                      # 
                #     #                          #
             *  #    #       * M (c,d)     *        #
                #   #                                  #
             *  #  #                                      #
                # #                       *                  #
              * #                                               #
                ########################*##########################
       C (0,0)    *                     E (e,0)                    A (a,0)
                       *            *
                              *

(Hypotheses)
h1 := 2 e - a = 0		(E is midpoint of CA)
h2 := 2 f - a = 0		(F is midpoint of AB, 1st coordinate)
h3 := 2 i - b = 0		(F is midpoint of AB, 2nd coordinate)
h4 := 2 g - b = 0		(G is midpoint of BC)
h5 := (c - e)^2 + d^2 - (c - f)^2 - (d - i)^2 = 0  (length EM = length FM)
h6 := (c - e)^2 + d^2 -  c^2      - (d - g)^2 = 0  (length EM = length GM)
h7 := (h - a) b + a j = 0	(H lies on AB)
h8 := - a h + b j = 0		(CH is perpendicular to AB)

(Conclusion)
Z  := (c - e)^2 + d^2 - (c - h)^2 - (d - j)^2 = 0  (length EM = length HM)

Appolonius' Circle Theorem is equivalent to the proposition

P(a,b,c,d,e,f,g,h,i,j) :=
 for all real numbers a,b,c,d,e,f,g,h,i,j:
  if    h1, h2, h3, h4, h5, h6, h7, and h8 = 0
  then  Z = 0

References

[BL] Burris, S., Lawrence, J.  Term rewrite rules for finite fields.
Int. J. of Algebra and Computation, vol. 1, No. 3 (1991) 353-369.

[CCC] Computers, Chess, and Cognition, T. Anthony Marsland and 
Jonathan Schaeffer (ed.), Springer Verlag 1990.

[CL]  Computational Logic: Essays in Honor of Alan Robinson,
J. Lassez and G. Plotkin (ed.), MIT Press, 1991.

[Fe1] Feferman, S. Transfinite recursive progressions 
of axiomatic theories. Journal of Symbolic Logic, 27 (1962) 383-390.

[Fe2] Feferman, S. Turing in the land of O(z).  In (R. Herken, ed.),
The Universal Turing Machine: A Half-century Survey, pp. 113-147.
Oxford University Press, 1988.

[Fe3] Feferman, S. Penrose's Goedelian Argument: A Review of _Shadows 
of the Mind_ by Roger Penrose. PSYCHE: an interdisciplinary journal of 
research on consciousness 2(7), May 1995. (Symposium on Roger Penrose's 
_Shadows of the Mind_).
http://psyche.cs.monash.edu.au/volume2-1/psyche-95-2-07-shadows-5-feferman.html
ftp://ftp.cs.monash.edu.au/psyche/v2-1/psyche-95-2-07-shadows-5-feferman.txt

[Her] Herschberg, I.S. et. al., Verifying and Codifying
Strategies in a Chess Endgame, [CCC], 183-196.

[Kap] Geometric Reasoning, Deepak Kapur (ed.), MIT Press, 1988.

[KZ]  Kapur, D. and Zhang, H., A Case Study of the Completion
Procedure: Proving Ring Commutativity Problems, [CL], 360-394.
See also [BL], and references therein.

[KF]  Komissarchik, E.A. and A.L. Futer, Computer Analysis of a
Queen Endgame, Journal of the International Computer Chess
Assoc., vol. 9 (1986) no. 4, 189-198.

[Kop] Kopec, D., Advances in Man-Machine Play, [CCC], 9-32.

[Mic] Michie, D., Brute Force in Chess and Science, [CCC], 239-258.

[Nie] All the Needles in a Haystack: Can Exhaustive Search Overcome 
Combinatorial Chaos? 
http://nobi.ethz.ch/febi/ex_search_paper/paper.html

[Roy] Roycroft, A.J., Queen and Pawn on b7 against Queen, in booklet
no. 7 of "Roycroft's 5-Man Chess Endgame Series", Chess Endgame
Consultants and Publishers, London, England.