船井情報科学振興財団

留学報告書

Long Thanh PHAM
Carnegie Mellon UniversityDecember 20, 2021

2019 年 9 月より Carnegie Mellon University (CMU) で Computer Science の博士課程に取り組んでいるファムです。今回の報告書では 2021 年後半を振り返ります。

1

インターンシップ

6 月上旬から 8 月下旬までアマゾンのクラウド部門である Amazon Web Services(AWS) で研究インターンシップに取り組みました。上司がボストン勤務であるため、私の正式な勤務地もボストンですが、研究チームのメンバーは全米各地に散らばっています。
インターンシップ形式として、私はハイブリッドを選択しました。一週間の内、数日間だけオフィスで働き、残りは在宅勤務という形式です。しかし、私の上司はずっと在宅勤務であり、オフィスに来ても知り合いに会える訳ではないので、私もずっと在宅勤務でした。そのため、アマゾンのボストンオフィスを訪れたのは 5 回ほどだけです。また、研究チームのボストン在住メンバーが夕食を一緒にする機会があり、上司に対面で会ったのはその日が最初で最後でした。このように、ボストンに来てもAWS のメンバーになかなか会えませんでしたが、ボストンに来たからこそ出会えた人達も少なくありません。

1.1 ボストンでの交友関係
ボストンでは、民間会社が経営する学生向けの寮に住んでおり、キッチンや食堂、シャワー室は共有でした。そのため、同じ寮の住民たちと顔を合わせ、会話する機会が（特に食堂で）多いです。その結果、3 か月という短い期間ではありましたが、学生時代の友人関係ような深い繋がりを築けました。ボストンでの写真を Figure 1に添付します。
インターンシップでは、AWS 社員だけでなく、博士課程に所属している他の研究インターン生たちとも（オンラインではあるが）交流を深めました。とりわけ親しいインターン生とは週に一度の頻度でオンライン雑談をしていました。将来、同じ職場の同僚になるかもしれない友人たちとの繋がりは一生の財産になると信じています。

1

(a) ボストンでの寮の友人たちとラザニアを一緒に (b) ボストンの街並み。アメリカの中で、ボストン食べた際。
は西欧風の街並で有名である。奥に映っている高層ビルがボストンで一番高い John Hancock Tower。

Figure 1: ボストンでの写真

1.2 研究
私の取り組んだ研究プロジェクトは CBMC という C 言語のための bounded modelchecker に関するものです。Model checker は端的に言うと、プログラムを解析するためのプログラムです。まず最初に、与えられたプログラムを抽象化したモデルを作成し、そのモデルが特定の安全性の条件（例：セキュリティに関する条件）を満たすかどうかをチェックするのが model checker です。もし、モデルが安全性の条件を満たすのであれば、もともとのプログラムも安全であると判明します（その逆は常に成り立つとは限らないが）。
今回のインターンシップの前半は、CBMC に loop variants という機能を加えるため、C++ というプログラミング言語でひたすらコードを書きました。この作業に研究的な要素はほとんどありませんが、CBMC の仕組みを詳しく学べた上、複雑なソースコードの全体像を素早く把握する能力は鍛えられました。
後半では、loop variants を自動的に推論できるかどうかを研究し、自動推論エンジンのプロトタイプを CBMC 上に実装しました。全ての loop variants を自動的に推論するのは数学的に不可能ですが、現実的なプログラムの loop variants にはパターンがあるので、例え一部の loop variants しか推論できなくても、ベンチマークで高評価を得ることが可能です。最初の一歩として、abstract interpretation という比較的古典的な技術を使った推論エンジンを実装し、その次のステップとして、線型計画法（linearprogramming）を使った推論アルゴリズムを研究する予定でした。後者の研究トピッ
クは大学での研究にも関連しているので楽しみでしたが、インターンシップの最後の2 週間はプレゼンテーションの準備に追われたため、結局研究できませんでした。
インターンシップの最後には、AWS からいい評価をいただき、来年のインターンシップのオファーも貰いました。教授と相談した結果、来年の夏は大学での研究に集中すると決めたので残念ながら AWS には戻りませんが、このインターンシップを通じて出会った人たちとの繋がりは大切にしたいです。
2

1.3 学び・感想
1.（当たり前だと思われるが）AWS での開発・研究は大学での研究と比較して、エンジニアリングの要素が大きく、サイエンスの要素が小さい。企業での研究は、今自分が面している実世界の問題を解決できるアイデアを文献から見つけ出し、それを実用化することに重きが置かれている。勿論、解決策が見つからない場合はゼロから研究し、面白いアイデアが出た場合は論文として提出するが、ゼロからの研究はあまり多くないように感じる。対照的に、大学での研究が扱う問題はより抽象的（悪い言い方をすれば、50％現実的、25％簡略化、残りの 25％架空）であり、今までにないアイデアや視点を生み出すことに重きが置かれている。
2. 産業界でのプログラミング言語理論の応用研究・開発において、かつてはインテルやマイクロソフト（特に Microsoft Research Institute）が大きな研究部門を有していた。しかし、最近は AWS が積極的に投資しており、この分野で一番大きな研究部門を持っているようである。
3. 短期的な視点で見ると、今回のインターンシップは大学での研究に役立たなかった。大学での研究に役立つ研究インターンシップをしたい、もしくは、インターンシップの研究成果を論文に仕上げたい場合、最初から自分で適切なプロジェクトを見つけ、それに AWS に提案する必要があるだろう。ただし、その場合、自分の目先の利益は得られるが、AWS に本当に役立つプロジェクトかどうかは不明である。上で説明したように、企業での研究・開発と大学での研究は性質が異なるからである。現在の大学での研究に関連しないにせよ、今回のように、AWS のビジネスに関連するプロジェクトから学べたことは多々あり、長期的に見て将来の研究に役立つかもしれないので、後悔はしていない。
4. AWS の待遇はいい。しかし、ボストンの物価は高い（笑）。

2

研究

前回のレポートでもお話ししたように、type-based resource analysis を mechanism
design に応用する研究をしており、その最初の一歩として、session types で表現された並行プログラムの worst-case input generation を 6 月末まで研究していました。7月上旬にある POPL 2022 の論文締め切りに間に合わせようと頑張りましたが、研究インターンシップが 6 月上旬に始まったため、締め切りには間に合いませんでした。
加えて、いざ論文を書き始めた際、理論的な結果は揃っていましたが、その重要さを力説できるだけのケーススタディーを上手くデザインできなかったので、理論的結果をさらに拡張することに決めました。
9 月にボストンからピッツバーグに戻った後、論文の仕上げに取り組みました。理論的結果の拡張と論文の執筆を同時に行ったので大変でしたが、11 月中旬には終わらせ、PLDI 2022 に提出しました。あとは無事採択されることを祈るのみです。
本来の目標であった、mechanism design に type-based resource analysis を応用する研究において、個人的に面白いと思う結果を得られましたが、指導教授はあまり満足しなかったので、一歩下がって、別の研究方向を探ることにしました。2021 年 9月に type-based resource analysis を少し拡張することで、オークションの一種である3

first-price/second-price auctions の incentive compatibility を自動的に証明できることが判明しましたが、これを指導教授を含め数人の教授にプレゼンしたところ微妙な反応が戻りました。原因は二つあり、(i)first-price/second-price auctions が非常に単純で、説得力に欠ける具体例である、(ii) 加えて、他のより伝統的な手法と比較して実用的なメリットはないです。
そのため、11 月中旬に worst-case input generation の論文を書き終えた後は、今まで焦点に当てていたオークションをより一般化した smart contracts を対象にした研究テーマを探しています。Smart contracts とは実生活の契約・取引を体現し、自動的に作動するプログラムのことです。主にブロックチェーン上に実装されますが、必ずしもブロックチェーンに限ったプログラムではありません。この場合の契約・取引の具体例として、仮想通過の送金、証券取引所での金融取引、オークション、選挙などが挙げられます。これら smart contracts のゲーム理論的な公平さを証明するためにプログラミング言語理論のアイデアの応用するというのが今の目標であり、現在、具体的な研究テーマを探していています。

3生活

3.1 歓迎会・送別会
2021 年 8 月に 2021 年度船井奨学生である荒川陸さんが CMU に到着し、博士課程を始めました。これで CMU の船井財団メンバーは 4 人になり、賑やかになりそうと思っていた矢先、2021 年 9 月には 2017 年度奨学生の林さんが博士課程を卒業しました。
荒川さんと林さんの歓迎会兼送別会を開き、CMU の船井財団メンバー全員で夕食を一緒にしました。Figure 2に写真を添付します。

(a) CMU の School of Computer Science での記念撮影。左から荒川さん、林さん、大谷さん、私。

(b) バーでの夕食。

Figure 2: CMU の船井財団メンバーとの歓迎会・送別会

43.2 日本への一時帰国
過去 2 年半、日本に戻っていませんでしたが、今年の冬に一時帰国することに決め、11 月 25 日（ちょうどアメリカでは感謝際の日）に日本に出発しました。シカゴでの乗り継ぎでしたが、シカゴから羽田の便は空席がほとんどでした。パンデミックの影
響で日米間の便が少ないせいか、アメリカでの乗り継ぎの待ち時間は異常に短いか異常に長いかの二択でした。私の場合、乗り継ぎ時間が異常に短い（シカゴで 51 分）フ
ライトを予約したため、シカゴで次の便に乗り遅れないかヒヤヒヤしていましたが、問題はありませんでした。しかし、ユナイテッド航空との賭けに負けた場合の損害が大きいので真似はしないください。乗り継ぎには十分時間に余裕を持たせましょう（笑）。
東京では 10 日間の自主隔離をし、その後、両親が住んでいる沖縄に向かいました。
アメリカには 1 月 6 日に戻る予定です。

3.3

CMU での博士課程選考委員会

現在 CMU での博士課程選考委員会に加わっています。12 月中旬に最初の会議があり、日本時間で真夜中の 0 時での参加になりました。日本とアメリカを跨って働くのに、14 時間という時差は厳しすぎると感じました。地球がなぜ球体なのかと恨んでいます（笑）
。選考委員会には教授だけでなく、現役の博士課程学生も参加します。博士
課程選考を内側から知るいい機会ですし、将来、ポスドクや助教のポジションの応募にも生かせる教訓が詰まっているはずなので、楽しみです（といっても選考委員会の仕事量は半端ないが）。

5