東ロボの論文時系列まとめ

[数学,東ロボ,論文読みメモ]

東ロボの論文時系列まとめ

東ロボの論文時系列まとめについてメモ ... メモ書き

• 2013年
  • 数式処理による入試数学問題の解法と言語処理との接合における課題
  • 深い言語理解と数式処理の接合による入試数学問題解答システム

• 2014年
  • 「東ロボくん, 代ゼミ模試に挑戦!」数学チームの結果について (数式処理とその周辺分野の研究)
  • 大学入試過去問による数学問題解答システムの評価と課題分析
  • Formula Simplification for Real Quantifier Elimination (Developments in Computer Algebra Research) ← 関連研究

• 2015年
  • 数式処理による入試問題への挑戦〜ロボットは東大に入れるか〜

• 2016年
  • 題材となるオブジェクトの抽象化による確率文章題の自動解答

• 2017年
  • センター試験「数学」整数問題解答システムの開発
  • Language Processing of Mathematical Problem Text
  • 数学問題の自然言語解析 上の論文の日本語版か
  • 大学入試における数列の問題を解くための自動推論とその実装について (数学ソフトウェアとその効果的教育利用に関する研究)

• 2018年
  • センター試験「数学」整数問題解答システムにおける探索空間の削減

  ざっくり読んでみた感じ

2013年

• 深い言語理解と数式処理の接合による入試数学問題解答システム
  • 課題の策定:「機械によって数学の問題を解く」とは何かを解明し、次にそれをインスタンス化する記号システムについて説明
  • システムでは、問題のテキストは、答えを見つけるように命令する指令、つまり、特定の形式であり、問題で与えられた条件を満たすZF集合論の項に変換されます
  • 次に、指令はソルバーの言語の式に変換され、推論を通じて答えを見つけます

• 数式処理による入試数学問題の解法と言語処理との接合における課題
  • 問題を解くアプローチは, 問題文を公理的集合論の式に変換して数式処理手法により問題を解く
  • 計算処理には数式処理アルゴリズムである実閉体 (RCF) 上の限量記号消去法 (quantifier elimination: QE)というものを使う、汎用性が高いらしい
  • 課題
  • -> (1) 二次試験はこの方式でいけるが、センター試験に対して高得点をとるという観点ではこの手法のみでは不十分
  • -> (2) 一般に整数に関する問題や三角関数・指数関数・対数関数の問題に対して適用できる QE アルゴリズムは存在しない

• 論文をよく見るとQEの改善版のアルゴリズムを実装してる論文が脚注に入っている
  • An effective implementation of symbolic–numeric cylindrical algebraic decomposition for quantifier elimination

• それぞれの論文の主題とするところ
  • 深い言語理解と数式処理の接合による入試数学問題解答システムが全体の理論で、問題文から作り上げた式を解く部分が数式処理による入試数学問題の解法と言語処理との接合における課題に見える。
  • (2)の課題は拡張RCFを利用して解決しているように見える（RCFは使う対象を増やしたり限定できたりするのかな？）

2014年

• 「東ロボくん, 代ゼミ模試に挑戦!」数学チームの結果について (数式処理とその周辺分野の研究)
  • この資料は一般向けにわかりやすく書かれている気がする
  • QEは限量記号がついた一階述語論理式を入力として，それと等価で限量記号のない論理式を出力するアルゴリズムである
    • 問題文 → 一階述語論理式→ ATPによりQEを実行
  • 理論の実践として代ゼミ模試を解かせている、QEは計算量が多いらしく独自のアルゴリズムを組み込んでいる
  • 結果的には完答多めだが計算量が爆発して解けてないものもある

• 大学入試過去問による数学問題解答システムの評価と課題分析
  • 解答システムの中間言語としての ZF 集合論は、その柔軟性の一方、自動推論のための表現体系としては全く現実的でない、という明らかな欠点をもつ。このため、自然言語からの翻訳結果を実用的な推論技術へと接続するためには、さらにもう一段階の処理が必要…
    • ここに関してはこの論文では解決せず、中間表現出力のためのプロトタイプを開発しているの記述にとどまる
    • ここは解答作成後の出力を気にしているのだろうか？別にいいじゃんという感はある

• 処理フロー

• 数学理論（theory）の分類
  • 問題分を解析してQEで解けるかどうか分類している
  • 実閉体の理論 (RCF) 、ペアノ算術 (PA) 、ZF 集合論
  • "表で「ZF 集合論」に分類した、残りの 40%の問題は、それらを直接表現でき、しかも現実的に自動演繹が可能な理論が見当たらないという意味でより問題となる問題である。"
  • → 40%が解答不能となると、東大入試ではセンター試験で足切りされそう、後の研究で解けない40%を埋める方式がまとめられている

• Formula Simplification for Real Quantifier Elimination (Developments in Computer Algebra Research) ← 関連研究
  • 限量された一階述語論理式を等価で扱いやすい問題に帰着させる手法について
  • QEで解くには問題文を扱いやすい問題に帰着させないといけない→こうやった、という論文
    • 偶論理式に対する一階述語論理式の簡単化

2015年

• 数式処理による入試問題への挑戦〜ロボットは東大に入れるか〜
  • 東ロボに関する富士通の報告(FJの研究所はソルバー後半の計算処理に携わっていたとのこと)。たぶん一番わかりやすい。

2016年

• 題材となるオブジェクトの抽象化による確率文章題の自動解答
  • 大学入試過去問による数学問題解答システムの評価と課題分析にて "このうち、現在の我々の意味表示の体系では直接翻訳できない確率および組み合わせ論の問題を除いた..." とあるので、確率問題に関しては分類後に独自で解こうとする試みと思われる

2017年

• センター試験「数学」整数問題解答システムの開発
  • センター試験「数学」整数問題解答システムの演繹部を開発
  • 穴埋め問題を論理式に翻訳すると空欄部分のみを自由変数とする論理式になる。解けるものと解けないものがあった。

• Language Processing of Mathematical Problem Text
• 数学問題の自然言語解析 上の論文の日本語版か
  • 人工知能研究に関するいくつかの論点

• 大学入試における数列の問題を解くための自動推論とその実装について (数学ソフトウェアとその効果的教育利用に関する研究)
  • 確率問題と同じく、数列もRCFで解けないので分類後に独自で解こうとする試み
  • そう考えると数学Aの問題はRCF的ではないのか

2018年

• センター試験「数学」整数問題解答システムにおける探索空間の削減
  • 大学入試過去問による数学問題解答システムの評価と課題分析にて "「RCF+PA」に分類された 15 題は、自然数（ないし整数・有理数）と実数をともに含むような問題である。これらの内ほとんどは、「…である実数 x は有理数（あるいは無理数）であることを示せ」というタイプの証明問題か、自然数と実数をともに含む命題を帰納法で示すタイプの問題であった。"
  • これもRCFで解けないので分類後に独自で解こうとする試みと思われる
  • 式の正規化と拡張されたマッチング規則を用いた式変形探索手続きで解くことができるようになった