「ロボットは東大に入れるか」という企て：5．深い言語処理と高速な数式処理の接合による数学問題の自動解答

全文

(1)くわだ. 小特集「ロボットは東大に入れるか」という企て基応専般. ［数学］. 5 深い言語処理と高速な数式処理の接合による数学問題の自動解答. 松崎拓也（名古屋大学）岩根秀直（富士通研究所）. 大学入試数学を自動的に解く意義. 問題文意味辞書. 東ロボ数学ソルバーは，問題文を論理式へと翻訳したのち，数式処理によって解答を導く構成である1. ），2）. （図 -1）．本稿では，このような方針で数学問題の自動解答に挑戦する意義について，言語処理，自動演繹，および両者を結合した人工知能システムという. 3 つの観点からまとめる．文の意味の理解とは，それを真とする世界の在り方を過不足なく捉えることだ（真理条件意味論）とい. 8,316 表層形 54,932 エントリ. 言語処理. が実数全体を動くとき空間内の点がつくる直線をとする. 1, 2, 0 を通り, とする球面がと共有点の満たす条件を求めよ.. 3点中心ををもつとき. （北大2011 前期理系）. 高階論理による意味表示公理. 概念定義による書き換え. 1,372 述語・関数 2,320 公理. 実閉体の一階論理式限量子消去解答. 図 -1 東ロボ数学ソルバーの構成. うのは標準的な考え方の 1 つである．しかし，実用. はきわめて高度な知的処理である．. 的な言語処理のための原理としてこれを採用した例は. 東ロボ「数学」では一階の実閉体の言語で表現で. 少ない．次の簡単な例を考えよ：. きる問題を最初の標的とし，徐々に対象とする問題を. 「自分の 4 匹の子猫たちみんなに，どうして翼がはえ. 拡大してきた．実閉体の理論は幾何をはじめ広い応. ているのか，ジェーン・タビーお母さんにはさっぱりわ. 用範囲を持ち，かつ，限量子消去によって決定可能. ☆1. けが分かりませんでした」. である．この「自動演繹の成功が原理的には保証さ. 問．お母さんはこれまで何匹の子を生みましたか．. れている」という性質は，論理式による問題表現を. 答．少なくとも 4 匹．正確には不明．. 接合面として，システムが言語処理と自動演繹に完全. この問答は現代の技術水準では不可能である．一. に分割できることを保証する．これは実問題において. 方で，照応（「自分」），量化（「みんな」），埋め込み節. は稀な性質だが，言語理解と演繹との境界で一般的. の事実性（「... のか」）といった一連の現象を正しく解. に発生するさまざまな課題を整理し解決するための. 析し真理条件を把握することは実応用において必須. 理論的な下支えが存在することは人工知能研究の題. であり，世界知識（「初産かどうか不明」）が不問とな. 材として大きな意義がある．. る大学入試数学は，これらの技術の総合的な評価のために好適であることが分かる．自動演繹の研究では，人が形式化した問題を入力. 数学問題テキストの言語処理. とし，「どの公理系の問題か」も指定するのが通常で. 言語処理部は，語・文・談話の 3 レベルに渡る多. ある．しかし，同値な表現の間でも，細部の差異に. 段の処理からなる（図 -2）．主たる技術課題は，言語. よって演繹処理の効率は大きく異なるため，言語処. 現象に対する被覆率の拡大と，正確な曖昧性解消で. 理の結果から適切な問題表現を導くことは単なる「演. ある．詳細の解説は別の機会に譲る．. 繹の前処理」ではなく重要な研究課題である．また，問題表現に基づき演繹を行う枠組みを決定すること ☆1. A・K・ル = グウィン「空飛び猫」村上春樹訳（講談社）．. 高速な数式処理最適化ソルバーなどの数理ソフトは，適切に簡単化情報処理 Vol.58 No.7 July 2017. 607.

(2) くわだ. 小特集「ロボットは東大に入れるか」という企て. 言語処理字句処理. /NP のグラフ /S とする. のグラフ à とする à. 問題. 円 O の周の長さ à 円/NN O/NP の/PP 周/NN の/PP 長さ/NN. 数式解析. (. 品詞解析. 直線 ℓ が円 C と接している. との) 接点の座標を(1, 1) とする. の. 文処理. 対角線. である. ゼロ照応検出は. 構文解析. 数学I+A. 共参照解析文間関係解析. 意味表示. (. 直線 ℓ が円 C と接している.. と. の) 接点の座標を(1, 1) とする.. を自然数とする. = と仮定する. = は偶数である. このとき, à. 修正あり. 問題・分野. 配点. 完全自動. 修正あり 2. 10. 0. 10. [1]-1 三角関数. 15. 0. [1]-2 集合. 10. 6. 3. [1]-2 指数・対数. 15. 5. 5. [1]-3 2次関数. 10. 2. 6. [2] 微分・積分. 30. 15. 19. [2]-1 図形と計量. 15. 11. 15. [2]-2 データ分析. 15. 6. 6. [4] 整数の性質. 20. 10. 10. [5] 図形の性質. 20 合計. 8 43 点. 10 70 点. [3] 数列 [4] ベクトル. =. だが，言語処理により生成される論理式は非常に冗長で，従来の手法では解けないことが多かった．そのため，東ロボ数学ソルバーでは改良した限量子消去手法 3 に加え，論理関数処理，幾何的不変性など）. 4）. が用いられている．. 11 12 43 点. 13 20 59 点. ＊修正あり：不足の辞書エントリを追加し，言語処理における曖昧性解消を人手で行った場合. 問題・分野. 配点. [1] 図形と方程式. 20. [2] 確率. 20. [3] 微積分. 20. [4] 整数. された入力を期待することが多い．数式処理も同様. 20 20 合計. 図 -3 進研マーク模試 2016 の結果文系. 図 -2 言語処理部の構成. を利用した論理式の簡単化手法. 数学II+B 完全自動. [1]-1 数と式. 意味合成談話構造処理. 配点. 問題・分野. 20 合計偏差値. 理系完全自動 0 白紙. 修正あり 20 白紙. 0. 6. 20 20 点. 20 46 点. 50.1. 68.1. 配点. 問題・分野 [1] 整数. 20. [2] 確率. 20. 完全自動 20 白紙. [3] 図形と方程式 20. 20. [4] 立体の体積. 20. [5] 積分の極限. 20. 20 白紙. 20 合計. 20 80 点. [6] 複素平面. ＊修正あり：文系[1] à不足の辞書エントリを追加文系[2] à 共参照解析の結果を修正. 偏差値. 76.2. 図 -4 代ゼミ東大模試 2016 の結果. においては完全に自動的な処理で 4 問に完答し偏差値 76.2 を達成した．. 上記の改良により，旧帝大の 2 次試験問題を人手で形式化し，生成した入力に対し，既存の限量子消去ツールでは正答率約 88% に対して，現在開発中のツールでは約 95% が解けた．. 言語処理部の性能向上および演繹部が対応する問. そのほかに，適用範囲拡大のため，多項式の問題. 題タイプの拡大に加え，演繹を通じた曖昧性解消な. に変換可能な三角関数問題への拡張や代数曲線で囲. ど分野横断的な技術開発がさらに必要である．. まれた図形の面積を求める手法が用いられている．. 2016 模試の結果 2016 年度のセンター形式および東大形式模試に対する評価結果を図 -3，4 に示す．2015 年度までの模試による数学解答システムの評価では，言語処理部のうち未完成の部分を，人手で付与した言語処理結果で代替していた．この，人が介在する設定での評価結果は，意味辞書の被覆率および曖昧性解消処理について理想化した場合の性能の上限となる．. 2016 年度は，人が介在する設定（図の「修正あり」）に加え，システム全体を自動的に動かした場合（「完全自動」）の結果を評価した．両設定の下での得点にはまだ開きがある．また，センター形式模試に対する得点は，理想化した設定の下でも東大受験者レベルには達していない．一方で，東大形式模試（理系） 608. 今後の展望. 情報処理 Vol.58 No.7 July 2017. 参考文献 1） Matsuzaki, T., Iwane, H., Anai, H. and Arai, N. H. : The Most. Uncreative Examinee: A First Step toward Wide Coverage Natural Language Math Problem Solving, In Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, pp.1098-1104 (2014). 2） Matsuzaki, T., Ito, T., Iwane, H., Anai, H. and Arai, N. H. : Semantic Parsing of Pre-university Math Problems, In Proceedings of the 55th Annual Meeting of the Association for Computational Linguistics (ACL-2017), 2017. to appear. 3） Iwane, H., Matsuzaki, T., Arai, N. H. and Anai, H. : Automated Natural Language Geometry Math Problem Solving by Real Quantifier Elimination, In Proceedings of the 10th International Workshop on Automated Deduction (ADG2014), pp.75-84 (2014). 4） Iwane, H. and Anai, H.: Formula Simplification for Real Quantifier Elimination using Geometric Invariance, In Proceedings of the 42nd International Symposium on Symbolic and Algebraic Computation (ISSAC-2017), 2017. to appear. （2017 年 3 月 31 日受付） ■松崎拓也（正会員） [email protected] 専門は言語処理．東大助教，国立情報学研究所特任准教授を経て現在，名古屋大学准教授． ■岩根秀直 [email protected] 専門は数式処理．（株）富士通研究所人工知能研究所所属．博士（数理学）．.

(3)