トーマス・ハーツ (Thomas Hirtz) 氏ら研究者グループは9月16日(現地時間)、自然言語から形式言語への変換における課題を解決する新たなフレームワーク「Sage (Semantic Agent-Guided Formalization Engine)」を発表した。Sageは、従来の単一的な変換手法ではなく、4段階のパイプラインとデュアルシグナル意味論的修正ループを導入。これにより、形式化プロセスにおける「厳密さの錯覚」を解消し、数学的な忠実性と構文的妥当性の両方を実現する。
従来のニューラル定理証明器は、数学の形式化において目覚ましい成果を上げてきたものの、多くの場合、忠実なLean 4形式ステートメントが既に提供されていることを前提としていた。しかし、非形式的な自然言語を形式言語に翻訳するプロセスは、重要なデータボトルネックとなっており、「厳密さの錯覚」という問題に直面していたと研究者らは指摘する。標準的な型チェッカーは、コンパイルはされるものの、仮説が欠落したり、無意味な真理を導入したり、数学的な境界を微妙に改変したりするステートメントを受け入れていたという。
この課題を解決するため、研究者らはSageを導入した。Sageは、単一的な翻訳を4段階に分解された生成パイプラインとデュアルシグナル意味論的修正ループで置き換えるエージェントフレームワークである。Sageの修正ループは、Lean 4コンパイラの診断結果と多次元の意味論的フィードバックを組み合わせることで、構文的妥当性と共に数学的な忠実性を強制する。
このパイプラインは、オープンエンドなクエリと宣言的な形式ターゲットの間のギャップを明示的に考慮に入れることで、モデルが未検証の回答を推測して高い形式化率を達成するのを防ぐ。これにより、従来のモデルが70.9%のアンサーリーケージ率を示したのに対し、Sageはリーケージを2.7%に抑制した。また、Omni-MATH without proofsデータセットにおいて、結合コンパイルと意味論的忠実性でパス@4スコア73.3%を達成。これは、ファインチューニングされたGoedel-Formalizer-V2ベースラインの42.0%を上回る結果である。
さらに、形式化されていない175のインターナショナル・マセマティカル・オリンピアード (International Mathematical Olympiad) 問題からなる新しいフロンティアIMO-Unformalizedにおいて、Sageはベースラインの19.4%に対し、パス@4で87.4%の検証済み忠実性を達成し、ゼロショット一般化能力を示した。盲目的なペアワイズ評価では79%以上で勝利したと報告されている。
参考: arXiv cs.LG (アーカイブ) — 2026年9月30日 13:00 (JST)