AIベンチマークとしての数学の未解決問題のスケーリング：DeepMindの数学の未解決問題形式化リポジトリへの貢献からのAI safety的な学び
要約: DeepMindの数学の未解決問題の形式化を集めるOSSのリポジトリformal-conjecturesに、２つの貢献をしました。貢献の中で、AIに対する数学未解決問題の形式化の影響を以下の３つ感じました(1)ベンチマークへの影響(2)AIと人間の協業への影響(3)AIによる自己改善への影響。
導入
Google DeepMindは、2025年に、数学的な形式的な検証ソフトであるLeanを用いた、未解決問題のステートメントの形式化リポジトリ formal-conjectures を立ち上げました。このリポジトリの公式のゴールは以下です。
"自動定理証明器と自動形式化ツールの優れたベンチマークになります。
形式化を通じて推測の正確な意味を明確にするのに役立ちます。
必要な定義を強調表示して、mathlibを拡張します。"(※1)
AIの能力の評価において、既存の数学ベンチマーク（MATHやGSM8K）は急速に飽和しています。次なるフロンティアは「未解決問題」です。
実際に、AIは最近、次々に数学の未解決問題に貢献した、あるいは解いたという報告がなされています。が、そこには「正解を誰が判定するのか」という巨大な壁があります。その検証の方法の１つが、形式的な検証ソフトLEANの利用です。
このリポジトリでは、未解決予想を単に形式化して並べるだけでなく、未解決問題に対する、中間的な定理の形式化も貢献だと明言されています。
"未解決予想の解決済みの変種の形式化された記述や、専用の問題リストからの解決済みの記述にも関心があります。主な目的は予想記述を収集することですが、解決済みの項目や反例については、特に定義を解明し検証する非常に短い証明を含めていただければ幸いです。"(※1)
中間的な定理というのは、例えば、フェルマーの最終定理という予想そのものではなく、その予想を解くことを可能とする、中間的な定理であるフライ・セール定理のようなものです。
私は、このリポジトリに２つの貢献をしました。
貢献1: Lonely runner conjecture (LRC)という未解決問題に対する、最近の発展を支えているテレンスタオの中間的な定理を形式化する提案を行いました。(※2) 提案はコミュニティに肯定的に受け入れられました。
しかし、この貢献の直後に、私は疑問が生じました。
このような中間的な定理は大量にあるため、このような提案は無限にできてしまいます。そうすると、LEANによる形式化を担当するリポジトリのコントリビューターのリソースを消費してしまいます。
そこで私は、２つ目の貢献を行いました。
貢献2:形式化を提案された中間的な定理を、Issueのタグにより分類することを提案しました。(※3)
これにより、形式化を行うコントリビューターが形式化の対象を理解して取り組みやすくなります。
この２つの貢献の経験の中で、私は、「これは、AI safetyに対して、どのような貢献だったのか？」ということを疑問に思いました。
私は、(1)数学ベンチマークへの影響、(2)数学における人間とAIの協業の変質、（３）AIの自己改善への影響、が考えられると感じました。
(1)数学ベンチマークへの影響:貢献１の経験からの学び
未解決問題の中間定理の検証機を作ることは、数学の未解決問題のベンチマークとしての難易度を変化させます。例えば、私が貢献したLRCはn<=10までののケースの解法が知られていますが、n=8を解くときに、私が貢献した中間定理であるテレンスタオの貢献の形式化があることにより、AIが解く場合の難易度を下げるでしょう。おそらくそれは、n>10のとかれていないケースでも同様だと考えられます。
これは、高度な数学のベンチマークでも同様の効果が考えられます。つまり、このようなジャッジの提供自体が、AIによる問題解決能力の過剰評価につながる可能性があります。
(2) 将来、AIと人間は数学でどのように協業してくのか。:貢献2の経験からの学び
未解決問題のリポジトリの環境構築は、人間とAIの共同作業の場をどのように設計するかを考える問題です。一種の、human computer interaction (HCI)です。私が貢献した「未解決問題の中間定理に対してタグ付けする提案」は、人間にとっての働きやすさだけでなく、AIにとっての学習や探索のしやすさにもつながります。
人間にとっては、数学の問題の形式化を行うコントリビューターのリソースを無駄にしないために、中間定理の重要性と未解決問題の形式化の評価を与えることができます。AIにとってもラベルにより、データ摂取しやすくデータ識別しやすく、未解決問題に取り組む場合の推論がしやすくなります。
このような、タグ付けは、数学における人間とAIの役割すら変質する可能性があります。例えば、将来のあり得る分業体制として、人間は数学の中間定理をどの程度このリポジトリに受け入れるかのジャッジをし、AIが実際に中間定理の形式化を行い、中間定理の検証機を利用して未解決問題の解決が可能かの探索を試みる。
このようなAIと人間の共同作業の場所作りや役割の分担がどのようになるべきかは、おそらく、未解決問題が解かれるスピードや解かれた未解決問題の性質により議論が深まっていくと思います。
(3) AIによる自己改善への影響:貢献1,貢献2からの学び
「未解決問題の形式化のレポジトリを育てることがAIの自律的な強化を招く」という可能性があります。
このリポジトリはオープンであるため、AIも貢献は可能でしょう。将来的に、AI自身がステートメントを探してきて、中間定理を形式化し、コミットすることで、AIの数学能力が自律的に高まる可能性があります。
これは、AI safetyではしばしば問題となる、AIの自律性の問題を提示します。なぜなら、新しい数学がAIを強化する可能性があるからです。これは、一般的に語られるAIプログラムをできるAIによるAIによる自己強化とは違いますが、AIによる自己改善の１つの姿です。つまり、新たな数学的な取り扱いを発見するなどで数学のフロンティアを拡大することで、AIが自律的に自己強化を行います。
これは、数学の未解決問題の解決という、人間には未来が読めない、AIによる自己改善につながる可能性があります。
付録
別の疑問1:SWEのCI/CDとは違うのか？
SWEのCI/CDとは違うのか？という疑問があります。直感的には、数学は人類にとっての未知でありながら、存在は間違いない現象を持っています。
CI/CDでは、保護ができないものを数学は内包している可能性があり、そのような数学の発見は、AIの能力にものすごい影響がある可能性があります。
別の疑問2:LEANは「検証機」なのか？
LEANはこれまで、「検証機」だと言われていました。ステートメントから、証明までを、行間なく、自然言語に頼らず判断できるからです。
しかし、Deepmindのこのリポジトリのような、ステートメントだけの形式化は、「検証機」というよりは、ジャッジメントです。ジャッジメント機能の整備は、検証機の整備とは違うのでしょうか？この部分の取り扱いはさらなる探索が必要な点です。
<参照>
※1 https://github.com/google-deepmind/formal-conjectures
※2 https://github.com/google-deepmind/formal-conjectures/issues/1935
※3 https://github.com/google-deepmind/formal-conjectures/issues/1941
