はじめに
代数トポロジーには蛇の補題というものがあります。数学専攻だと大学3年生で学ぶものです。これまで、気になるLLMが出た際にこれを証明できるかをチェックしてきました（蛇の補題チャレンジと勝手に呼んで）。
この度、OpenAI o1-previewが蛇の補題チャレンジにおおよそクリアしたので、それを記録したいと思います。
蛇の補題とは？
次のの可換図式を考えます。
\begin{array}{ccccccccc}
& & & & & & & & \\
& & A' & \xrightarrow{\alpha} & A & \xrightarrow{\beta} & A'' & \rightarrow & 0 \\
& & \downarrow f' & & \downarrow f & & \downarrow f'' & & \\
0 & \rightarrow & B' & \xrightarrow{\gamma} & B & \xrightarrow{\delta} & B'' & & \\
\end{array}
上下がどちらも完全系列のとき、以下も完全系列だというのが蛇の補題です。
\ker(f') \xrightarrow{k} \ker(f) \xrightarrow{l} \ker(f'') \xrightarrow{\partial} \operatorname{coker}(f') \xrightarrow{m} \operatorname{coker}(f) \xrightarrow{n} \operatorname{coker}(f'') \\
（おそらく、Qiitaの多くの読者は不明な用語ばかりと思うが、詳細を解説するのが目的ではないので、「なんか専門的なものなんだな」と流してもらいたい。）
OpenAI o1-previewの証明
全文
o1-previewで実行した結果全文は、以下のリンクから見られます。
全文（画像・・・開いて長いなーと思ってください）
全文（生出力）
**The Snake Lemma**
**Statement:**
Let
\[
\begin{array}{ccccccccc}
& & & & & & & & \\
0 & \rightarrow & A' & \xrightarrow{\alpha} & A & \xrightarrow{\beta} & A'' & \rightarrow & 0 \\
& & \downarrow f' & & \downarrow f & & \downarrow f'' & & \\
0 & \rightarrow & B' & \xrightarrow{\gamma} & B & \xrightarrow{\delta} & B'' & \rightarrow & 0 \\
\end{array}
\]
be a commutative diagram in an abelian category (such as the category of abelian groups or modules over a ring), where the rows are exact sequences. Then there exists an exact sequence (called the "snake sequence"):
\[
\ker(f') \xrightarrow{k} \ker(f) \xrightarrow{l} \ker(f'') \xrightarrow{\partial} \operatorname{coker}(f') \xrightarrow{m} \operatorname{coker}(f) \xrightarrow{n} \operatorname{coker}(f'') \\
\]
where \( \partial \) is a connecting homomorphism, and \( k, l, m, n \) are naturally induced maps.
---
**Proof:**
We will construct each map in the sequence and verify exactness at each step.
**Step 1: Define the Maps Between Kernels**
1. **Define \( k: \ker(f') \rightarrow \ker(f) \) by \( k(a') = \alpha(a') \).**
- **Justification:** Since \( f'(a') = 0 \) (because \( a' \in \ker(f') \)) and the diagram commutes (\( f \circ \alpha = \gamma \circ f' \)), we have:
\[
f(\alpha(a')) = \gamma(f'(a')) = \gamma(0) = 0.
\]
Therefore, \( \alpha(a') \in \ker(f) \), making \( k \) well-defined.
2. **Define \( l: \ker(f) \rightarrow \ker(f'') \) by \( l(a) = \beta(a) \).**
- **Justification:** For \( a \in \ker(f) \), \( f(a) = 0 \). Using the commutativity \( f'' \circ \beta = \delta \circ f \), we get:
\[
f''(\beta(a)) = \delta(f(a)) = \delta(0) = 0.
\]
So \( \beta(a) \in \ker(f'') \), and \( l \) is well-defined.
**Step 2: Define the Connecting Homomorphism \( \partial \)**
3. **Define \( \partial: \ker(f'') \rightarrow \operatorname{coker}(f') \).**
- **Construction:**
- Let \( a'' \in \ker(f'') \). Since \( \beta \) is surjective (from the exactness of the top row), there exists \( a \in A \) such that \( \beta(a) = a'' \).
- Applying \( f'' \) gives:
\[
f''(a'') = f''(\beta(a)) = \delta(f(a)) = 0,
\]
so \( \delta(f(a)) = 0 \), implying \( f(a) \in \ker(\delta) = \operatorname{Im}(\gamma) \) (from the exactness of the bottom row).
- Therefore, there exists \( b' \in B' \) such that \( \gamma(b') = f(a) \).
- The element \( b' \) is not uniquely determined, but any two choices differ by an element in \( \operatorname{Im}(f') \) (we'll verify this shortly).
- Define \( \partial(a'') = [b'] \in \operatorname{coker}(f') = B' / \operatorname{Im}(f') \).
- **Well-Definedness:**
- Suppose \( a \) and \( a' \) are two elements in \( A \) such that \( \beta(a) = \beta(a') = a'' \).
- Then \( a - a' \in \ker(\beta) = \operatorname{Im}(\alpha) \), so \( a - a' = \alpha(a'') \) for some \( a'' \in A' \).
- Applying \( f \) gives:
\[
f(a) - f(a') = f(\alpha(a'')) = \gamma(f'(a'')).
\]
- Therefore, \( \gamma(b' - b'') = \gamma(f'(a'')) \), implying \( b' - b'' = f'(a'') \) (since \( \gamma \) is injective on \( \operatorname{Im}(f') \)).
- Thus, \( [b'] = [b''] \) in \( \operatorname{coker}(f') \), so \( \partial(a'') \) is independent of the choice of \( a \) and \( b' \).
**Step 3: Define the Maps Between Cokernels**
4. **Define \( m: \operatorname{coker}(f') \rightarrow \operatorname{coker}(f) \) by \( m([b']) = [\gamma(b')] \).**
- **Justification:** For \( b' \in B' \), \( \gamma(b') \in B \). Since \( \gamma \) is a homomorphism, \( m \) is well-defined and linear.
5. **Define \( n: \operatorname{coker}(f) \rightarrow \operatorname{coker}(f'') \) by \( n([b]) = [\delta(b)] \).**
- **Justification:** Similar to above, \( \delta(b) \in B'' \), and \( n \) is a well-defined homomorphism.
**Step 4: Verify Exactness of the Sequence**
We will now show that the sequence is exact at each point.
1. **Exactness at \( \ker(f) \):** \( \operatorname{Im}(k) = \ker(l) \).
- **Proof:**
- **\( \operatorname{Im}(k) \subseteq \ker(l) \):** For \( a' \in \ker(f') \),
\[
l(k(a')) = l(\alpha(a')) = \beta(\alpha(a')) = 0 \quad (\text{since } \beta \circ \alpha = 0).
\]
Thus, \( k(a') \in \ker(l) \).
- **\( \ker(l) \subseteq \operatorname{Im}(k) \):** Let \( a \in \ker(f) \) such that \( l(a) = \beta(a) = 0 \). Then \( a \in \ker(\beta) = \operatorname{Im}(\alpha) \), so \( a = \alpha(a') \) for some \( a' \in A' \). Applying \( f \) gives:
\[
0 = f(a) = f(\alpha(a')) = \gamma(f'(a')).
\]
Since \( \gamma \) is injective on \( \operatorname{Im}(f') \), \( f'(a') = 0 \), so \( a' \in \ker(f') \). Therefore, \( a = k(a') \), proving \( \ker(l) \subseteq \operatorname{Im}(k) \).
2. **Exactness at \( \ker(f'') \):** \( \operatorname{Im}(l) = \ker(\partial) \).
- **Proof:**
- **\( \operatorname{Im}(l) \subseteq \ker(\partial) \):** For \( a \in \ker(f) \),
\[
\partial(l(a)) = \partial(\beta(a)) = [b'],
\]
where \( f(a) = \gamma(b') \). Since \( f(a) = 0 \), \( \gamma(b') = 0 \), so \( b' \in \ker(\gamma) = 0 \) (from the exactness at \( B' \)), implying \( b' = 0 \). Hence, \( \partial(\beta(a)) = [0] \), so \( \beta(a) \in \ker(\partial) \).
- **\( \ker(\partial) \subseteq \operatorname{Im}(l) \):** Let \( a'' \in \ker(\partial) \), so \( \partial(a'') = [0] \). This means there exists \( b' \in \operatorname{Im}(f') \) such that \( \gamma(b') = f(a) \) for some \( a \in A \) with \( \beta(a) = a'' \). Since \( b' = f'(a') \) for some \( a' \in A' \), we have:
\[
f(a - \alpha(a')) = f(a) - f(\alpha(a')) = \gamma(b') - \gamma(f'(a')) = 0.
\]
Moreover, \( \beta(a - \alpha(a')) = \beta(a) - \beta(\alpha(a')) = a'' - 0 = a'' \). So \( a - \alpha(a') \in \ker(f) \), and \( l(a - \alpha(a')) = a'' \), implying \( a'' \in \operatorname{Im}(l) \).
3. **Exactness at \( \operatorname{coker}(f') \):** \( \operatorname{Im}(\partial) = \ker(m) \).
- **Proof:**
- **\( \operatorname{Im}(\partial) \subseteq \ker(m) \):** For \( a'' \in \ker(f'') \), \( \partial(a'') = [b'] \). Applying \( m \), we get:
\[
m(\partial(a'')) = m([b']) = [\gamma(b')] = [f(a)],
\]
where \( f(a) = \gamma(b') \). Since \( f(a) \in \operatorname{Im}(f) \), \( [f(a)] = 0 \) in \( \operatorname{coker}(f) \). Therefore, \( m(\partial(a'')) = 0 \), so \( \partial(a'') \in \ker(m) \).
- **\( \ker(m) \subseteq \operatorname{Im}(\partial) \):** Let \( [b'] \in \ker(m) \), so \( m([b']) = [\gamma(b')] = 0 \). This implies \( \gamma(b') \in \operatorname{Im}(f) \), so \( \gamma(b') = f(a) \) for some \( a \in A \). Let \( a'' = \beta(a) \). Then:
\[
f''(a'') = f''(\beta(a)) = \delta(f(a)) = \delta(\gamma(b')) = 0,
\]
since \( \delta \circ \gamma = 0 \). Thus, \( a'' \in \ker(f'') \), and \( \partial(a'') = [b'] \), showing \( [b'] \in \operatorname{Im}(\partial) \).
4. **Exactness at \( \operatorname{coker}(f) \):** \( \operatorname{Im}(m) = \ker(n) \).
- **Proof:**
- **\( \operatorname{Im}(m) \subseteq \ker(n) \):** For \( [b'] \in \operatorname{coker}(f') \),
\[
n(m([b'])) = n([\gamma(b')]) = [\delta(\gamma(b'))] = [0],
\]
since \( \delta \circ \gamma = 0 \). Thus, \( m([b']) \in \ker(n) \).
- **\( \ker(n) \subseteq \operatorname{Im}(m) \):** Let \( [b] \in \ker(n) \), so \( n([b]) = [\delta(b)] = 0 \), implying \( \delta(b) \in \operatorname{Im}(f'') \). Since \( \delta(b) = f''(b'') \) for some \( b'' \in B'' \), and \( \delta(b - f(b'')) = 0 \), we have \( b - f(b'') \in \ker(\delta) = \operatorname{Im}(\gamma) \). So \( b - f(b'') = \gamma(b') \) for some \( b' \in B' \). Therefore, \( [b] = [\gamma(b')] \), and \( [b] \in \operatorname{Im}(m) \).
---
**Conclusion:**
We have constructed maps \( k, l, \partial, m, n \) such that the sequence
\[
\ker(f') \xrightarrow{k} \ker(f) \xrightarrow{l} \ker(f'') \xrightarrow{\partial} \operatorname{coker}(f') \xrightarrow{m} \operatorname{coker}(f) \xrightarrow{n} \operatorname{coker}(f'')
\]
is exact. This completes the proof of the Snake Lemma.
証明の評価
この出力は100点満点ではないですが、大筋出来ていて、ほぼクリアと思ってよさそうです。Step1,Step2,...と証明のステップを分け、それぞれのステップで証明すべき事項を細分化して、よく整理された証明で読みやすいです。一般的な書籍・論文の証明の書き方とは異なり、マークダウンを活用した書き方になっているのも新鮮です。
証明自体の課題を挙げると以下の通りです。
- 仮定ではアーベル圏で議論しているが、加群での議論になっている
- 仮定の$0\rightarrow A$ と $B''\rightarrow 0$の部分が無くてもよい（これをつけるバージョンもある）
- $\partial$ が準同型なことをチェックしていない
- Step3の箇所は簡単だが、さぼりすぎ
- Step4の4の $b''\in B''$ の部分が、本当は $a''\in A''$ とすべき（併せて変数修正）
仮定が微妙な個所は、蛇の補題を色んな記述をつなぎ合わせて理解しているのかなと思えます。
問題の難しい部分
蛇の補題を自力で証明するのはかなり困難です。特に、写像 $\partial$ の構成を知識なく実施することは難しいです。それができても、チェックすべき項目が多いことも難易度を上げています。人間であれば地道にするかもしれませんが、LLMの場合、途中で諦める危険が高いです。
実際の失敗パターン
自分が試した範囲では、これまでは上手くいかなかったのですが、以下の失敗パターンがありました。
- 証明が途中で終わる
- 証明すべき項目の列挙が全然足らない
- チャットで手伝っても、論理が正しく運用されない
- 蛇の補題の主張がデタラメ
2023年の4月くらいから試しているのですが、当時のChatGPTはトークン数制限が強く、そのことに気が付いて諦めました。色々と間違いを指摘したりして頑張ったのですが、滅茶苦茶な論理をしていて、ムキーとなりながら試していました。
ChatGPTのアップデートがあると、たまに再チャレンジしてました。しかし、それまで出来ていたはずなのに、デタラメな図式を蛇の補題だと出してきて、劣化しているかのような状況が頻発しました。これの失敗はgpt-4oでも見られます。
ちなみに、o1-preview でも日本語で行うと上手く行きませんでした（偶然もあるかもしれませんが）。
OpenAI o1は何が変る？
OpenAI o1で推論方法がどのように変わるのかの詳細が、APIドキュメントのOpenAI o1の推論方法の説明に記載されています（正式リリースで変更される可能性がありますが）。
そこに記載された重要な図がこちらになります。これは、OpenAI o1はサーバー側でchain of thoughtを行うことを示した図です。reasoningトークンを導入する工夫もあります。
ちなみに、推論途中の出力はAPIの結果に含まれないそうですが、outputトークンして課金対象になるそうです。
蛇の補題の思考過程
ウェブ版ChatGPTでは、思考過程を見ることができます。蛇の補題の場合、以下の通りでした（しれっと思考時間54秒と書かれているのもびっくりですが）。へんちくりんな日本語になっていますが、雑な翻訳になっているだけのようです。言語設定を英語にして新規に利用すると自然な英語になりました（既に日本語で表示されたものは変わらない）。プレビュー版なので、変わるかもしれませんが。
まとめ
OpenAI o1-previewで蛇の補題チャレンジほぼクリアできたことを紹介しました。
o1系でサーバー側でchain of thoughtをしてくれるようになり、それでかなり賢くなりそうだと理解しました。きっと、Chain of thoughtが上手く機能するようにチューニングしていて、そういうのも効いているのだと思います。
一度ほぼクリアを見ると、gpt-4oや他の既存モデルでもchain of thoughtを駆使すれば、蛇の補題を証明できたのかもしれないと疑惑が出てきます。気が向いたらそういうのも確かめたいなと思います。
OpenAI o1は、これまでのモデルから大幅に推論コストが上がるモデルになります。これをどんな使い方をしていくと良いのかというのが、今後吟味されていくのだと思います。正式版リリースが楽しみですね。
以上。