オペレーターツリーによる自動形式化のための神経記号フレームワーク：分解・構造化・修復

Abstract

自動形式化（autoformalization）は、人間の数学と形式数学の間における重要な架け橋として機能し、自然言語の問題を形式言語へと翻訳します。先行研究では、データ合成や多様な学習パラダイムに焦点を当ててエンドツーエンドの大規模言語モデル（LLM）を最適化する取り組みが行われてきましたが、これらは一般に形式コードを平坦な列として扱い、数学的命題に内在する階層的な論理を見落としています。本研究では、自動形式化をモジュール式のパイプラインへと再構成するニューラル・シンボリック枠組みである Decompose, Structure, and Repair（DSR）を提案します。DSRは命題を論理的構成要素へ分解し、それらを構造化された演算子ツリーへ写像します。さらに、トポロジカルな設計図を活用することで、サブツリーの洗練（refinement）によって誤りを正確に局所化し、修復します。加えて、標準的な教科書から選び、専門家が Lean 4 で精密に注釈した、学部・大学院レベルの定理156件からなるベンチマーク PRIME を導入します。実験結果は、DSRが新たな最先端の性能を確立し、同等の計算予算のもとで一貫してベースラインを上回ることを示しています。データセット、モデル、コードは近日中に公開されます。