Без заголовка

машинную метрику качества нельзя, зато: 1) можно подключить пруф чекер и направить фидбек от него на вход сети, таким образом она будет учиться выдавать только корректные теории 2) сеть учится на осмыслегнных, прагматичных теориях, а не на случайном потоке корректных формул, так что есть надежда, что она внутри себя там что-то "поймет" про прагматики и поэтому ее выдача будет не совсем уж бессмысленным перебором всех корректных теорий подряд