ProofOptimizerは、証明の簡素化を目的とした初の言語モデルであり、追加の人間による監督なしで訓練されています。近年、神経定理証明は急速に進展し、機械的に検証可能な長大な証明を生成していますが、これらは人間にとって理解が困難です。この問題に対処するため、ProofOptimizerは専門家の反復と強化学習を用いてLeanを介して簡素化の検証を行い、訓練信号を提供します。実験の結果、ProofOptimizerは最先端のRL訓練プローバーが生成した証明を大幅に圧縮し、標準ベンチマークでは87%、57%、49%の証明長の削減を達成しました。さらに、簡素化された証明はLeanでのチェックが速く、下流のプローバー性能も向上します。