松崎拓也, 岩根秀直, 穴井宏和, 相澤彰子, 新井紀子諸氏による論文『深い言語理解と数式処理の接合による入試数学問題解答システム』

松崎拓也, 岩根秀直, 穴井宏和, 相澤彰子, 新井紀子の諸氏による『深い言語理解と数式処理の接合による入試数学問題解答システム』 という論文が出たとのこと. 冒頭部を引用してみよう.

あらゆる数学のオブジェクトは Zermelo-Fraenkel の公理的集合論 (ZF) の (保存拡大の) 項だと考えることだできるので, ここでいう「計算」とは ZF の項の書き換えだと見做せよう. では, その計算をどこえめるべきか. 即ち, 問題文の直訳である項を, それと同等であるような無数の項のうちから, どのようなものに書き換えれば問題が「解けた」ことになるのだろうか. それを考えるヒントは, 解答群の中に見いだすことができる. 大学入試を例にとると, 証明問題以外では, 解答に現れるのは, \(y = 2ax - a2,(x < 0 \to a = 3) \wedge (x ≥ 0 \to a = 5)\), \(a_1 + · · · + a_n > 0\) のような限量記号をひとつも含まないような式である. しかも, その式は, 実閉体の理論に三角関数や指数関数などの超越関数をシンボリックにしか利用しないような拡張を行った実閉体の体系 (拡張 RCF) に弱いペアノ算術の体系を加えた体系 (\(\mathrm{RCF}^{+ }+\mathrm{PA}\)) で表現されるようなものにほぼ限られる. また, 模範解答に現れる式も, 実は \(\mathrm{RCF}^{+ }+\mathrm{PA}\) で記述可能な式が圧倒的に多いことに気づく. となれば, 問題文を同等の \(\mathrm{RCF}^{+ }+\mathrm{PA}\) の式に変換し, その式から限量記号を消去することが, 大学入試の数学問題を「解く」ことだと考えてもよいだろう.

この先の細かい部分はほぼ何を言っているのか分からないが, 試み自体がとても面白い. こんなこともやっている人がいるのか. 楽しい.