AIBR プレミアム
拓海先生、最近『Mathesis』という論文の話を聞きました。うちの現場でもAIを活かしたいのですが、これはどんな研究なんでしょうか。投資対効果の観点で端的に教えてくださいませ。
素晴らしい着眼点ですね！要点を3つでお伝えしますよ。1つ目、この論文は自然言語（英語など日常文）で書かれた数学問題を、そのまま機械が理解できる形式言語（Lean 4）に自動で翻訳し、形式的に証明まで試みる仕組みを示しているんですよ。2つ目、単に翻訳するだけでなく、翻訳の良し悪しを実際に検証して学習する仕組み、つまり強化学習（Reinforcement Learning、RL）を使って改善する点が新しいです。3つ目、実際の評価指標やベンチマーク（Gaokao‑FormalやLeanScorer）を整備し、性能を数値で示している点が投資判断で重要です。一緒に噛み砕いていきましょう。大丈夫、一緒にやれば必ずできますよ。
専門用語が並ぶと不安になります。まず『autoformalizer』という言葉がわかりません。要するに人が書いた問題文をプログラムが理解できるように書き換えるツールということで良いですか？
素晴らしい着眼点ですね！その通りです。autoformalizerとは、自然言語（Natural Language、NL）で書かれた数学問題を、形式証明系で扱える形式言語（Formal Language、FL）に変換する自動化ツールです。例えるなら、現場の作業指示書を工場の制御システムが読める命令書に自動で書き換えるソフトと同じ役割です。大丈夫、これなら現場の説明にも使えますよ。
なるほど。しかしその精度が肝ですね。翻訳ミスがあると現場では危険です。論文ではどうやって正確さを担保しているのですか？
大事な視点ですね。Mathesisは二つの工夫で精度を上げています。一つは生成した形式化コードをLean 4コンパイラで実行して構文上のエラーを検出すること、もう一つは意味的な妥当性を示すために導出できるかを試すことです。これらの結果を報酬に回して強化学習で学習させるため、単純な模倣学習より実運用に近い評価で改善できますよ。
これって要するに、自然文の問題を自動で定理証明可能なコードに翻訳して、翻訳が正しければ証明までできるように学習する仕組みということ？
その理解で正しいですよ。要点を3つにまとめると、1) 自然言語→Lean 4への自動形式化、2) 形式化の良否をコンパイルと証明試行で評価して強化学習に組み込む、3) ベンチマークと評価指標で性能を測る、です。だから実務における
監修者
阪上雅昭（SAKAGAMI Masa-aki）
京都大学 人間・環境学研究科 名誉教授
論文研究シリーズ
AI技術革新 - 人気記事
PCも苦手だった私が
