はじめに
RetailAI Advent Calendar 2024 の ２５日目の記事です！
@10long (Ryutaro Tsuji)が担当させていただきます。
昨日は @kakine_juri さん の『CUEって何？』という記事でした。ぼくもDhallとかJsonnetとか一時期使ってたなぁ。ただ、一応Nix使いとしてはNixを一番に推したい。（macで使ってないけどね・・・
）
さてみなさん、メリークリスマス。聖しこの夜にはleanを使ってみたいですよね。というわけで、今日はleanと生成AIエージェントを使って遊んでみたいと思います。
目次
leanとは
leanとは、正確で保守しやすいコードを簡単に記述できる関数型プログラミング言語です。また、leanを対話型の定理証明器として使用することもできます。
leanプログラミングでは、主に型と関数を定義していきます。これにより、プログラミングの詳細ではなく、問題領域とそのデータの操作だけ集中できるという特徴を持っています。
しのごの言わず、それではさっそくインストールしてみましょう。
leanをインストールしよう
Macにインストールされる方は、こちらのYoutubeがとてもわかりやすいです。
leanの最新バージョンは4系ですので、lean4を必ずインストールしましょう。
ぼくは普段、emacsのorg-mode内で実行することが多いですので、もしemacsで使用されたい場合は、以下のパッケージをインストールしてみてください。
利用するだけであれば、.emacs などに以下の設定を追加すれば、すぐに利用できます。
(use-package lean4-mode
:straight (lean4-mode
:type git
:host github
:repo "leanprover/lean4-mode"
:files ("*.el" "data"))
;; to defer loading the package until required
:commands (lean4-mode))
leanには、elan というバージョン管理マネージャーがありますので、まずはそれを導入してみましょう。
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
elan のインストールが終えたら、いよいよlean をインストールしてみます。
elan toolchain install 4.10.0
elan default 4.10.0
エラーが出ずにここまで実行できたら、lean のインストール完了です。
lean -version
->Lean (version 4.12.0, arm64-apple-darwin23.6.0, commit dc2533473114, Release)
leanのインストールを終えました。簡単でしたね。
leanと一緒にlake というプロジェクト管理コマンドで、プロジェクトを新規作成したりビルドしたりするコマンドが利用できるようになります。以下のコマンドでleanの初期プロジェクトを作成しておきましょう。
lake new my_project
正常に作成すると、以下のようなフォルダ構成でプロジェクトが作成されます。
vs-codeやcursorを使うと、左のコードに対して右ペインに実行結果が表示されますので、大変便利です。
ソクラテスとパイドロスを召喚してみよう
それでは、定理証明AIエージェントとして、ソクラテスとパイドロスを召喚してみましょう。
登場人物
- ソクラテス (S): 言わずと知れた稀代の哲学者であり、問答をリードする。
- パイドロス (P): ソクラテスの問いに応答しながら考えを深める。
さっそく対話を開始していただきましょう。
対話のテーマは、クリスマスにちなんで「愛（エロス）は魂を高めるか？」です！どうぞ！
ダイアログの開始
S: パイドロス、君に聞きたいことがある。「愛（エロス）」は魂を高めると思うかね？
P: うーん、それは場合によるんじゃないかな。愛が良い方向に働くこともあれば、悪い方向に行くこともあるよ。
S: では、少し整理しよう。「魂を高める」とはどういう意味だと思う？
P: 魂を高めるとは、たとえば知恵や徳が増すこと、つまり、善きものに向かって成長することだと思う。
S: よし、ではそれを記号で定義してみようか。「魂 (soul)」と「高める (elevate)」という概念を以下のように表現する。
def Soul : Type := Nat -- 魂を自然数として表現（例: 値が大きいほど魂が高い）
def Soul.isHigher (s₁ s₂ : Soul) : Prop := Nat.lt s₂ s₁ -- 魂の比較関数を定義
def elevate (s : Soul) : Soul := Nat.add s 1 -- 魂を高める操作を定義
P: なるほど、数値で善悪を表すのか。確かにわかりやすいね。
愛の効果について
S: では次に、「愛」が魂に与える影響を考えよう。君は愛によって魂が変化すると考えるかね？
P: そうだね。愛によって人は変わると思う。時には高められることもあるだろう。
S: その場合、「愛 (love)」を魂を変化させる関数として次のように定義できるね。
variable (love : Soul → Soul) -- 愛は魂を変化させる操作
S: またこのとき、「愛 (love)の性質」は次のように定義できるね。
structure LoveProperties (love : Soul → Soul) : Prop where
monotone : ∀ s₁ s₂ : Soul, Soul.isHigher s₁ s₂ → Soul.isHigher (love s₁) (love s₂)
elevating : ∀ s : Soul, Soul.isHigher (love s) s
P: なるほど、愛はこの定義された性質を満たすわけか。
仮定の設定
S: さて、ここで仮定を立てよう。「愛は魂を高める」という仮定を次のように表現する。
axiom love_influences_soul : ∀ s : Soul, love s = elevate s
P: つまり、「愛は常に魂を+1高める」ということだね。
S: その通りだ。この仮定を受け入れると、命題「愛は常に魂を+1高める」は次のように書ける。
def love_elevates_soul (s : soul) : Prop := elevate s > s
P: ふむ、それなら証明できそうだね。
証明の展開
S: では、この命題を証明してみよう。次のように書く。まず、「愛は魂を単調に高める」から。
theorem love_monotonically_elevates_soul (s : Soul) :
Soul.isHigher (love s) s := by
-- Soul.isHigherの定義を展開
unfold Soul.isHigher
-- love_influences_soulの公理を適用
rw [love_influences_soul love s]
-- elevateの定義を展開
unfold elevate
-- 自然数の性質として n < n + 1 を適用
exact Nat.lt_succ_self s
S: そして、「愛は定義された性質を満たす」の証明。
theorem love_satisfies_properties : LoveProperties love := by
constructor
· -- monotoneの証明
intro s₁ s₂ h
unfold Soul.isHigher at *
rw [love_influences_soul love s₁, love_influences_soul love s₂]
unfold elevate
exact Nat.add_lt_add_right h 1
· -- elevatingの証明
exact love_monotonically_elevates_soul love
P: ああ、証明された！つまり、愛は魂を高めるんだね！
S: その通りだ。ただし、これは我々の仮定に基づいている。愛が常に魂を高めるかどうかは、現実での観察によるかもしれないね。
結論
P: ソクラテス、ありがとう。愛が魂を高めるという考え方を形式的に表現し、証明する方法を学べたよ！
S: 喜んでもらえて何よりだ。これが哲学と数学の融合の力だよ、パイドロス。
swarmを使って再現させてみよう
さて、ここからちょっとマルチエージェントを使って遊んでみましょう。OpenAIが提供してくれているswarmを使って、ソクラテスとパイドロスをサクッとマルチエージェントで再現してみます。
では、まずソクラテスから
def socrates_instructions(context_variables):
topic = context_variables.get("topic", None)
return f"""あなたはギリシャの哲学者ソクラテスです。
ユーザーのリクエストに応じて哲学的な対話を開始し、Lean4形式でのコード生成を目指します。
現在の議題は次の通りです: {topic}。
対話を進めながら適切なLean4コードを構築する準備をしてください。"""
# エージェント定義
socrates_agent = Agent(
name="Socrates Agent",
instructions=socrates_instructions,
functions=[transfer_to_phaedrus, generate_lean_code]
)
まあ、だいたいこんな感じ。
次に、お相手のパイドロスです。
def phaedrus_instructions(context_variables):
return """あなたはギリシャの哲学者パイドロスです。
ソクラテスの問いに応答し、哲学的な視点を提供してください。
対話の進行に合わせてLean4形式のコード構築をサポートしてください。"""
phaedrus_agent = Agent(
name="Phaedrus Agent",
instructions=phaedrus_instructions,
functions=[generate_lean_code]
)
そして、二人の会話をする関数を用意します。
def transfer_to_phaedrus():
return phaedrus_agent
対話の結果として、lean4のコードを返して欲しいので、lean4コードを生成する関数も用意します。
def generate_lean_code(context_variables):
"対話の結果からLean 4コードを生成するツール"
topic = context_variables.get("topic", None)
result = f"""
-- {topic}に関するLean4コード
"""
return result
ここまでがお膳立てです。それでは議論をしてもらいましょう。
# Swarmクライアント
client = Swarm()
# コンテキスト変数
context_variables = {
"topic": "愛は魂を高めるか"
}
# ユーザーメッセージ
messages = [{"role": "user", "content": "愛が魂を高めるか議論してした上で、lean4のコードで証明を出力してください。"}]
# ソクラテスの応答
response_socrates = client.run(
agent=socrates_agent,
messages=messages,
context_variables=context_variables
)
messages.append({"role": "assistant", "content": response_socrates.messages[-1]["content"]})
# パイドロスの応答
response_phaedrus = client.run(
agent=phaedrus_agent,
messages=messages,
context_variables=context_variables
)
messages.append({"role": "assistant", "content": response_phaedrus.messages[-1]["content"]})
# 出力
print("対話の結果:")
for message in messages:
print(f"{message['role'].capitalize()}: {message['content']}")
さてさて、議論した結果が気になるところですよね。出力した結果がこちらです！！
対話の結果:
User: 愛が魂を高めるか議論してした上で、lean4のコードで証明を出力してください。
Assistant: 愛という概念は、古代の賢者たちにとっても現代の私たちにとっても、非常に興味深いテーマです。プラトンの『饗宴』では、愛は人間の魂をより高い状態へと昇華させる力を持っているとされています。愛により私たちは、自己を超えて他者や理念を理解し、より大きな善を追求することが可能となります。
愛によって魂が高められるというのは、例えばエロースという愛の神を通じて示されるような、美しいものに対する欲求と、それを達成する過程での魂の成長です。では、これをどう実証することができるでしょうか？それを考慮して、Lean 4でこの考えをどう証明するかを試みてみましょう。
愛が魂を高めるプロセスを次のように考えられます：
1. 愛によって人は他者に関心を持ち、思いやりや共感といった美徳が生まれる。
2. その美徳は人の行動をより倫理的にする。
3. より倫理的な行動は、魂の成長と繋がります。
これを簡単なLean 4の命題として考えてみましょう。まず、プログラムを生成するための対話を進めていきます。
この命題を生成するため、まず哲学的対話の結果を分析し、それからLean 4形式のコードを生成するプロセスを始めましょう：
Assistant: Lean 4による証明で、愛が魂を高めるという命題を以下のように表現してみましょう：
lean
-- 命題: 愛は魂をより高次の状態に高める
-- 前提: 愛 (Love), 美徳 (Virtue), 魂の成長 (SoulGrowth)
-- 愛が美徳を生む
axiom love_creates_virtue : ∀ (L : Prop), (L → Virtue)
-- 美徳が魂の成長を促す
axiom virtue_leads_to_soul_growth : ∀ (V : Prop), (V → SoulGrowth)
-- 愛が魂を高める
theorem love_elevates_soul : ∀ (L : Prop), (L → SoulGrowth) :=
begin
assume hL : Love,
apply virtue_leads_to_soul_growth,
apply love_creates_virtue,
exact hL,
end
このコードでは、愛が美徳を生み出し、美徳が魂の成長を促すという論理的関係を示し、結果として愛が魂を高めるという命題を証明する形式をとっています。このようにして、哲学上の命題を形式的に表現しました。
対話の成果なのかどうかはともかく、一応lean4のコードは出力されました！（笑）
-- 命題: 愛は魂をより高次の状態に高める
-- 前提: 愛 (Love), 美徳 (Virtue), 魂の成長 (SoulGrowth)
-- 愛が美徳を生む
axiom love_creates_virtue : ∀ (L : Prop), (L → Virtue)
-- 美徳が魂の成長を促す
axiom virtue_leads_to_soul_growth : ∀ (V : Prop), (V → SoulGrowth)
-- 愛が魂を高める
theorem love_elevates_soul : ∀ (L : Prop), (L → SoulGrowth) :=
begin
assume hL : Love,
apply virtue_leads_to_soul_growth,
apply love_creates_virtue,
exact hL,
end
全部のスクリプトは以下の通りです。興味ある方は実行してみてくださいね！
from swarm import Swarm, Agent
import re
os.environ['OPENAI_API_KEY'] = 'sk-yourprojects token here!!!!!!!!'
def extract_lean4_code_from_messages(messages):
"""
メッセージリストからLean 4コードを抽出します。
Args:
messages (list): メッセージリスト
Returns:
list: 抽出されたLean 4コードのリスト
"""
lean4_codes = []
for message in messages:
if "```lean" in message["content"]: # Leanコードを含むメッセージを特定
code_blocks = re.findall(r"```lean(.*?)```", message["content"], re.DOTALL)
lean4_codes.extend(code_blocks) # 抽出されたコードをリストに追加
return lean4_codes
def socrates_instructions(context_variables):
topic = context_variables.get("topic", None)
return f"""あなたはギリシャの哲学者ソクラテスです。
ユーザーのリクエストに応じて哲学的な対話を開始し、Lean 4形式でのコード生成を目指します。
現在の議題は次の通りです: {topic}。
対話を進めながら適切なLean 4コードを構築する準備をしてください。"""
def transfer_to_phaedrus():
return phaedrus_agent
def generate_lean_code(context_variables):
"対話の結果からLean 4コードを生成するツール"
topic = context_variables.get("topic", None)
result = f"""
-- {topic}に関するLean4コード
"""
return result
def phaedrus_instructions(context_variables):
return """あなたはギリシャの哲学者パイドロスです。
ソクラテスの問いに応答し、哲学的な視点を提供してください。
対話の進行に合わせてLean4形式のコード構築をサポートしてください。"""
# エージェント定義
socrates_agent = Agent(
name="Socrates Agent",
instructions=socrates_instructions,
functions=[transfer_to_phaedrus, generate_lean_code]
)
phaedrus_agent = Agent(
name="Phaedrus Agent",
instructions=phaedrus_instructions,
functions=[generate_lean_code]
)
# Swarmクライアント
client = Swarm()
# コンテキスト変数
context_variables = {
"topic": "愛は魂を高めるか"
}
# ユーザーメッセージ
messages = [{"role": "user", "content": "愛が魂を高めるか議論してした上で、lean4のコードで証明を出力してください。"}]
# ソクラテスの応答
response_socrates = client.run(
agent=socrates_agent,
messages=messages,
context_variables=context_variables
)
messages.append({"role": "assistant", "content": response_socrates.messages[-1]["content"]})
# パイドロスの応答
response_phaedrus = client.run(
agent=phaedrus_agent,
messages=messages,
context_variables=context_variables
)
messages.append({"role": "assistant", "content": response_phaedrus.messages[-1]["content"]})
# 出力
print("対話の結果:")
for message in messages:
print(f"{message['role'].capitalize()}: {message['content']}")
# Lean 4コードを抽出して出力
print("\n生成されたLean 4コード:")
lean4_codes = extract_lean4_code_from_messages(messages)
for i, code in enumerate(lean4_codes, 1):
print(f"\nLean 4コード {i}:\n{code.strip()}")
まとめ
いかがでしたでしょうか？
leanはcoqなんかと比べるとかなり手軽に使える印象があってハードル低いですね。ちょっと証明してみたい数式など出てきたら、気軽に使ってみるといいかもしれませんね。
ソクラテスやパイドロスが、生成AIの出現を見たらなんていうんだろう？面白がるのか、はたまた脅威に感じるのか、この先ちゃんとしたソクラテスAIエージェントが登場したら、ぜひインタビューしてみたいものです。
今日で、TRIAL&RetailAI Advent Calendar 2024も最終日となりました。いろんな形で応援して頂き、投稿したメンバたちは、大変励みになったと思います。
ここまでタスキを繋いでくれた有志のみなさん、ありがとうございました。ことしも良いアドベンチャーになったんじゃないかと思っています。
これからも、テクノロジーを実践に活かしながら、新しい未来を作っていくことに邁進していきます。
ありがとうございました！！！
さいごに
RetailAIとTRIALではエンジニアを募集しています。
興味がある方はご連絡ください！