MaLeCoP - Machine Learning Connection Prover

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21230%2F11%3A00191749" target="_blank" >RIV/68407700:21230/11:00191749 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

MaLeCoP - Machine Learning Connection Prover

Popis výsledku v původním jazyce

Probabilistic guidance based on learned knowledge is added to the connection tableau calculus and implemented on top of the lean-CoP theorem prover, linking it to an external advisor system. In the typical mathematical setting of solving many problems ina large complex theory, learning from successful solutions is then used for guiding theorem proving attempts in the spirit of the MaLARea system. While in MaLARea learning-based axiom selection is done outside unmodified theorem provers, in MaLeCoP thelearning-based selection is done inside the prover, and the interaction between learning of knowledge and its application can be much finer. This brings interesting possibilities for further construction and training of self-learning AI mathematical experts on large mathematical libraries, some of which are discussed. The initial implementation is evaluated on the MPTP Challenge large theory benchmark

Název v anglickém jazyce

MaLeCoP - Machine Learning Connection Prover

Popis výsledku anglicky

Probabilistic guidance based on learned knowledge is added to the connection tableau calculus and implemented on top of the lean-CoP theorem prover, linking it to an external advisor system. In the typical mathematical setting of solving many problems ina large complex theory, learning from successful solutions is then used for guiding theorem proving attempts in the spirit of the MaLARea system. While in MaLARea learning-based axiom selection is done outside unmodified theorem provers, in MaLeCoP thelearning-based selection is done inside the prover, and the interaction between learning of knowledge and its application can be much finer. This brings interesting possibilities for further construction and training of self-learning AI mathematical experts on large mathematical libraries, some of which are discussed. The initial implementation is evaluated on the MPTP Challenge large theory benchmark

Druh

R - Software

CEP obor

JD - Využití počítačů, robotika a její aplikace

OECD FORD obor

—

Projekt

—

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2011

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Interní identifikační kód produktu

MaLeCoP

Technické parametry

"open source", SWI-Prolog, UNIX-Bash, Perl

Ekonomické parametry

Nemá ekonomické parametry, určeno pro základní výzkum v oboru automatického uvažování a strojového učení.

IČO vlastníka výsledku

68407700

Název vlastníka

ČVUT FEL Katedra kybernetiky