News

World-championship in Automated Reasoning: computer scientist awarded

  • Faculté des Sciences, des Technologies et de Médecine (FSTM)
    Université / Administration centrale et Rectorat
    04 septembre 2019
  • Catégorie
    Université

On the occasion of the annual World Championship for Automatic Theorem Proving (“CADE ATP System Competition”, in short CASC) which took place on 28-29 August 2019 in Brazil, Alexander Steen, computer scientist at the University of Luxembourg, won a prize for “Leo-III”, a computer software that proves mathematical conjectures autonomously.

Automatic reasoning

Leo-III has been developed since 2014 by Alexander Steen, post-doc researcher within the Computer Science and Communications Research Unit (CSC) at the University of Luxembourg. “Leo-III is a computer software that we call “automated theorem prover” or, more general, a reasoning system that tries to find proofs for mathematical conjectures completely autonomously, that is without any help or advice from humans. The input of such systems is a problem statement in a formal logical language, and the output is — if successful – a formal proof of that conjecture”, explains Alexander.

Applications in mathematics and beyond

Theorem provers are used by mathematicians and computer scientists to formalise and to find proofs. In the first case, the human can input a proof of a mathematical statement and the system will check it for correctness; in the latter case, the proof is generated by the system in full.

Specifically, Leo-III automated a logical language which is referred to as “higher-order logic”, which is a very expressive formalism that can capture even more applications; but is also harder to realise in practice. Recently, Christoph Benzmüller, Professor at Freie Universität Berlin, Germany, and affiliated with the University of Luxembourg, has applied such systems to assess e.g. philosophical arguments from metaphysics.

“I am currently working on applying this technology to reasoning in the context of computer ethics and normative applications. With this step, of course, the target audience will eventually be even wider than just mathematicians and computer scientists”, adds Alexander.

International recognition

Leo-III ranked first place in the category “Large Theory Batch” (LTB) during the annual World Championship for Automatic Theorem Proving with over 54% solved problems (5441 out of 10000). “I am very happy about the good performance that Leo-III demonstrated in the LTB category, that has classically been dominated by first-order provers in the last years. This is a strong indication that the extra efforts of automating higher-order logic come with convincing benefits in practical applications”. The next best systems, the world leading first-order provers E (DHBW Stuttgart) and Vampire (U Manchester) found roughly 15% and 17% less solutions, respectively. Leo-III also ranked second place in the smaller THF division.

Leo-III is open-source software and freely available for use and further development. Details on the system and its theoretical foundations can be found in Steen’s PhD thesis. 

More information: http://page.mi.fu-berlin.de/lex/leo3/