自然言語の形式数学変換エージェント Sage──解答漏洩を 2.7% に抑え Omni-MATH で 73.3% の成功率を達成

論文概要

AI による定理証明（Neural Theorem Prover）の進展に伴い、自然言語で書かれた数学の命題を形式数学言語である Lean 4 に変換する作業の重要性が高まっている。しかし、従来の単一的な翻訳アプローチでは、構文エラーは回避できても仮説を脱落させたり自明な真理を導入したりする「厳密性の幻想（illusion of rigor）」という深刻なボトルネックが存在していた。本論文では、この課題を解決するエージェント型フレームワーク「Sage (Semantic Agent-Guided Formalization Engine)」が提案されている。Sage は、4段階に分解された生成パイプラインと二重シグナルによる意味的補正ループを組み合わせることで、数学的忠実度と構文的妥当性を同時に強制する。

関連研究

これまでの神経定理証明や形式化手法の多くは、正しい Lean 4 の形式的文がすでに提供されているという前提に依存していた。オープンエンドなクエリから宣言的な形式的ターゲットへの翻訳においては、モデルが未検証の答えを推測して高い形式化率に見せかける「解答漏洩（answer leakage）」が問題視されてきた。既存のファインチューニングされたモデル（例えば Goedel-Formalizer-V2 など）は、このギャップを十分に埋めることができていなかった。

新規性と貢献

本研究の最大の貢献は、単なるコンパイル通過（構文的妥当性）だけでなく、多次元的な意味的フィードバックループによって数学的妥当性を担保する点にある。これにより、従来モデルが 70.9% 示していた解答漏洩率を 2.7% まで激減させ、Omni-MATH ベンチマークにおいて pass@4 で 73.3%（既存ベースラインの 42.0% から大幅向上）という高いジョイントコンパイル・意味的忠実度を実現した。さらに、未形式化の国際数学オリンピック問題 175 問からなる新規ベンチマーク IMO-Unformalized において、ゼロショット汎化による 87.4% の検証済み忠実度を達成している。

提案手法の詳細

Sage は、従来の単一モデルによる一括翻訳を廃し、4段階に分解された生成パイプラインを採用している。なぜこの設計にしたかといえば、推論プロセスを分割することで各段階におけるコンテキストの劣化を防ぎ、Lean 4 のコンパイラ診断と外部の意味的評価シグナルを組み合わせたフィードバックループを個別に適用できるようにするためである。これにより、オープンな問いから形式的記述への移行時に発生しやすい解のリークや境界条件の欠落を構造的に排除する。

評価・考察

評価実験では、Omni-MATH および IMO-Unformalized が用いられた。OMNI-MATH における評価では、Sage が解答漏洩を 2.7% に抑制しつつ高い成功率を示した。 また、IMO-Unformalized においては、ベースラインの 19.4% に対して 87.4% の pass@4 検証済み忠実度を記録し、ブラインドペアワイズ評価の 79% 以上で勝利を収めた。 この結果は、複雑な未解決の数学的命題に対しても、意味的補正エージェントが有効に機能することを強く裏付けている。

応用例と今後の展望

実務的なインパクトとして、自動定理証明や形式検証を導入する金融・暗号技術分野や高度な数理最適化を行う研究開発組織において、自然言語の仕様書や数学的要件定義から信頼性の高い形式仕様を自動生成するワークフローへの応用が考えられる。国内の数理最適化やセキュリティ検証を担う研究開発部門（例えば、金融機関の数理モデリング部門や暗号プロトコル検証チームなど）において、数人規模の検証チームの工数を大幅に削減する基盤技術となり得る。今後の課題としては、より大規模な定理ライブラリへのスケーリングや、複雑なカスタム公理系に対するエージェントの適応力向上が挙げられる。

結論

Sage は、自然言語から Lean 4 への形式数学変換において、多段階分解生成と二重シグナル意味的補正ループを導入することで、解答漏洩を極限まで抑制しつつ高い忠実度での形式化を実現した。定理証明のエージェント化における新たなマイルストーンとなる成果である。

注釈

• Lean 4: プログラミング言語兼用の対話式定理証明系。数学の定理が正しいことをコンピュータで厳密に検証するために使用される。
• Omni-MATH / IMO-Unformalized: 高度な数学の問題や、国際数学オリンピックの未形式化問題を収録したベンチマーク。