社会人大学院生になって2年経過した
私は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本を国際学会に出して、査読してもらっているところです。査読してもらっている間に次の論文を書き始めています。
