From: Bill Dubuque Newsgroups: sci.math Subject: brute-force vs. intuition [was: NY Times (10 Dec) report on Larry Wos's achievement] Date: 16 Dec 1996 16:17:38 -0500 Organization: MIT Message-ID: References: <58krc3$ltj@newsflash.concordia.ca> 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 >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.