FLOC and Urban

I went to FLOC, Federated LOgic Conferences, in Oxford, just for one day, Friday 13th July.  It turned out to be a lucky day.  I did most of a "Summit on Formal Methods meets Machine Learning", without winning any jackpots.  Maybe I missed the best bit, I ducked out towards the end to see "Three Research Vignettes in honour of Mike Gordon".

The only thing which stood out for me, to take away from the "summit", was a little snippet about progress on SAT solvers in the first decade of this century.  That they improved by two orders of magnitude, just from algorithmic improvement (not from hardware acceleration).  With which, in my head I wove a little story about why we should not use neural nets for everything, even if we might, perhaps, in principle.  Why did I need that little story?  Well, because I'm talking  about "Cognitive Architecture", and what I have to say probably needs to sound a lot like GOFAI (good old fashioned AI), even though I do recognise many places in the architecture where neural nets are desirable.  So I want ways of defending a GOFAI/ML/DL hybrid monster.  It shouldn't need a defence, but in some quarters anything with a whiff of GOFAI is non-PC.

After the tribute to Mike Gordon there was a reception.  At the reception I met Josef Urban, whose work I had been aware of, as much to my liking, particularly in direction and breadth of vision.  That was probably the most important thing which happened to me at FLOC 2018.  I can tell that, because I have been reviewing his ideas, and I am now intent on orienting the account I am trying to give of my own ideas so that its relation to Urban's ideas is clear.

In this post I will sketch explicitly some of the connections.

My starting point is dreams and vision.   Urban cites "three semantic dreams".  Semantics is a particular emphasis in his writing, and though I to attach great strategic importance to (formal) semantics, I have not yet well understood the role which semantics plays in Urban's ideas.

The "semantic dreams" are:

 (i) The dream of general Artificial Intelligence, and in particular AI that helps with general scientific reasoning and research.
(ii) The dream of Automated Reasoning, and in particular Automated Theorem Proving that could attack nontrivial mathematical theorems.
(iii) the QED dream, of all of mathematics (and perhaps also programming and all exact sciences backed by mathematics) being done in a form that is fully understandable to computers, verified for correctness by computers, and assisted in various semantic ways by computers.

which might compresses down to AI/AR/QED, noting however that no mention is made of "common sense", the whole endeavour is scientifically oriented.  So as far as AI is concerned it would for most observers fall short of the (present) holy grail of "general Artificial Intelligence", GAI.

Urban's vision is not a mere amalgamation of these.  His describing these as "semantic dreams" adds a perspective or emphasis which I have not previously seen, and he quickly expands out on the dreams in the following way:

 My basic motivation is the dream of scientific AI. I cannot imagine any other future than the one in which computers will to a very large extent semantically understand, assist, and develop not just mathematics and computer science, but also physics, chemistry, biology, medicine, engineering, economics, law, politics, etc.

 In his "dreams" Urban is clearly talking about important ideals rather than visionary people, and it is clear that he does have some distinguished visionaries in mind (notably Leibniz, perhaps John McCarthy) who don't appear because that's not what his list is.

I think of myself as engaged in a contemporary sequel to the ambitious projects of three prior philosophers, Aristotle, Leibniz and Carnap, all of whom I have seen as visionary advocates for deductive reason in its broadest application and the automation of reason.

These two triples of inspiration are complementary.  So it is of interest, looking in greater detail, to see how Urban's ideas and my own fit together, and to consider what kind of synthesis from them might be possible.

Urban uses the words "semantic", "understanding" and "reason".  I like to talk about the "deductive paradigm", and the "deductive/computational paradigm shift" which have a lot to do with semantics and reason.  In my next blog post I will talk about these ideas and see whether they fit together.