私は2020年の10月に北陸先端科学技術大学院大学 (JAIST) 先端情報科学 博士前期課程の東京社会人コースに入学しました。緒方研究室に所属しています。形式検証が主な研究テーマです。入学前から長期履修制度というものを利用することを決めていたので、2023年の9月に修了予定です。私が所属している研究室では、社会人コースのほとんどの方が長期履修制度を利用していると思います。2年でやったことを書きます。

JAISTでは修了するために講義で多くの単位を取得する必要があります。私は以下の講義を履修しました。

  • Operating Systems
  • System Optimization
  • Discrete Signal Processing
  • Computer Networks
  • Mathematical Logic
  • Machine Learning
  • Advanced Computer Networks
  • Distance Learning System
  • Data Science
  • Systems Engineering for Machine Learning Applications
  • Foundation of Software Verification
  • Introduction to International Standardization
  • Introduction to Medical Service Science
  • Innovation Design for IoT Services
  • Innovation Theory and Methodology for Social Competencies
  • Innovation Theory and Methodology for Creativity

これらの講義はすべてオンラインで受講しました。結構がんばって勉強したつもりでしたが、満点だったのはMachine Learningのみでした。(Machine Learningは全然得意ではないので意外でした)

Mathematical Logicは講義の内容も進め方も面白かったです。講義の前に録画された動画を見ておいて、わからないところがあればあれば質問するという流れでした。最後はレポートを書いて、それに対して口頭試問を受けました。”Prove the compactness theorem for X.”や”Prove the completeness of Y.”みたいな感じの問題やなんらかのsolverをプログラムで書く問題などでした。個人的には予め動画を見てわからないことがあれば質問するスタイルが自分のペースで進められてしっくり来ました。

JAISTでは副テーマ研究というものがあります。副テーマ研究を説明した文章を見つけたので、以下に引用しています。

本学では専攻分野に関する主テーマ研究のほか、関連分野の知識等を修得し、幅広い視点から研究を行う能力を身に付けるため、副テーマ研究を実施しています。複数の研究テーマに取り組むことにより、多彩な課題に対する適応力や応用力を高めることができます。副テーマ研究では当該テーマに関する学外の専門家(他大学の教員など)に指導を受けることも可能です。

副テーマ研究の担当の先生によるかもしれないですが、研究対象は先生が用意したものでも自分で考えたものでもよいことが多いと思います。私は副テーマ研究の担当の先生が用意していた”機械学習システムの検証実験”というテーマを選択しました。副テーマ研究を担当してくださった青木先生が書いた以下の論文に書かれている手法を応用的なシステムに対して適用するといった内容でした。

T. Aoki, D. Kawakami, N. Chida and T. Tomita, “Dataset Fault Tree Analysis for Systematic Evaluation of Machine Learning Systems,” 2020 IEEE 25th Pacific Rim International Symposium on Dependable Computing (PRDC), 2020, pp. 100–109, doi: 10.1109/PRDC50213.2020.00021.

かなり雑にまとめると、機械学習を用いたシステムに対して故障木を使って分析しつつ、統計的な手法で評価しました。半年ほどかかりました。

主テーマ研究

主テーマ研究ではあるDistributed consensus protocolのモデル検査をしています。このテーマは入学前に指導教員とメールで「こういうのに関心があります。」と送って決めました。入試で研究計画について発表する必要があったので、このテーマで発表しました。実際に主テーマ研究を始めたのは、講義と副テーマの単位をほぼ取り終えた後です。最初の1年と数か月は主テーマ研究にほとんど着手していませんでした。

モデル検査では書換え論理に基づく計算機言語および処理系あるMaudeを利用しています。関数型プログラミング言語や論理型プログラミング言語みたいな感じ書けて、読み書きしやすいと思います。MaudeはLTLモデル検査器とsearchコマンドを提供しており、それらでモデル検査することができます。Maudeの仕様はPDFで600ページほどです。
http://maude.cs.illinois.edu/w/images/6/65/Maude-3.2.1-manual.pdf

モデル検査の規模が大きくなる場合はJAISTにあるLarge Memory PC Clusterというサーバーを利用させてもらっています。メモリが数TBあって便利です。
https://www.jaist.ac.jp/iscenter/mpc/lmpcc/

現在、論文1本を国際学会に出して、査読してもらっているところです。査読してもらっている間に次の論文を書き始めています。

--

--

私は2020年の10月に北陸先端科学技術大学院大学(Japan Advanced Institute of Science and Technology)先端情報科学 博士前期課程の東京社会人コースに入学しました。緒方研究室に所属しています。形式検証が主な研究テーマです。

修了するためには研究以外で20単位以上必要なので、この半年は講義の受講がメインでした。受講した講義は以下のとおりです。

  • システム最適化
  • オペレーティングシステム特論
  • データサイエンス論
  • 機械学習工学
  • 高機能コンピュータネットワーク
  • 遠隔教育システム工学
  • 人間力イノベーション論
  • 創出力イノベーション論

優が7つ、良が1つでした。良があったのはとても残念でした。自習と比べると、必死に勉強しようと自然と思える点、テストやレポートを通して理解度が明確になる点、先生から興味深い話を聞ける点が良かったです。未経験のことを短期間で習得しようとすることも楽しいです。

個人の将来的な目標は技術で未解決の問題を解決することです。人の役に立ち、かつ普遍的な知見となるようなことを目指したいです。博士前期課程では研究をとおして専門性を深めていくための準備をしたいと考えていたので、まだやりたいことはできていません。

いつ勉強していますか?

平日の朝と夜、休日です。

仕事と大学院を両立するのは大変ですか?

まだ、それほど大変だとは感じていません。自分の意志で自由に使える時間が多いことが関係していると思います。ただ、大学院で勉強や研究をしている状態と大学院に入学せず、何もしない状態を比較すれば、前者はやることが単純に増えているので、より大変だと言えるでしょう。また、どれだけ成果を出したいかは人それぞれですし、同様の事象に直面した際に大変だと捉えるかどうかも人それぞれです。

大学は文系学部だったのに、数学は大丈夫ですか?

今のところは大丈夫です。理解できていない箇所を明確にして、予め自習していたからです。ただ、ユーザーとして数学を使っているだけなので、数学自体を研究対象にするレベルのことはわかりません。

--

--

誰?

  • 大学では経済学を専攻していたが、大学院では情報科学の分野で研究をしたい人
  • 社会人
  • プログラミング歴は約5年

受験の流れ

オンラインでJapan Advanced Institute of Science and Technology(JAIST)の東京社会人コース説明会に参加した。

関心のある研究室に受け入れが可能かを問うメールを送った。COVID-19のため、対面でなく、メールでやり取りすることになった。教授が発表した論文や担当している講義の資料のリンクが送られてきた。講義の単位を取得できそうとかなどについて確認するため課題を出していただくことになった。講義の資料はi217 Functional Programmingという講義のものだった。

講義資料の指定された箇所を読み終わったという旨のメールを送った。1つ目の課題を出していただいた。

1つ目の課題が完了した。課題をメールで送付した。

2つ目の課題を出していただいた。

2つ目の課題が完了した。課題をメールで送付した。短期間で2つの課題を完成させることができたので、該当の講義に関しては単位を取得できるレベルであるという評価を受けた。大学院や研究について改めて説明を受けた。どのような研究をしたいかと問われた。

分散システムを形式検証したいという内容(実際には具体的な内容)のメールを送信した。そのメールに対する返信内容から自分のしたい研究を行うことができそうだとわかった。
出身大学に成績証明書と卒業証明書を発行する手続きをした。

研究計画書の書き方を問うメールを送り、アドバイスをいただいた。

研究計画書のドラフトを送付した。内容はよいという返信をいただいた。

研究に関係する論文を読んでまとめたり、情報科学や数学の基礎的な内容を改めて勉強したりし始めた。職歴調書、エントリーシート、研究計画書を作成した。

博士前期課程の社会人コース特別選抜に出願した。

口頭試問で使用する資料を作成し始めた。

受験票が届いた。

有給を取得して、口頭試問でのプレゼンテーションの練習をひたすら行った。

品川で口頭試問を受けた。会場に向かう最中にスマートフォンを無くして少し焦ったが、早めに出発していたので試験に間に合った。

合格通知が届いた。

  • COVID-19のため出願期間と入試の日程が一度延期になった。
  • 課題は関数型プログラミングと証明に関する内容だった。関数型プログラミング言語を用いて簡単な関数型プログラミング言語を実装した経験、数理論理学の基礎的な内容が書かれた本を読んだ経験、高校数学の知見などが役立ったと思う。
  • 私が学部で文系科目専攻だったことが関係するのか(?)、面接では情報科学や数学に関する基礎的な質問があった。こちらも趣味で色々やっていたことが役立ったと思う。

--

--