• 検索結果がありません。

PDFファイル 3D3 「教育支援におけるモデリング」

N/A
N/A
Protected

Academic year: 2018

シェア "PDFファイル 3D3 「教育支援におけるモデリング」"

Copied!
4
0
0

読み込み中.... (全文を見る)

全文

(1)

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象限 内部

示 .

(2)

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}]

(3)

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=1

x

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

2

t

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

(4)

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

3

35

3

1

.

5

×

10

2

71

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

n

i=1

x

i1

簡単 計算 ,特

殊 仮定(

場合

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

問 同様,具体的 方針 事前 決

5.

大学入試 数学 問題 ,数式処理

現実的

確認

解法 手 解 場合

,問題

理解 基

知識 必要

事例 積 重

,数学教育 改

,人工知能研究 進展

期待

参考文献

[Wolfram 11] Wolfram Research, I.: Some Notes on

Inter-nal Implementation (2011)

[

穴井

11]

穴井 宏和

,

横山 和弘:

QE

計算

応用

,

東京大学出版会

(2011)

[

小島

89]

小島 寛之:

花束

,

大学

数学

,

Vol. 33, No. 11–12, pp. 56–57 (1989)

[

松崎

13]

松崎 拓也

,

岩根 秀直

,

穴井 宏和

,

相澤 彰子

,

新井 紀

子:深 言語理解 数式処理 接合

入試数学問題解

,

人工知能学会全国大会論文集

(CD-ROM), pp.

2A4–1 (2013)

[

聖文新社

08]

聖文新社 編集部(編):東京大学 数学入試問題

50

,

聖文新社

(2008)

[

大数

93]

大学

数学 編集部(編):東大入試・

10

年 軌跡

,

東京出版

(1993)

参照

関連したドキュメント

Methods suggested in this paper, due to specificity of problems solved, are less restric- tive than other methods for solving general convex quadratic programming problems, such

T. In this paper we consider one-dimensional two-phase Stefan problems for a class of parabolic equations with nonlinear heat source terms and with nonlinear flux conditions on the

In particular, we show that, when such a polynomial exists, it is unique and it is the sum of certain Chebyshev polynomials of the first kind in any faithful irreducible character of

In order to demonstrate that the CAB algorithm provides a better performance, it has been compared to other optimization approaches such as metaheuristic algorithms Section 4.2

It turned out that the propositional part of our D- translation uses the same construction as de Paiva’s dialectica category GC and we show how our D-translation extends GC to

The main problems which are solved in this paper are: how to systematically enumerate combinatorial braid foliations of a disc; how to verify whether a com- binatorial foliation can

In this section we apply approximate solutions to obtain existence results for weak solutions of the initial-boundary value problem for Navier-Stokes- type

In order to solve this problem we in- troduce generalized uniformly continuous solution operators and use them to obtain the unique solution on a certain Colombeau space1. In