生成AI数学オリンピックに参加してみた結果
はじめに
コンテストの概要
2024年の5月、私はKaggleが主催する「AI Mathematical Olympiad」に参加しました。このコンテストは、生成AIを活用して数学オリンピックレベルの問題に挑戦するものです。主な内容は以下の通りです。
目的
AIモデルの数学的推論能力向上
コンペ内容:
LaTeX形式で提供される中高生レベルの数学問題（算数、代数、幾何を含む）を解く
国際的なチームが作成した110題の問題（難易度はAMC12とAIMEの間）
評価方法:
モデルの予測ラベルと正解ラベル（0～999の整数）の一致度で評価
コード要件:
ノートブックでの提出必須
CPU・GPU実行時間はそれぞれ最大9時間以内
インターネットアクセス無効
外部データや事前学習済みモデルの使用は許可
実際の問題例
1.
What is the minimum value of $5x^2+5y^2-8xy$ when $x$ and $y$ range over all real numbers such that $|x-2y| + |y-2x| = 40$?2.
Let $k, l > 0$ be parameters. The parabola $y = kx^2 - 2kx + l$ intersects the line $y = 4$ at two points $A$ and $B$. These points are distance 6 apart. What is the sum of the squares of the distances from $A$ and $B$ to the origin?3.
Let $k, l > 0$ be parameters. The parabola $y = kx^2 - 2kx + l$ intersects the line $y = 4$ at two points $A$ and $B$. These points are distance 6 apart. What is the sum of the squares of the distances from $A$ and $B$ to the origin?コンテストに参加した動機と目的
今回のコンテストに参加した動機は、たまたまコンテスト期間中に大学時代の同期と食事をする機会があり、その際にこのコンテストの話題が出たことがきっかけでした。数学に関連したこのコンテストが非常に面白そうだと感じ、参加を決めました。
私は大学時代に数学を専攻しており、現在は生成AIに特化したエンジニアとして活動しています。そのため、LLM（大規模言語モデル）やファインチューニングの勉強も兼ねて、このコンテストに挑戦しました。
アプローチ方法
実際のアプローチ方法
今回のコンテストでは、与えられた数学の問題を解決するために、Pythonのz3ライブラリを使用し、以下の手順に従ってアプローチしました。
データセットの作成とファインチューニング
まず、約300個のデータセットを作成し、そのデータを使用してモデルをファインチューニングしました。
問題文をJSON形式に変換
ファインチューニングしたモデルを使用して、与えられた数学の問題文を特定のJSON形式に変換しました。これにより、問題の構造を整理し、後続の処理がスムーズに進むようにしました。
実際のLLMに与えたプロンプト
このプロンプトは、LLMに対して数学の問題をステップバイステップで分類し、変数を抽出し、目的を定義し、制約をリスト化させるために使用しました。
template_solver = """You are an advanced AI system with exceptional mathematical reasoning and problem-solving capabilities, specifically designed to solve intricate math problems. Your task is to generate a comprehensive JSON representation of the following math problem. Please think step by step.
1. Classify Problem:
- `label`: Choose one from `'general'`, `'optimization'`, `'counting'`, or `'summation'`.
2. Extract Variables:
- `var`: List variables with types (`Real`, `Int`, `Bool`). Format: `["Type", "variable_name"]`.
- Example: `[["Real", "x"], ["Int", "y"]]`.
- Ensure **all** variables in constraints are listed here. You need to check it here carefully.
3. Define Objective:
- `target`: Specify the objective. For optimization: `["maximize": "variable"]` or `["minimize": "variable"]`.
- Example: `["maximize": "profit"]`, `["minimize": "cost"]`.
- For non-optimization: `"x"`.
4. List Constraints:
- `constraints`: List all constraints as strings in an array.
- Example: `[["x >= 1"], ["x <= 10"], ["y == 2"]]`,`[["x == Sqrt(9**3)"]]`, `[["result == LCM(9,12,15)"]]`
Problem:
{problem}
JSON representation:
{ai_output}
"""solve関数に入力
変換したJSON形式のデータをsolve関数に入力します。solve関数は、問題の種類に応じて最適な解法を選択し、解答を導き出します。
solve関数の詳細
solve関数は、問題の種類に応じて以下の4つの解法関数を呼び出します。
satisfiability・general（一般問題）
sat_solve関数: 一般的な充足可能性問題に対して、与えられた制約のもとで解を探索します。
counting（数を数える問題）
count_solve関数: 満たす解の数を数える問題に対して、全ての解を列挙し、その数をカウントします。
summation（合計を求める問題）
sum_solve関数: 全ての満足する解の合計を求める問題に対して、解の合計値を計算します。
optimization（最適化問題）
opt_solve関数: 最適化問題に対して、与えられた条件の下で最小化または最大化を行います。この関数は、結果の信頼性を高めるために複数回実行され、最も一般的な解を採用します。
実際のsolve関数
ここに示されるコードは、solve関数の実装例です。このコードは問題の種類に応じた適切な解法を実行するためのものです。
from z3 import *
from collections import Counter
# 数字の各桁の合計を計算する再帰関数
SumDigits = RecFunction('SumDigits', IntSort(), IntSort())
n = Int('n')
RecAddDefinition(SumDigits, n, If(n == 0, 0, (n % 10) + SumDigits(n / 10)))
# 階乗を計算する再帰関数
Factorial = RecFunction('Factorial', IntSort(), IntSort())
m = Int('m')
RecAddDefinition(Factorial, m, If(m == 0, 1, m * Factorial(m - 1)))
# 最大公約数 (GCD) を計算する再帰関数
GCD_prepare = RecFunction('GCD_prepare', IntSort(), IntSort(), IntSort())
a = Int('a')
b = Int('b')
RecAddDefinition(GCD_prepare, (a, b), If(b == 0, a, GCD_prepare(b, a % b)))
# 複数の数の最大公約数を計算する関数
def GCD(*args):
if len(args) == 1:
return args[0]
if len(args) == 2:
return GCD_prepare(args[0], args[1])
return GCD_prepare(args[0], GCD(*args[1:]))
# 最小公倍数 (LCM) を計算する再帰関数
LCM_prepare = RecFunction('LCM_prepare', IntSort(), IntSort(), IntSort())
RecAddDefinition(LCM_prepare, (a, b), If(Or(a == 0, b == 0), 0, (a * b) / GCD_prepare(a, b)))
# 複数の数の最小公倍数を計算する関数
def LCM(*args):
if len(args) == 1:
return args[0]
if len(args) == 2:
return LCM_prepare(args[0], args[1])
return LCM_prepare(args[0], LCM(*args[1:]))
# 制約付きの充足可能性問題を解く関数
def sat_solve(var, target, constraints, timeout=600000):
solver = Solver()
solver.set('timeout', timeout)
# 変数を設定
for var_type, var_name in var:
exec(f'{var_name} = {var_type}("{var_name}")')
# ターゲット変数をInt型に設定
exec(f'{target} = Int("{target}")')
# 制約を追加
for constr in constraints:
solver.add(eval(constr[0]))
if solver.check() == sat:
return solver.model()[eval(target)]
else:
raise RuntimeError("Constraints are unsatisfiable.")
# 満たす解の数を数える関数
def count_solve(var, target, constraints, timeout=600000):
count = 0
s = Solver()
s.set('timeout', timeout)
# 変数を設定
for var_type, var_name in var:
exec(f'{var_name} = {var_type}("{var_name}")', globals(), locals())
# 制約を追加
for const in constraints:
s.add(eval(const[0], globals(), locals()))
# 全ての解を数える
while s.check() == sat:
count += 1
model = s.model()
# 現在の解を除外する制約を追加
exclude_current = []
for var_type, var_name in var:
exclude_current.append(eval(f'{var_name} != model[{var_name}]', globals(), locals()))
s.add(Or(exclude_current))
return count
# 解の合計を求める関数
def sum_solve(var, target, constraints, timeout=600000):
total = 0
s = z3.Solver()
s.set('timeout', timeout)
# 変数を設定
for var_type, var_name in var:
exec(f'{var_name} = z3.{var_type}("{var_name}")')
# 制約を追加
for const in constraints:
s.add(eval(const[0], globals(), locals()))
# 解を合計する
while True:
if s.check() != z3.sat:
break
else:
solution = s.model()[eval(target, globals(), locals())]
total += solution.as_long()
s.add(eval(f'Not({target} == {solution})', globals(), locals()))
return total
# 最適化問題を解く関数
def opt_solve(var, target, constraints, timeout):
opt = z3.Optimize()
opt.set('timeout', timeout)
# 変数を設定
for var_type, var_name in var:
exec(f'{var_name} = z3.{var_type}("{var_name}")')
# ターゲット変数をInt型に設定
target_var_name = target[0][1]
exec(f'{target_var_name} = z3.Int("{target_var_name}")')
# 制約を追加
for constr in constraints:
opt.add(eval(constr[0], globals(), locals()))
# 最適化目標を設定
if target[0][0] == 'minimize':
opt.minimize(eval(target[0][1], globals(), locals()))
actual_target = target[0][1]
elif target[0][0] == "maximize":
opt.maximize(eval(target[0][1], globals(), locals()))
actual_target = target[0][1]
else:
raise ValueError("Target must include 'minimize' or 'maximize'.")
if opt.check() == z3.sat:
return opt.model()[eval(actual_target)]
else:
raise RuntimeError("Constraints are unsatisfiable.")
# 問題の種類に応じて適切な関数を呼び出す関数
def solve(label, var, target, constraints, timeout=600000):
if label == 'satisfiability' or label == 'general':
result = sat_solve(var, target, constraints, timeout)
elif label == 'counting':
result = count_solve(var, target, constraints, timeout)
elif label == 'summation':
result = sum_solve(var, target, constraints, timeout)
elif label == 'optimization':
results = []
for _ in range(3):
result = opt_solve(var, target, constraints, timeout)
results.append(result)
result_counts = Counter(results)
# 3回の試行で共通の結果が見つからない場合、最大5回まで試行
if len(result_counts) == 3:
for _ in range(2):
result = opt_solve(var, target, constraints, timeout)
results.append(result)
result_counts = Counter(results)
if result_counts.most_common(1)[0][1] > 1:
break
most_common_result, count = result_counts.most_common(1)[0]
if count == 1:
raise RuntimeError("No common result found in up to 5 tries.")
return most_common_result
else:
raise ValueError("'label' must be 'satisfiability', 'counting', 'summation', or 'optimization'.")
if not isinstance(result, int):
result = result.as_long()
if result < 0:
raise ValueError("Result must be non-negative.")
if result > 1000:
result %= 1000
return result例①: 具体的な問題の変換
例えば、以下の数学の問題を考えてみます。
What is the minimum value of $5x^2+5y^2-8xy$ when $x$ and $y$ range over all real numbers such that $|x-2y| + |y-2x| = 40$?この問題をファインチューニングされたモデルで処理すると、以下のようにJSON形式に変換されます。
{
"label": "optimization",
"var": [
["Real", "x"],
["Real", "y"],
["Real", "min_value"]
],
"target": [
["minimize", "min_value"]
],
"constraints": [
["Abs(x - 2*y) + Abs(y - 2*x) == 40"],
["min_value == 5*x**2 + 5*y**2 - 8*x*y"]
]
}
この変換結果の理由として、この問題は与えられた制約のもとで関数の最小値を求める「最適化問題」に分類されるためです。
例②: 具体的な問題の変換
次に、以下の数学の問題を考えてみます。
There exists a unique increasing geometric sequence of five 2-digit positive integers. What is their sum?この問題をファインチューニングされたモデルで処理すると、以下のようにJSON形式に変換されます。
{
"label": "general",
"var": [
["Int", "a"],
["Int", "b"],
["Int", "c"],
["Int", "d"],
["Int", "e"],
["Int", "sum"],
["Real", "ratio"]
],
"target": "sum",
"constraints": [
["9 < a"],
["a < b"],
["b < c"],
["c < d"],
["d < e"],
["e < 100"],
["sum == a + b + c + d + e"],
["a * ratio == b"],
["b * ratio == c"],
["c * ratio == d"],
["d * ratio == e"]
]
}この変換結果の理由として、この問題は一意な増加する等比数列を求め、その総和を計算する「一般的な問題」として分類されています。
他の参加者のアプローチとの比較
1位のアプローチ（Team Numina）
Team Numinaは、以下のような非常に先進的なアプローチを採用し、1位を獲得しました。
大規模なファインチューニング:
DeepSeekMath-Base 7Bモデルを使用し、2段階でファインチューニングを行いました。まず、大規模な自然言語の数学問題を使用して基本的な推論能力を高め、その後、ツール統合型推論（Python REPLとの統合）に対応するデータセットで再ファインチューニングしました。
高度な推論アルゴリズム:
自己一貫性を持つツール統合型推論（SC-TIR）を採用し、複数の解候補を生成して、最も適切な解を選択する方法で精度を高めました。これにより、異なる条件下でも安定した結果を得ることができました。
検証セットの活用:
AMCやAIMEといった厳選された検証セットを用いてモデルを評価し、過学習を防ぎつつ、異なる難易度の問題に対するモデルの性能を最適化しました。
私のアプローチとの違い
私のアプローチと比較すると、以下のような違いがあります。
ファインチューニングの規模と方法:
私は約300個のデータセットを使用してファインチューニングを行いましたが、Team Numinaははるかに大規模なデータセットと2段階のファインチューニングプロセスを採用していました。これにより、彼らのモデルはより広範な数学問題に対応する能力を得ていました。
推論アルゴリズム:
私はsolve関数を使用して、問題の種類に応じたシンプルな推論アルゴリズムを適用しましたが、Team Numinaはより高度なSC-TIRアルゴリズムを使用して解答の精度を高めていました。
参考：
終わりに
今回のKaggleコンペティション「AI Mathematical Olympiad」では、残念ながら期待していた結果を得ることはできませんでした。その原因としては、以下の2つが主な要因だと考えています。
うまくいかなかった理由
ファインチューニングの知識の不足:
ファインチューニングの手法や最適化についての知識が不足していたことが、モデルの性能向上を妨げた要因の一つです。適切なファインチューニングを行うためには、データの選定、学習率の調整、エポック数の決定など、多くの要素を深く理解する必要がありますが、これらを十分に行えなかったことが結果に影響したと考えています。
データセットの量と質:
使用したデータセットの量が限られていたこと、そしてその質が他の上位参加者に比べて劣っていたことが、モデルのパフォーマンスを制約しました。大規模かつ多様なデータセットを使用することで、モデルはより広範な問題に対応する能力を得ることができますが、今回はそれが不十分でした。
振り返りと今後の展望
今回のアプローチがうまくいけば、より良い結果、さらには1位を目指すことも可能だったと感じています。特に、LLMに問題文からJSON形式を生成させる部分は、他の参加者に比べて効率的であり、強みとなり得た部分です。多くの参加者が問題文から直接Pythonコードを生成させている中、私のアプローチでは中間形式を利用することで、モデルの理解を助け、より正確な解答を導き出すことができたと考えています。
しかし、今回のアプローチでは限界も明らかになりました。特に、確率や図形に関する問題では、モデルが十分な精度で解答を導き出すことができませんでした。これらの問題タイプは、solve関数で解くことが難しいため、JSON形式への変換が難しく、適切な制約や変数の設定が困難であるため、今後の課題として取り組んでいきたいと考えています。
今後は、ファインチューニングの知識を深め、質の高いデータセットを収集・作成することで、モデルの性能をさらに向上させていきたいと思います。また、今回の経験を糧に、次回のコンペティションではより良い結果を目指し、さらなる成長を遂げたいと考えています。
この記事が、同じように生成AIや数学に挑戦している方々にとって何かしらの参考になれば幸いです。引き続き、生成AIの可能性を探求し、新たなチャレンジを続けていきたいと思います。
お仕事の依頼・相談について
提供できるサービス
私は、以下のようなシステム開発とコンテンツ作成を幅広くサポートしています。OpenAI API・ファインチューニングをはじめとするさまざまな技術を活用し、お客様のニーズに合わせたソリューションを提供します。
自動化システムの構築：AIを利用したカスタマーサポート、FAQシステム、チャットボットなど、業務効率化を図るためのシステムを構築します。ニーズに応じて最適なツールや技術を組み合わせて対応します。
GPTs/Dify開発：OpenAIの技術を活用し、カスタムGPTモデルやDifyを使用したシステム開発をサポートします。
コンテンツ作成：AIを活用したコンテンツ作成を支援します。ブログ記事、マーケティング資料、教育コンテンツなど、さまざまな分野でのコンテンツを作成します。
詳しくはこちら：
案件のご相談はこちらから
これらの技術やサービスに興味がある方、または具体的なプロジェクトのご相談がある方は、ぜひお気軽にご連絡ください。お客様のニーズに合った最適なソリューションを提供いたします。
X(Twitter)のDMでもお問い合わせいただけます。X(Twitter)での問い合わせはこちら
おまけ
実際に使用したデータセット
ここでは、今回のコンペティションで実際に使用したデータセットとその作成方法について説明します。このデータセットは、問題文を特定のJSON形式に変換するために作成されました。
データセットの作成方法
以下の記事で紹介している方法を使用しました。
実際のGASのコード
以下に、Google Apps Script（GAS）を使用してデータセットを作成するためのコードを示します。このコードは、OpenAIのAPIを利用して、問題文を特定のJSON形式に変換するものです。
const OpenAI_API_KEY = "your_openai_api_key_here";
const MAX_TOKENS = 4000;
const MODEL_NAME = "gpt-4o";
const MODEL_TEMP = 0.7;
function generateResponse(prompt) {
const url = "https://api.openai.com/v1/chat/completions";
const payload = {
model: MODEL_NAME,
messages: [
{role: 'system', content: `Do not solve a math problem. You just need to output the specific JSON format.
#### Instruction:
Generate a JSON representation of this math problem:
1. Classify Problem:
- 'label': Choose one from 'general', 'optimization', 'counting', or 'summation'.
2. Extract Variables:
- 'var': List variables with types ('Real', 'Int', 'Bool'). Format: ['Type', 'variable_name'].
- Example: [['Real', 'x'], ['Int', 'y']].
- Ensure **all** variables in constraints are listed here. You need to check it here carefully.
3. Define Objective:
- 'target': Specify the objective. For optimization: ['maximize': 'variable'] or ['minimize': 'variable'].
- Example: ['maximize': 'profit'], ['minimize': 'cost'].
- For non-optimization: 'x'.
4. List Constraints:
- 'constraints': List all constraints as strings in an array.
- Example: [['x >= 1'], ['x <= 10'], ['y == 2']], [['x == Sqrt(9**3)']], [['result == LCM(9,12,15)']]
#### Example Problems and JSON Outputs:
1. **Optimization Problem**:
- **Problem**: What is the minimum value of \(5x^2+5y^2-8xy\) when \(x\) and \(y\) range over all real numbers such that \(|x-2y| + |y-2x| = 40\)?
- **JSON Output**:
{
"label": "optimization",
"var": [
["Real", "x"],
["Real", "y"],
["Int", "min_value"]
],
"target": [
["minimize": "min_value"]
],
"constraints": [
["Abs(x - 2*y) + Abs(y - 2*x) == 40"],
["min_value == 5*x**2 + 5*y**2 - 8*x*y"]
]
}
2. **General Problem**:
- **Problem**: Let \(k, l > 0\) be parameters. The parabola \(y = kx^2 - 2kx + l\) intersects the line \(y = 4\) at two points \(A\) and \(B\). These points are distance 6 apart. What is the sum of the squares of the distances from \(A\) and \(B\) to the origin?
- **JSON Output**:
{
"label": "general",
"var": [
["Real", "k"],
["Real", "l"],
["Real", "x1"],
["Real", "x2"],
["Real", "y1"],
["Real", "y2"],
["Real", "result"]
],
"target": "result",
"constraints": [
["k > 0"],
["l > 0"],
["y1 == k*x1**2 - 2*k*x1 + l"],
["y2 == k*x2**2 - 2*k*x2 + l"],
["y1 == 4"],
["y2 == 4"],
["Abs(x1 - x2) == 6"],
["result == x1**2 + y1**2 + x2**2 + y2**2"]
]
}
3. **Counting Problem**:
- **Problem**: How many positive perfect squares less than \(2023\) are divisible by \(5\)?
- **JSON Output**:
{
"label": "counting",
"var": [
["Int", "x"]
],
"target": "x",
"constraints": [
["x > 0"],
["x**2 <= 2023"],
["x % 5 == 0"]
]
}
4. **General Problem**:
- **Problem**: There are two integers, one large and one small. The larger integer is 2 smaller than 4 times the smaller integer, and if we subtract 7 times the smaller integer from 2 times the larger integer, we get 1. Find these two integers and answer the sum of the two integers.
- **JSON Output**:
{
"label": "general",
"var": [
["Int", "x"],
["Int", "y"],
["Real", "result"]
],
"target": "result",
"constraints": [
["x < y"],
["y == 4*x - 2"],
["2*y - 7*x == 1"],
["result == x + y"]
]
}
5. **Isometric and Equi-Difference Sequence**:
- **Problem**: There are three numbers \(x\), \(y\), and \(z\) which are distinct from each other and in this order form an isometric sequence. Also, \(z,x,y\) form an equi-difference sequence in this order. \(x+y+z = 3\), give the value of \(z\].
- **JSON Output**:
{
"label": "general,",
"var": [
["Real", "x"],
["Real", "y"],
["Real", "z"],
["Real", "d"],
["Real", "ratio"]
],
"target": "z",
"constraints": [
["y == x + d"],
["z == y + d"],
["x == z * ratio"],
["y == x * ratio"],
["x + y + z == 3"],
["d != 0"]
]
}
---
### Summary of Key Points:
- **Understand** the problem thoroughly before generating the output.
- **Generate** a structured JSON output adhering to the specified format.
- Ensure the JSON structure includes **label**, **var**, **target**, and **constraints**.
- Use **examples** as references to construct your output correctly.`},
{role: 'user', content: prompt.toString()}
],
temperature: MODEL_TEMP,
max_tokens: MAX_TOKENS,
};
const options = {
contentType: "application/json",
headers: { Authorization: "Bearer " + OpenAI_API_KEY },
payload: JSON.stringify(payload),
};
return JSON.parse(UrlFetchApp.fetch(url, options).getContentText()).choices[0].message.content.trim();
}
確率問題を解かせる方法
今回のコンペティションにおいて、ファインチューニングの際には使用しませんでしたが、確率問題を解かせるためのsolve関数とデータセットも別途作成していました。このセクションでは、その詳細と使用しなかった理由について説明します。
確率問題を解かせるsolve関数
以下に示す関数は、確率問題を解決するために作成したものです。この関数は、指定された条件に基づいて試行を繰り返し、確率を計算します。
def solve_dice(dices, sides, probability_target, probability_constraints):
trials = 100000
allcases = dices**sides
success = 0
for _ in range(trials):
dice = list([random.randint(1,sides) for _ in range(dices)])
for condition in probability_constraints:
condition = eval(condition)
count = 0
if condition == True:
count += 1
success += 1
probability = Fraction(round(success*allcases/trials),allcases)
numerator = probability.numerator #分子
denominator = probability.denominator #分母
answer = eval(probability_target)
return answerこの関数は、サイコロの目や回数に基づいて確率を計算します。100,000回の試行を行い、指定された条件を満たす回数をカウントし、その確率を計算して結果を返す仕組みです。
確率問題データセット
使用しなかった理由
確率問題のsolve関数とデータセットを使用しなかった主な理由は、JSON形式の構造が他の問題タイプとは異なるためです。確率問題に特化したJSON形式は、他の一般的な問題や最適化問題とは異なる構造を持っており、これがファインチューニング時にモデルの一貫性を乱し、全体的な精度を下げる原因となる可能性がありました。
一緒にこのコンテストに参加してくれた筑波大学の数学専攻の仲間たちありがとうございました。
トなかい
酒井綺香
この記事が気に入ったらサポートをしてみませんか？