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.
1.
用
数学 問題 解 試
,大
2
分
.
第
1
,
数学
活用
試
.
Computer based math
∗1,
導入
,数学教育 変革
提唱
.手 問題 解 際 ,
利用
問題
解 際
,
解法 大
異
場合
,
,数学教育
導入
,学習 通
獲得
能力 大
異
得 .
第
2
,
「
東大 入
」
,
人工知能
試
.大学入試
数学 問題 人工知能
解 試
,問題文 一階
述語論理式 変換 ,限量記号消去法(
quantifier elimination,
QE
)
数式処理
適用
採用
[
松崎
13]
.自然言語 書
問題文
処理
形 自動変換
難
,変換
問題 解
思
,必
.
以上 背景 踏
,大学入試 数学 問題 ,
(数式処理
) 処理
人手 変換
解
,手 解 場合
利用
解 場合 考 方 違
確認
,数式処理
適
用可能性 検討
目指 .
2.
手法
本研究 用
,取 組 問題
解答方針 確認
.
2.1
Raspberry Pi Model B
(
ARM11
700 MHz
,主記
憶
512MB
)上 動作
Mathematica
10.0 for Linux ARM
(32-bit) (November 19, 2013)
利用
.
問題 取 組 際 用
Mathematica
主 関数 以下
通
∗2.引数
省略
.
連絡先
:
https://twitter.com/yabuki/
∗1 https://www.computerbasedmath.org/∗2 http://reference.wolfram.com/language/
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
求
.
2.2
取 組 問題 解答方針
1988
年 東京大学理系数学 入試問題全
6
題 取 組 (本
番 試験時間
150
分.配点
440
点中
120
点).
年
出題
全問題 扱
,
大学入試数学
思
.
1988
年 問題 扱
,東大入試数学
有名 難問
2
題 含
.実際,文献
[
大数
93]
,第
2
問 第
3
問
,「結論 予想
容易
,
解答
極
困難 超難問
」,「方針 立
,計算 十分
難問
」
記載
,
文献
[
聖文新社
08]
,「高度 読解力 図形的
,強靱
論理的思考力 粘 強 計算力」 要
問題 代表例
,
2
題 紹介
.
取 組 問題 解答方針 以下 示 .
1988
年 東京大学 理系 第
1
問
✓
✏
xy平面上 一次変換f 次 3条件 . (i) 点(1,0) f 第4象限 内部 . (ii) 点(0,1) f 第2象限 内部 . (iii) 点(1,1) f 第1象限 内部 .
f 逆変換 存在 示 . ,点P 像
f(P) 第1象限 内部 ,点P 第1象限 内部
示 .
✒
✑
The 28th Annual Conference of the Japanese Society for Artificial Intelligence, 2014
1.
仮定 述語
記述
.
2.
証明
命題,設問 前半 「一次変換 対応
行列
行列式
0
」 ,後半 「点
P
像
(
x, y
)
,
逆写像 第
1
象限
」 記述
.
3.
Refine[]
使
命題 真
確認
(本研
究
,
証明 代
仮定
).
問題文
明示
,以下 知識 利用
.
(a) 2
次元平面 一次変換 ,
2
行
2
列 行列 表現
.
(b)
一次変換 逆変換 存在
,対応
行列 行
列式
0
同等
.
問題 解
以下 示 .
A = {{a, c}, {b, d}}; assum = And[
With[{p = A.{1, 0}}, And[p[[1]] > 0, p[[2]] < 0]], With[{p = A.{0, 1}}, And[p[[1]] < 0, p[[2]] > 0]], With[{p = 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.
一辺 長
1
正四面体 頂点 座標 適当 決
.
2.
頂点 座標変換
.
3.
頂点
xy
平面上
正射影 求
.
4.
頂点 正射影
含 最小 凸多角形 面積 求
.
5.
MaxValue[]
MinValue[]
使
面積 最大値 最
小値 求
.
問題文
明示
,以下 知識 利用
.
(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
三角関数 変換 ,
A
2+
B
2= 1
条件 追加
,
MaxValue[]
MinValue[]
計算
[
穴井
11]
.
問題 解
以下 示 .
Needs["PolyhedronOperations‘"]
area[{A_, B_, C_}] := Abs[Det[{B - A, C - A}]]/2;
v1 = PolyhedronData["Tetrahedron", "VertexCoordinates"]; v2 = Map[Function[{p},
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 *)
MinValue[{s2, And[A^2 + B^2 == 1, P^2 + Q^2 == 1]}, {A, B, P, Q}] (* 出力:1/(2*Sqrt[2]) *)
1988
年 東京大学 理系 第
3
問
✓
✏
C y=x3
−x,−1≤x≤1 与 xy平面上 図形
.次 条件 xy平面上 点P全体 集合 図示
.
「C 平行移動 図形 ,点P 通 , 図形C
共有点 1点 , 3個存在
.」
✒
✑
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
)
関係 図示
.
問題文
明示
,以下 知識 利用
.
(a)
y
=
f
(
x
)
x
方向
a
,
y
方向
b
平行移動
y
−
b
=
f
(
x
−
a
)
.
(b) 3
次方程式
3
個 解 持 .
a, b
持
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];
条件
eqn
a
3
次方程式 見
(
b
a
従属
).題意
図形
3
個存在
,
3
次方程式
3
個 解 持
.
X, Y
持
a
方程式
f
(
a
) = 0
異
解 持
条件 ,次
記述
(実行 不要).
Reduce[Exists[{a1, a2},
And[f[a1] == 0, f[a2] == 0, a1 != a2]], {X, Y}]
The 28th Annual Conference of the Japanese Society for Artificial Intelligence, 2014
応用
方針
4
以降 実行
.
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];
RegionPlot[region, {X, -1, 1}, {Y, -1, 1},
PlotPoints -> 50, MaxRecursion -> 8] (*出力 図1(a).*)
1988
年 東京大学 理系 第
4
問
✓
✏
xy平面上 原点 傾 a(a >0) 出発 折 線状 動
点P 考 . ,点P y座標 増加 , 値
整数 動 方向 傾 s倍(s >0) 変化
.
P 描 折 線 直線x=b(b >0) 横切 a, b, s
関 条件 求 .
✒
✑
1.
y
=
n
対応
x
求
.
2.
x
b
大
n
存在
,
限定子 使
記述
.
3.
Reduce[]
使
限定子 消去 ,
a
,
b
,
s
関
条
件 求
.
問題文
明示
,以下 知識 利用
.
(a)
y
値 整数 点
調
十分
.
(b)
∑
n i=1x
i−1
x
̸
= 1
(
x
n−
1)
/
(
x
−
1)
,
x
= 1
n
(単純
Sum[x^(i - 1), {i, 1, n}]
,
x
= 1
場合 考慮
).
問題 解
以下 示 .
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)) *)
1988
年 東京大学 理系 第
5
問
✓
✏
xyz空間 ,xz平面上 0≤z≤2−x2 表 図
形 z軸 回転 得 不透明 立体 V
.V 表面上z座標1 点光源P .
xy平面上 原点 中心 円C ,P 光 当
部分 長 2π ,C 部分 長 求
.
✒
✑
1.
点
P
座標
(1
,
0
,
1)
.
2.
点
P
通
V
接平面 求
.
3.
接平面
xy
平面 交線
x
=
X
求
.
4.
光 当
部分 弧 対応
中心角
t
,方程
式
2
rt
= 2
π, r
cos
t
=
X
立
.
5.
Solve[]
使
方程式 解 ,
r
求
.
6.
求
長 ,
2
πr
−
2
π
計算
.
問題文
明示
,以下 知識 利用
.
(a)
対称性
,点
P
座標
(1
,
0
,
1)
.
(b)
,点
P
V
接平面 対
,
V
同 側
領域
.
(c)
接平面
a
(
x
−
1) +
by
+ (
z
−
1) = 0
形 記述
.
問題 解
以下 示 .
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 *)
1988
年 東京大学 理系 第
6
問
✓
✏
空間内 点O 対 ,4点A,B,C,D
OA = 1,OB = OC = OD = 4
,四面体ABCD 体積 最大値 求
.
✒
✑
1. A
,
B
,
C
,
D
座標
表示
.
2.
四面体
ABCD
体積 求
.
3.
MaxValue[]
使
体積 最大値 求
.
問題文
明示
,以下 知識 利用
.
(a) A
(0
,
0
,
1)
.
(b) A
(0
,
0
,
1)
,四面体
ABCD
体積 最大
,
BCD
含 平面
xy
平面 平行
.
(c) 3
次元
a
,
b
,
c
,
d
作
四面体 体積 ,
Cross[b - a, c - a].(d - a)/6
.
問題 解
以下 示 .
a = {0, 0, 1};
b = {4 Cos[t], 0, -4 Sin[t]};
c = {4 Cos[t] Cos[u], 4 Cos[t] Sin[u], -4 Sin[t]}; d = {4 Cos[t] Cos[v], 4 Cos[t] Sin[v], -4 Sin[t]}; f = Simplify[Cross[b - a, c - a].(d - a)/6]
体積
f
,次
t
関数
u
v
関数 積
.
f
=
32
3
(4 sin
t
+ 1) cos
2t
sin
(
u
2
)
sin
(
v
2
)
sin
(
u
−
v
2
)
.
,
f
最大値 次
求
.
part1 = 32 Cos[t]^2 (1 + 4 Sin[t]); part2 = f/part1;
With[{
p1min = MinValue[{part1, 0 <= t < Pi}, {t}], p1max = MaxValue[{part1, 0 <= t < Pi}, {t}], p2min = MinValue[{part2,
And[0 <= u < 2 Pi, 0 <= v < 2 Pi]}, {u, v}], p2max = MaxValue[{part2,
And[0 <= u < 2 Pi, 0 <= v < 2 Pi]}, {u, v}]}, If[And[p1max > 0, p2max > 0],
If[And[p1min < 0, p2min < 0], Max[p1max p2max, p1min p2min], p1max p2max]]] (* 出力:9 Sqrt[3] *)
3.
結果
全
6
問 解答 結論(第
3
問 結論 図
1(a)
,他 問題
結論
中 記載) ,
[
大数
93]
掲載
一致
.
計算時間 利用記憶容量 表
1
通
.
The 28th Annual Conference of the Japanese Society for Artificial Intelligence, 2014
-1.0 -0.5 0.0 0.5 1.0 -1.0
-0.5 0.0 0.5 1.0
(a)本手法 結果
I-35 72 125M
I3 5
-72 125M
-1.0 -0.5 0.5 1.0x
-1.0
-0.5 0.5 1.0 y
y=x3-x
y=1
9Hx 3
-9xL
y=1
4Hx 3-3x2-x+3-xL
y=1
4Hx 3+3x2-x-3L
(b)模範解答
図
1:
第
3
問 解答
表
1:
計算時間 利用記憶容量
問題
計算時間(秒)
利用記憶領域(
MB
)
第
1
問
4
.
6
10
第
2
問
3
.
3
×
10
335
第
3
問
1
.
5
×
10
271
第
4
問
3
.
2
×
10
18
第
5
問
6
.
8
×
10
21
第
6
問
7
.
0
×
10
17
4.
考察
大学入試 数学 問題 数式処理
使
解
,問題文
数式処理
用 言語 置 換
,問題
理解 基
対称性
発見 ,計算量 減
工夫 必要
.
数学 学習 数式処理
導入
場合
,手 解 場合 ,数式処理
利用
解 場合
,解 方 大
異
注意
.数
式処理
利用
学習
身
能力 ,数学
学習
身
期待
能力 違
明
研究 必要
.
結論(真偽値 数値,図形) 模範解答
一致
,
得
結果 数学的 正
,大学入試
正解 見
.
,
Mathematica
7
Reduce[]
,
350
Mathematica
1400
C
使
[Wolfram 11]
,試験 採点者
検証
現
実的
.
4.1
各論
4.1.1
第
1
問
後半 問
対
,点
P
自体
(
x, y
)
解
,点
P
像
(
x, y
)
命題 記述
.
変数 導入方法
,試行錯誤 必要
.
4.1.2
第
2
問
知識
(e)
受験数学 学
思
,
MaxValue[]
MinValue[]
利用
,
,
数式 表現
知識 有用
.
知識
(f)
用
,面積 三角関数 記述
,
MaxValue[]
MinValue[]
最大値 最小値 求
.三角関数 含 式 関
問題
,
変数変換 有力
.
難問
有名 本問
,数式処理
利用
,比較的簡単 解
.
解法 ,文献
[
小島
89]
掲載
,人間 手 解 方法
大
異
.
4.1.3
第
3
問
a
3
次方程式
初
知識
(b)
利用
.
,具体的 方針 事前 決
難
場合
.
本手法
第
3
問 結論 図
1(a)
,模範解答 図
1(b)
,曲線 式 交点 座標,曲線自体 点自体
含
描
.
4.1.4
第
4
問
Mathematica
,
∑
ni=1
x
i−1