Нейросеть прогнала свои триллионы умножений и написала лажу. Движок проверил, сказал нейросети - думай еще. Сколько таких итераций?
Вы сейчас о процессе обучения сети или о применении обученной сети?
В процессе обучения итераций много. Но это общая ситуация для практически полезных нейросетей. Время их обучения при заданных гиперпараметрах измеряется сутками, а то и в неделями. А потом изменим гиперпараметры и попробуем еще раз, и еще, и еще... Это долгая песня.
Если Вы про применение обученной сети, то пока/если/поскольку она будет доказывать теорему быстрее человека-математика, это будет выгодно.
Вы можете спросить: возможно ли вообще обучить нейросеть доказательству теорем? Я не специалист ни по нейросетям, ни по пруфчекерам, могу только спекулировать. Трудности с математическим доказательством в том, что оно должно быть безупречным. Одна ошибка разрушает все доказательство. Это отличается от обычного использования генеративных нейросетей, когда им достаточно выдать "нечто, похожее на правду".
С другой стороны, доказательство на формальном языке - это набор строк с заданным началом и концом и определенным синтаксисом. Если не ошибаюсь, пруфчекеры устроены так, что соблюдение синтаксиса гарантирует логическую корректность (пусть меня поправят те, кто с ними работал). Каждый может
убедиться, что даже туповатая по нынешним меркам GPT-4.1 nano безупречно соблюдает синтаксис русского языка, хотя он запутанный и сложный. Не вижу, почему бы ей не овладеть куда более простым синтаксисом пруфчекера, если бы у нее была достаточно большая обучающая выборка.