Upgrade to Pro
— share decks privately, control downloads, hide ads and more …
Speaker Deck
Features
Speaker Deck
PRO
Sign in
Sign up for free
Search
Search
Solving olympiad geometry without human demonst...
Search
Toma Tanaka
January 22, 2024
Technology
4
660
Solving olympiad geometry without human demonstrations
Solving olympiad geometry without human demonstrationsの論文紹介
AlphaGeometryの論文
間違いや修正箇所などがあればご指摘ください!
Toma Tanaka
January 22, 2024
Tweet
Share
More Decks by Toma Tanaka
See All by Toma Tanaka
AI研究の自動化に向けたOSSの開発
fuyu_quant0
0
84
大規模言語モデルの論理構造の把握能力と予測モデルの生成
fuyu_quant0
0
170
Evolutionary Optimization of Model Merging Recipes
fuyu_quant0
4
2.3k
Inductive-bias Learning: 大規模言語モデルによる予測モデルの生成
fuyu_quant0
0
210
論文紹介:Language Model Inversion
fuyu_quant0
0
260
量子コンピュータとデータサイエンティスト
fuyu_quant0
0
390
スライド用GPTを使った 「量子コンピュータ」の スライド作成
fuyu_quant0
0
35k
Other Decks in Technology
See All in Technology
Goに育てられ開発者向けセキュリティ事業を立ち上げた僕が今向き合う、AI × セキュリティの最前線 / Go Conference 2025
flatt_security
0
290
“2件同時配達”の開発舞台裏 〜出前館PMが挑んだダブルピック実現に向けた体験設計〜
demaecan
0
160
[2025-09-30] Databricks Genie を利用した分析基盤とデータモデリングの IVRy の現在地
wxyzzz
0
410
API提供者のためのMCPサーバー設計ガイド / MCP Server Design Guide for API Providers
yokawasa
0
240
非同期処理実行基盤 Delayed脱出 → Solid Queue完全移行への旅路。
srockstyle
3
1.5k
DEFCON CHV CTF 2025 Write-up
bata_24
0
200
PyCon JP 2025 DAY1 「Hello, satellite data! ~Pythonではじめる衛星データ解析~」
ra0kley
0
840
AIを導⼊しても、 開発⽣産性は"爆増"していない なぜ?
kinosuke01
4
3.6k
実装で解き明かす並行処理の歴史
zozotech
PRO
1
120
AI時代だからこそ考える、僕らが本当につくりたいスクラムチーム / A Scrum Team we really want to create in this AI era
takaking22
1
170
Green Tea Garbage Collector の今
zchee
PRO
2
360
いま注目しているデータエンジニアリングの論点
ikkimiyazaki
0
550
Featured
See All Featured
Designing Dashboards & Data Visualisations in Web Apps
destraynor
231
53k
Testing 201, or: Great Expectations
jmmastey
45
7.7k
We Have a Design System, Now What?
morganepeng
53
7.8k
Visualizing Your Data: Incorporating Mongo into Loggly Infrastructure
mongodb
48
9.7k
How to Create Impact in a Changing Tech Landscape [PerfNow 2023]
tammyeverts
53
3k
[RailsConf 2023 Opening Keynote] The Magic of Rails
eileencodes
30
9.7k
RailsConf & Balkan Ruby 2019: The Past, Present, and Future of Rails at GitHub
eileencodes
140
34k
Responsive Adventures: Dirty Tricks From The Dark Corners of Front-End
smashingmag
252
21k
CSS Pre-Processors: Stylus, Less & Sass
bermonpainter
358
30k
A designer walks into a library…
pauljervisheath
208
24k
Art, The Web, and Tiny UX
lynnandtonic
303
21k
How to Ace a Technical Interview
jacobian
280
23k
Transcript
田中 冬馬 2023/1/22 ShibuyAI No.4
自己紹介 株式会社ブレインパッド データサイエンティストとしてマーケティング分析,広告文の自動生成などの自 然言語処理の業務に従事 その他の活動 LLM 関連で論文執筆 Inductive-bias Learning: Generating
Code Models with Large Language Model Data Science wiki データ分析手法,AI 関連の技術のまとめサイト Qiita の執筆 @fuyu_quant 1
概要 Googe DeepMind の研究,Nature(2024/1/17) に掲載 言語モデルと演繹的推論を組み合わせたAlphaGeometry を提案 平面幾何学の問題限定でIMO 金メダリストの平均的なスコアに迫る正解率を達成 (SOTA)
演繹的推論だけで導けない補助項の生成に言語モデルを利用 人間による注釈や問題文を使わず合成データだけで言語モデルを学習 学習データ不足になりがちな数学などの領域に対する一つの指針となるフレーム ワーク ※IMO ...International mathmatical Olympaid( 国際数学オリンピック) 2
前提知識 DD(Deductive databse) http://www.mmrc.iss.ac.cn/~xgao/paper/jar-gdbase.pdf データベースを使い幾何学的な問題を演繹的に推論する手法 AR(Algebraic reasoning) 代数的な概念,原則,手法を用いて問題を解く方法 論文のAppendix に記載
(※ 上記についての説明は含みませんが内容は理解できると思います) 3
背景・課題,目的 4
背景・課題 背景 定理証明能力は論理的な推論に精通し,広範な空間を探索する能力を必要と するため人工知能研究の一つの焦点 定理証明は学習ベースの手法では困難と言われている 課題 学習データが少ない 人間の証明を機械が検証可能な言語(Lean9 など) に翻訳したデータが少な
い 特に幾何学は翻訳することが難しく証明例が非常に少ない 5
目的 人によるデータ作成を行わずに合成データを作成する方法を提案 合成データにより学習した言語モデルと演繹的推論をくみあわせる他手法 (AlphaGeometry) を使いIMO 金メダリストの平均スコアに迫るスコアを実証す る. 6
手法 7
手法 学習のための合成データの作成 利用した言語モデル 言語モデルの学習 AlphaGeometry の動作 8
学習のための合成データの生成 右図にあるような“ 前提” からサンプリン グを行う “ 前提“ から記号的演繹エンジン(DD+AR) を使い様々なtrue statements
を生成 証明の中の部分的な演繹推論を取り出 し,1 億個のユニークな証明のサンプル を生成 (IMO-AG-30 問題を含まないような) ・・・ ( 全部で55 個) 9
学習のための合成データの生成 記号的演繹エンジン(DD+AR) を使い“ 前提” をもとにtrue statements を生成 上記の場合,学習データサンプルは以下のようになる 前提:ランダムサンプリングしたもの 結論:“HA
⊥BC” 証明:“HA ⊥BC” 以外の緑色のノード 10
利用した言語モデル 利用したライブラリ Meliad 人気のあるTransformer アーキテクチャを拡張し,長いシーケンスに対応させたものなどが含まれ ている https://github.com/google-research/meliad 言語モデル アーキテクチャ:(Transformer-XL with
sliding window ?) Meliad のベースラインモデルで採用されており,今回の研究では基本設定を使ったと記載があるため パラメータ:1 億5100 万 12 層 埋め込み次元:1024 アテンションのヘッド:8 Tokenizer SentencePiece を単語モードで学習 11
言語モデルの学習 “ 前提, 結論, 証明” の順番で文字列を作成し,“ 前提, 結論” から“ 証明”
を生成するよ うに言語モデルを学習 このような学習を行うことで演繹的推論だけでは導けない補助項を生成できる ようになる 補助項の構築は以前から研究されていたが,手作業で作成されたテンプレ ートなどを活用しており人間の経験のサブセットに制限されていた 言語モデルと組み合わせることで記号的演繹エンジン(DD+AR) で解ける以上の 問題を解くことができる 12
AlphaGeometry の証明方法 実行方法( 以下を繰り返す) 記号的演繹エンジンで与えられた記述から証明を試みる a. 証明できない場合に言語モデルにより補助項を追加する b. 設定 最大反復回数:16
回 ビームサーチ LLM の出力の上位512 個を用いて探索する 13
結果 14
結果 テストデータセット 2000 年から現在までのIMO の公式問題から作成 AlphaGeometry が対象とする幾何学の問題に絞り作成 幾何学的な不等式など,他の数学の領域を必要とする問題は対象外 全部で30 題の問題を用意
全て学習データに含まれていないことを確認済み 15
結果 AlphaGeometry は30 問中25 問を 解答 16
結果 10 種類のソルバーを使い比較 AlphaGeometry でSOTA を達成 17
結果 人間にも難しい問題はAlphaGeometry の証明の長さに反映されている 簡単な問題( 人間のscore>3.5) では人間のスコアと証明長に相関は見られない 18
まとめ 19
概要( 再掲) Googe DeepMind の研究,Nature(2024/1/17) に掲載 言語モデルと演繹的推論を組み合わせたAlphaGeometry を提案 平面幾何学の問題限定でIMO 金メダリストの平均的なスコアに迫る正解率を達成
(SOTA) 演繹的推論だけで導けない補助項の生成に言語モデルを利用 人間による注釈や問題文を使わず合成データだけで言語モデルを学習 学習データ不足になりがちな数学などの領域に対する一つの指針となるフレーム ワーク ※IMO ...International mathmatical Olympaid( 国際数学オリンピック) 20
None
関連するリンク 公式ページ https://deepmind.google/discover/blog/alphageometry- an-olympiad-level-ai-system-for-geometry/ Nature https://www.nature.com/articles/s41586-023-06747-5 GitHub https://github.com/google-deepmind/alphageometry