要約
自然言語の数学的記述を形式的な実行可能なコードに翻訳することは、自動定理証明における基本的な課題である。これまでの研究では、生成とコンパイルの成功に焦点が当てられてきたが、生成された形式化が元の問題の意味論的意図を真正に捉えているかどうかの評価という批判フェーズには十分な注意が払われていなかった。本稿では、CriticLean（批評者主導強化学習フレームワーク）を紹介する。このフレームワークは、批評者の役割を受動的な検証者から能動的な学習構成要素へと高めるものである。具体的には、まず、監督微調整と強化学習を通じて訓練されたCriticLeanGPTを提案し、Lean 4 形式化の意味論的一致性を厳密に評価する。次に、モデルが正しくない形式化と意味論的に正しい形式化を区別する能力を測定するために設計されたベンチマークCriticLeanBenchを導入し、訓練されたCriticLeanGPTモデルが強力なオープンソースおよびクローズドソースのベースラインを大幅に上回ることを示す。CriticLean フレームワークに基づいて、FineLeanCorpusというデータセットを構築した。このデータセットは285,000以上の問題からなり、豊富な領域多様性、広範な難易度カバー、そして人間による評価に基づく高い正確性を持つ。全体として、我々の結果は批判フェーズの最適化が信頼性のある形式化の生成において不可欠であることを示しており、我々はCriticLeanが将来の形式数学的推論に関する進歩に貴重な洞察を与えることを期待している。