I denna uppsats introducerar vi ett system som heter GamePad som kan användas för att utforska tillämpningen av maskininlärningsmetoder för teorem som bevisar i Coq proof assistent. Interaktiva teorem bevis såsom Coq gör det möjligt för användare att konstruera maskinkontrollerbara bevis i ett steg-för-steg sätt. Därför ger de en möjlighet att utforska teorem som bevisar sig med mänsklig tillsyn. Vi använder GamePad för att syntetisera bevis för en enkel algebraisk omskrivning problem och träna baslinje modeller för en formalisering av Feit-Thompson teorem. Vi behandlar positionsutvärdering (dvs. förutsäga antalet bevis steg kvar) och taktik förutsägelse (dvs. förutsäga nästa bevissteg) uppgifter, som uppstår naturligt i taktikbaserade teorem bevis.
2) REF där författarna introducerade GamePad dataset (med baslinje neurala modeller) för att utvärdera neurala modeller på uppgifterna för positionsutvärdering (dvs. Förutsäga hur många återstående bevissteg som krävs för att slutföra ett bevis) och en taktikförutsägelse (dvs. Förutsäga vad nästa bevissteg kommer att bli).
GamePad: A Learning Environment for Theorem Proving
{'venue': 'ArXiv', 'journal': 'ArXiv', 'mag_field_of_study': ['Mathematics', 'Computer Science']}