The 28th Annual Conference of the Japanese Society for Artificial Intelligence, 2014
3D3-5
数学入試問題
数式処理
性能評価
Performance Evaluation of Symbolic Computation System on
University Entrance Examination Problems
矢吹 太朗 ∗1
Taro Yabuki
∗1
千葉工業大学 社会
科学部
Faculty of Social Systems Science, Chiba Institute of Technology
In trying to solve mathematical problems by artificial intelligence, the problems are transformed to first order
logic expression and solved by mathematical algorithms such as quantifier elimination. In this paper, we transform
mathematical problems of the University of Tokyo entrance examination in 1988 by hand, and try to solve them
by mathematical algorithms. By measuring computation time and required storage capacity, and by checking
knowledge introduced by us, effectiveness and validity of the method are discussed.
AbsoluteTime[] 1900 年 1 月 1 日
秒単位
経過時
間 与
．
MaxMemoryUsed[]
保存
使
最大
数 与
．
MaxValue[{f, cons }, {x, y, ...}, dom ] 制約条件 cons
下
f
最大値 与
．同様 ，MinValue[]
最小値 与
．
Reduce[expr, vars, dom ] 領域 dom ，vars
方
程式
不等式 解 ，限定子 除去
，命
題 expr 簡約
．
Refine[expr, assum ] expr 中
仮定 assum
満足
明示的 数式 置換
際 得
expr 形 与
．
Solve[expr, vars, doms ] 領域 doms ，方程式 系 expr
解 変数 vars
求
．
1.
用
分
第1
試
数学 問題 解 試
，大
2
．
数学
活用
．Computer based math∗1
，
導入
，数学教育 変革
提唱
．手 問題 解 際 ，
利用
問題
解 際
，
解法 大
異
場合
，
，数学教育
導入
，学習 通
獲得
能力 大
異
得 ．
第2 ，
「
東大 入
」
，
人工知能
試
．大学入試
数学 問題 人工知能
解 試
，問題文 一階
述語論理式 変換 ，限量記号消去法（quantifier elimination,
QE）
数式処理
適用
採用
[松崎 13]．自然言語 書
問題文
処理
形 自動変換
難
，変換
問題 解
思
，必
．
以上 背景 踏
，大学入試 数学 問題 ，
（数式処理
） 処理
人手 変換
解
，手 解 場合
利用
解 場合 考 方 違
確認
，数式処理
適
用可能性 検討
目指 ．
2.
，
，取 組 問題
．
1988 年 東京大学 理系 第 1 問
2.1
Raspberry Pi Model B（ARM11
700 MHz，主記
憶 512MB）上 動作
Mathematica 10.0 for Linux ARM
(32-bit) (November 19, 2013) 利用
．
問題 取 組 際 用
Mathematica 主 関数 以下
∗2
．引数
省略
．
通
xy 平面上 一次変換 f
https://www.computerbasedmath.org/
http://reference.wolfram.com/language/
3 条件
．
f
第 4 象限
内部
．
(ii) 点 (0, 1)
f
第 2 象限
内部
．
(iii) 点 (1, 1)
f
第 1 象限
内部
．
1
次
(i) 点 (1, 0)
f (P)
連絡先: https://twitter.com/yabuki/
∗1
∗2
問題 解答方針
1988 年 東京大学理系数学 入試問題全 6 題 取 組 （本
番 試験時間 150 分．配点 440 点中 120 点）．
年
出題
全問題 扱
，
大学入試数学
思
．1988 年 問題 扱
，東大入試数学
有名 難問 2 題 含
．実際，文献 [大数 93]
，第 2 問 第 3 問
，
「結論 予想
容易
，
解答
極
困難 超難問
」
，
「方針 立
，計算 十分
難問
」
記載
，
文献 [聖文新社 08]
，
「高度 読解力 図形的
，強靱
論理的思考力 粘 強 計算力」 要
問題 代表例
，
2 題 紹介
．
取 組 問題 解答方針 以下 示 ．
手法
本研究 用
解答方針 確認
取 組
2.2
f
逆変換 存在
第 1 象限 内部
示 ．
，点 P
示 ．
，点 P 像
第 1 象限 内部
The 28th Annual Conference of the Japanese Society for Artificial Intelligence, 2014
1. 仮定 述語
記述
．
2. 証明
命題，設問 前半 「一次変換 対応
行列
行列式 0
」 ，後半 「点 P 像 (x, y)
，
逆写像 第 1 象限
」 記述
．
3. Refine[] 使
命題 真
確認
（本研
究
，
証明 代
仮定
）．
問題文
明示
，以下 知識
利用
RotationMatrix[c, {0, 0, 1}].
RotationMatrix[b, {0, 1, 0}].
RotationMatrix[a, {1, 0, 0}].p], v1];
v3 = Map[Function[{p}, p + {x, y, z}], v2];
v4 = Map[Function[{p}, Take[p, 2]], v3];
s1 = FullSimplify[Total[Map[area, Subsets[v4, {3}]]]/2];
s2 = FullSimplify[s1 /.
{Cos[a] -> A, Sin[a] -> B, Cos[b] -> P, Sin[b] -> Q},
And[A^2 + B^2 == 1, P^2 + Q^2 == 1]];
．
MaxValue[{s2, And[A^2 + B^2 == 1, P^2 + Q^2 == 1]},
{A, B, P, Q}] (* 出力：1/2 *)
(a) 2 次元平面 一次変換 ，2 行 2 列 行列 表現
．
(b) 一次変換 逆変換 存在
，対応
行列 行
列式 0
同等
．
問題 解
以下 示
MinValue[{s2, And[A^2 + B^2 == 1, P^2 + Q^2 == 1]},
{A, B, P, Q}] (* 出力：1/(2*Sqrt[2]) *)
1988 年 東京大学 理系 第 3 問
．
y = x3 − x, −1 ≤ x ≤ 1 与
xy 平面上 図形
．次 条件
xy 平面上 点 P 全体 集合 図示
．
「C 平行移動
図形 ，点 P 通 ，
図形 C
共有点
1点
，
3 個存在
．」
C
A = {{a, c},
assum = And[
With[{p =
With[{p =
With[{p =
{b, d}};
A.{1, 0}}, And[p[[1]] > 0, p[[2]] < 0]],
A.{0, 1}}, And[p[[1]] < 0, p[[2]] > 0]],
A.{1, 1}}, And[p[[1]] > 0, p[[2]] > 0]]];
Refine[Det[A] != 0, assum] (* 出力：True *)
Refine[
With[{p = Inverse[A].{x, y}}, And[p[[1]] > 0, p[[2]] > 0]],
And[x > 0, y > 0, assum]] (* 出力：True *)
1988 年 東京大学 理系 第 2 問
空間内 平面 α
．一辺 長 1 正四面体 V
α上
正射影 S
，V
位置 変
S
最大値 最小値 求
．
，空間 点 P 通
α 垂直 直線 α 交
点
P
α上
正射影
，空間図形 V
各点 α 上
正射影全体
α 上 図形 V
α上
正射影
．
1.
2.
3.
4.
5.
明示
，以下 知識
利用
1. C
x 方向 a，y 方向 b 平行移動
．
2. C 平行移動
図形 C 共有点
1点
条件 記述 ，condition
．
3. 点 P 座標 (X, Y )
，
C 平行移動
図
形上 点
，条件 condition
eqn
．
4. 条件 eqn
(a, b)
3 個存在
条件 ，限定子 使
記述
．
5. Reduce[] 使
限定子 消去 ，
結果得
(X, Y ) 関係 図示
．
問題文
一辺 長 1 正四面体 頂点 座標 適当 決
．
頂点 座標変換
．
頂点 xy 平面上
正射影 求
．
頂点 正射影
含 最小 凸多角形 面積 求
．
MaxValue[]
MinValue[] 使
面積 最大値 最
小値 求
．
問題文
明示
，以下 知識 利用
(a) y = f (x) x 方向
f (x − a)
．
(b) 3 次方程式
a, b
解 持
不要）．
．
(a) 平面 α xy 平面
．
(b) 「
位置 変
」
操作，
3 次元
空間
移動 ，x, y, z
軸 周
回転 平
行移動 合成 表現
．
(c) 頂点 正射影
考
十分
．
(d) 2 次元
A, B, C 作
三角形 面積 ，
Abs[Det[B - A, C - A]]/2
．
(e) 平面上 4 点 含 最小 凸多角形 面積 ，4 点
作
4 個 三角形 面積 和 1/2
．
(f) 三角関数 含 式 最大値 最小値 ，A = cos a, B =
sin a
三角関数 変換 ，A2 + B 2 = 1
条件 追加
，MaxValue[]
MinValue[] 計算
[穴井 11]．
条件
a，y 方向
b 平行移動
．
y−b =
3個 解 持 ．
持 x
，次
方程式 f (x) = 0
1
記述
（実行
Reduce[Exists[x1, f[x1] == 0,
ForAll[x2, f[x2] == 0, x1 == x2]], {a, b}]
応用
，方針 1
3
次
実行
．
condition = Simplify[Reduce[
Exists[x1, And[-1 <= x1 <= 1, -1 <= x1 - a <= 1,
x1^3 - x1 == (x1 - a)^3 - (x1 - a) + b],
ForAll[x2, And[-1 <= x2 <= 1, -1 <= x2 - a <= 1,
x2^3 - x2 == (x2 - a)^3 - (x2 - a) + b],
x1 == x2]], {a, b}, Reals]]
(* 出力：a^3 == 4 (a + b) && (-2 <= a < 0 || 0 < a <= 2) *)
eqn = And[Y == (X - a)^3 - (X - a) + b,
-1 <= X - a <= 1, condition];
Needs["PolyhedronOperations‘"]
area[{A_, B_, C_}] := Abs[Det[{B - A, C - A}]]/2;
条件 eqn
a
3 次方程式 見
（b
a
従属
）
．題意
図形
3 個存在
，
3 次方程式
3個 解 持
．
X, Y
持 a 方程式 f (a) = 0 異
解 持
条件 ，次
記述
（実行 不要）
．
v1 = PolyhedronData["Tetrahedron", "VertexCoordinates"];
v2 = Map[Function[{p},
Reduce[Exists[{a1, a2},
And[f[a1] == 0, f[a2] == 0, a1 != a2]], {X, Y}]
問題 解
以下 示
．
2
The 28th Annual Conference of the Japanese Society for Artificial Intelligence, 2014
応用
方針 4 以降
実行
問題 解
．
RegionPlot[region, {X, -1, 1}, {Y, -1, 1},
PlotPoints -> 50, MaxRecursion -> 8] (* 出力 図 1(a)．*)
1988 年 東京大学 理系 第 4 問
，以下 知識
以下 示
明示
，以下 知識 利用
．
(0, 0, 1)
．
(0, 0, 1)
，四面体 ABCD 体積 最大
，BCD 含 平面 xy 平面 平行
．
(c) 3 次元
a, b, c, d 作
四面体 体積 ，
Cross[b - a, c - a].(d - a)/6
．
(a) A
(b) A
問題 解
a
b
c
d
f
．
=
=
=
=
=
以下
示 ．
{0, 0, 1};
{4 Cos[t], 0, -4 Sin[t]};
{4 Cos[t] Cos[u], 4 Cos[t] Sin[u], -4 Sin[t]};
{4 Cos[t] Cos[v], 4 Cos[t] Sin[v], -4 Sin[t]};
Simplify[Cross[b - a, c - a].(d - a)/6]
体積 f
．
，次
t
関数
v
関数 積
( )
(
u
xyz 空間
，xz 平面上 0 ≤ z ≤ 2 − x2 表
形 z 軸
回転
得
不透明 立体 V
．V
表面上 z 座標 1
点光源 P
xy 平面上 原点 中心
円 C ，P
光 当
部分 長
2π
，C
部分 長
．
( )
図
f=
点 P 座標 (1, 0, 1)
．
点P 通 V
接平面 求
．
接平面 xy 平面 交線 x = X 求
．
光 当
部分 弧 対応
中心角 t
式 2rt = 2π, r cos t = X 立
．
5. Solve[] 使
方程式 解 ，r 求
．
6. 求
長 ，2πr − 2π 計算
．
)
.
，f
最大値 次
求
．
求
1.
2.
3.
4.
32
u
v
u−v
(4 sin t + 1) cos2 t sin
sin
sin
3
2
2
2
．
，以下 知識
求
問題文
．
1988 年 東京大学 理系 第 5 問
明示
最大値
条
Simplify[Reduce[Exists[n, Or[
And[s != 1, b < (s^(1 - n) (s^n - 1))/(a (s - 1))],
And[s == 1, b < n/a]]],
{a, s, b}, Reals], And[0 < a, 0 < b, 0 < s]]
(* 出力：s <= 1 || b < s/(a*(-1 + s)) *)
問題文
体積
1. A, B, C, D 座標
表示
．
2. 四面体 ABCD 体積 求
．
3. MaxValue[] 使
体積 最大値 求
．
(a) y 値 整数 点
調
十分
．
∑n i−1
n
x
x
=
̸
1
(x
−
1)/(x
−
1)
，
x=1
(b)
i=1
n
（単純 Sum[x^(i - 1), {i, 1, n}]
，x = 1 場合 考慮
）．
問題 解
，4 点 A, B, C, D
，四面体 ABCD
，
利用
対
．
関
点O
OA = 1, OB = OC = OD = 4
明示
1988 年 東京大学 理系 第 6 問
空間内
xy 平面上 原点
傾 a（a > 0） 出発 折 線状 動
点P 考
．
，点 P
y 座標
増加 ，
値
整数
動 方向 傾
s 倍（s > 0） 変化
．
P 描 折 線 直線 x = b（b > 0） 横切
a, b, s
関
条件 求
．
問題文
示 ．
cond = Reduce[ForAll[{x, y, z},
And[z == 2 - (x^2 + y^2),
a (x - 1) + b y + (z - 1) == 0],
And[x == 1, y == 0, z == 1]], {a, b}, Reals];
splane = (a (x - 1) + b y + (z - 1) == 0) /.
First[Solve[cond, {a, b}]];
X = x /. First[Solve[splane /. {z -> 0}, x]];
sol = Solve[And[2 r t == 2 Pi, r Cos[t] == X], {r, t}, Reals];
(2 Pi r - 2 Pi) /. First[sol] (* 出力：4 Pi *)
region = Reduce[Exists[{a1, a2, a3, b1, b2, b3},
And[
eqn /. {a -> a1, b -> b1},
eqn /. {a -> a2, b -> b2},
eqn /. {a -> a3, b -> b3},
(a1 != a2), (a2 != a3), (a3 != a1)
]], {X, Y}, Reals];
1. y = n 対応
x 求
．
2. x b
大
n 存在
限定子 使
記述
．
3. Reduce[] 使
限定子 消去 ，a, b, s
件 求
．
以下
With[{
p1min = MinValue[{part1, 0 <= t < Pi},
p1max = MaxValue[{part1, 0 <= t < Pi},
p2min = MinValue[{part2,
And[0 <= u < 2 Pi, 0 <= v < 2 Pi]},
p2max = MaxValue[{part2,
And[0 <= u < 2 Pi, 0 <= v < 2 Pi]},
If[And[p1max > 0, p2max > 0],
If[And[p1min < 0, p2min < 0],
Max[p1max p2max, p1min p2min],
p1max p2max]]] (* 出力：9 Sqrt[3] *)
，方程
利用
(a) 対称性
，点 P 座標 (1, 0, 1)
．
(b)
，点 P
V 接平面 対
同 側
領域
．
(c) 接平面 a(x − 1) + by + (z − 1) = 0 形 記述
part1 = 32 Cos[t]^2 (1 + 4 Sin[t]);
part2 = f/part1;
．
3.
．
3
{u, v}],
{u, v}]},
結果
全 6 問 解答 結論（第 3 問 結論
結論
中 記載） ，[大数 93]
一致
．
計算時間 利用記憶容量 表 1 通
，V
{t}],
{t}],
図 1(a)，他
掲載
．
問題
The 28th Annual Conference of the Japanese Society for Artificial Intelligence, 2014
，比較的簡単
掲載
異
．
y
1.0
1.0
I-
3
5
72
125
1
y= Hx3 -3x2 -x+3-xL
4
M
0.5
0.5
-1.0
0.5
-0.5
1.0
x
-0.5
-0.5
1
y= Hx3 +3x2 -x-3L
4
-1.0
-1.0
-0.5
0.0
0.5
1.0
(a) 本手法 結果
I
3
5
72
M
- 125
-1.0
1
y= Hx3 -9xL
9
(b) 模範解答
図 1: 第 3 問 解答
問題
第1問
第2問
第3問
第4問
第5問
第6問
4.
表 1: 計算時間 利用記憶容量
計算時間（秒） 利用記憶領域（MB）
4.6
10
3.3 × 103
35
1.5 × 102
71
3.2 × 10
18
6.8 × 10
21
7.0 × 10
17
考察
大学入試 数学 問題 数式処理
使
解
，問題文
数式処理
用 言語 置 換
，問題
理解 基
対称性
発見 ，計算量 減
工夫 必要
．
数学 学習 数式処理
導入
場合
，手 解 場合 ，数式処理
利用
解 場合
，解 方 大
異
注意
．数
式処理
利用
学習
身
能力 ，数学
学習
身
期待
能力 違
明
研究 必要
．
結論（真偽値 数値，図形） 模範解答
一致
，
得
結果 数学的 正
，大学入試
正解 見
．
，Mathematica
7
Reduce[] ，
350
Mathematica
1400
C
使
[Wolfram 11]，試験 採点者
検証
現
実的
．
4.1
解法 ，文献 [小島 89]
，人間 手 解 方法
大
5.
大学入試 数学 問題 ，数式処理
用
現実的
解
確認
．
解法 手 解 場合
異
，問題
理解 基
知識 必要
．
事例 積 重
，数学教育 改
善
，人工知能研究 進展
期待
．
参考文献
[Wolfram 11] Wolfram Research, I.: Some Notes on Internal Implementation (2011)
[穴井 11] 穴井 宏和, 横山 和弘：QE
応用, 東京大学出版会 (2011)
各論
4.1.1 第 1 問
後半 問
対
，点 P 自体 (x, y)
解
，点 P 像 (x, y)
命題 記述
変数 導入方法
，試行錯誤 必要
．
4.1.2 第 2 問
知 識 (e)
受験数学 学
思
MaxValue[]
MinValue[] 利用
，
，
数式 表現
知識 有用
．
知識 (f) 用
，面積 三角関数 記述
MaxValue[] MinValue[] 最大値 最小値 求
．三角関数 含 式 関
問題
，
変数変換 有力
．
難問
有名 本問
，数式処理
利用
．
4.1.3 第 3 問
a
3 次方程式
初
知識
(b) 利用
．
，具体的 方針 事前 決
難
場合
．
，模範解答 図
本手法
第 3 問 結論 図 1(a)
1(b)
，曲線 式 交点 座標，曲線自体 点自体
含
描
．
4.1.4 第 4 問
∑n
Mathematica
， i=1 xi−1
簡単 計算 ，特
殊 仮定（
場合 x ̸= 1） 下 行
危険
知
．
Reduce[] 引数 {a, s, b} {a, b, s}
解
．変数 順番 大切
．
4.1.5 第 5 問
接平面 (x − 1) + ay + b(z − 1) = 0 形 記述
，計
算時間 68 秒
3300 秒 ，利用記憶容量 21 MB
230 MB 増加
．
，得
結果 同等
，
変数 導入方法
計算時間 大
異
場合
．
4.1.6 第 6 問
問題
定式化
，現実的 時間
解
．
(a)，(b)
知識
，計算量 減
必要
．
体積 f ，t 関数 u v 関数 分
，MaxValue[]
最大値 求
．f
2
部分 分
，解
途中 初
．
第 3 問 同様，具体的 方針 事前 決
難
．
y=x3 -x
0.0
解
計算
[小島 89] 小島 寛之：
花束
Vol. 33, No. 11–12, pp. 56–57 (1989)
．
, 大学
数学,
[松崎 13] 松崎 拓也, 岩根 秀直, 穴井 宏和, 相澤 彰子, 新井 紀
子：深 言語理解 数式処理 接合
入試数学問題解
答
, 人工知能学会全国大会論文集 (CD-ROM), pp.
2A4–1 (2013)
，
[聖文新社 08] 聖文新社 編集部（編）
：東京大学 数学入試問題
50 年, 聖文新社 (2008)
，
[大数 93] 大学
数学 編集部（編）
：東大入試・10 年 軌跡,
東京出版 (1993)
4
© Copyright 2024 ExpyDoc
