船井情報科学振興財団

留学報告書

Long Thanh PHAM
Carnegie Mellon University
June 26, 2021

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

1研究

２０２１年前半は去年から引き続き type-based resource analysis を mechanism designに応用する研究をしています。Type-based resource analysis というのは、型システムを利用して、プログラムの資源量を解析する分野です。また、mechanism design は、オークションなど mechanisms のデザインを、ゲーム理論の視点から研究する分野です。Mechanisms というのは、複数の参加者が各自の利益を第一に追求しそれぞれ意思決定するゲーム・システムのことであり、例として、オークションや選挙があげられます。オークションでは、参加者全員、勝つという目標がありますが、入札価格は皆違います。その中でたった一人の落札者・買い手を（公正に）決めるにはどうしたらいいのか、また、勝った場合、落札価格はいくらに設定すべきなのかといった質問
を mechanism design は扱っています。同様に選挙でも、有権者全員それぞれ希望の候補者がいますが、実際に当選できるのは候補者の一部だけです。この場合、どうやって当選者を決めるか（i.e. 多数決がいいのか、それともポイント制度にすべきなのか）という質問も mechanism design で扱われます。
私の研究では最初に、worst-case input generation algorithm をデザインしました。
Type-based resource analysis では、プログラムの資源量がインプットサイズの関数として算出されます。この情報を基に、一番資源を多く要するインプットを算出するというのが、worst-case input generation の目標です。この worst-case input generation
algorithm のデザインを終えた後、オークションの解析に応用できるか研究しました。
現在、論文執筆中です。

2インターンシップ

６月上旬から８月下旬まで、アマゾンのクラウドコンピューティング部門である
Amazon Web Services (AWS) で研究インターンシップをしています。AWS の中でもAutomated Reasoning Group (ARG) という、プログラム解析や SAT・SMT を扱っている研究部門に所属しています。担当上司がボストン勤務であるため、私のオフィス

1

もボストンです。しかし、ARG のメンバーは（パンデミック以前から）全米に散らばっています。私の周囲はニューヨーク勤務のメンバー多いようですが、私の上司はボストン勤務ですし、そのさらに上の上司はミネアポリス勤務です。
インターンシップの形式に関して、インターン生にはフル在宅勤務とハイブリッド勤務という二つの選択肢が与えられます。ハイブリッド形式は在宅勤務とオフィス勤務の両方を組み合わせたもので、一週間の内、２・３日間はオフィスで仕事をし、それ以外の日は在宅勤務になります。インターン生は各自好みの形式をインターンシップの数か月前に選びます。ただし、ハイブリッド形式を選んでも、ずっと在宅勤務することは可能ですし、逆にフル在宅勤務を選択しても、後にハイブリッドに変更することも可能です。私はハイブリッド形式を以下の理由で選択しました。
1. 過去２年間、ピッツバーグの同じアパートでずっと一人暮らしをしてきたので、新しい街であるボストンに移ることで、気分転換をし、効率向上をしたかった。
2. 在宅勤務だと仕事と私生活の境界線が曖昧になるので、時折オフィスに来ることで、メリハリをつけたかった。
面白いことに、ボストンには引っ越ししましたが、今のところずっと在宅勤務です。オフィスを訪れたのは社員証を受け取るための一回だけです。ピッツバーグからボストンに引っ越しするだけで、周囲の環境（e.g. 部屋、街、ボストンでの新しい交友関係など）ががらりと変わりました。その結果、ボストンでの在宅勤務はピッツバー
グでの在宅勤務は異なり新鮮であり、わざわざオフィスに通勤して新鮮さを求める必要がありませんでした。今のところ、ボストンでの在宅勤務に満足していますが、一部のインターン生はオフィスに来ているようなので、私も時折オフィスに顔を出すことで、人間関係を広げられたらいいなと考えています。
このインターンシップでは、CBMC という C 言語のための model checker に loop
variants/ranking functions という機能を加えるのが目標です。１２週間のインターン
シップの前半は、プログラマーが書いた loop variants を解析する機能を私が実装し、後半は適切な loop variants を自動的に導き出す機能を研究する予定です。この loop
variants を自動的に導き出す機能には、CMU での研究を生かせると思うので、楽しみです。
インターンシップの最初の２週間は、仕事に加え、アマゾンをもっとよく知ってもらうためのオンライン研修がありました。時間はかかりましたが、アマゾンの企業文化を知ることができ、有意義でした。特に印象的なのは、leadership principles と呼ばれる１４カ条のアマゾンの社訓であす。ちなみに、第一カ条は「顧客の利益が第一優先」です。アマゾン創成期の企業文化・哲学を、後に入社した社員にも受け継いでもらうために、社訓という形で明文化し、その教育を徹底している点に感心しました。

3生活

CMU が手配してくれたワクチンの一回目の接種を４月中旬にし、４週間後の５月中旬に２回目の接種をしました。5 月下旬以降、ボストンでは交通機関（e.g. 電車やタクシー）以外であればマスクの着用義務がなくなりました。
ベトナムのパスポート更新のために、5 月中旬にニューヨークのベトナム領事館を訪れました。領事館は国連本部のすぐ隣でした。２年前に博士課程のために日本か2

らアメリカに向かう途中でニューヨークシティの JFK 国際空港で乗り継ぎをしましたが、ニューヨークシティの街並みを実際に目にするのは今回が初めてです。マンハッタンの高層ビル群の高さと密度には度肝を抜かれました。普段、ピッツバーグでは普通に前を向いているだけで目の前の建物全体が視界の中に入ります。対照的にマンハッタンではビルが高すぎるため、（ビルからある程度離れていても）頭を上に向けないとビル全体が視界に入りません。
CMU 所属の他の船井財団奨学生（i.e. 林さんと大谷さん）とは２月にオンライン雑談をしました。２０２０年９月の青木さん送別会以来です。５月中旬には、BBQ レストランでランチを一緒にしました。その際の写真を以下に添付しました。

(a) マンハッタンの様子。タイムズスクエア付近。 (b) BBQ レストランでの昼食。左から、林さん、私、大谷さん。撮影者：林さん。

５月下旬、インターンシップ開始の一週間前にボストンに移りました。ボストンでのアパートは自分で探す必要がありました。アマゾンからは家賃補助金（インターンシップ中に住む街によって微調整）が貰えますが、その使途は自由であり、使い切れなかった分は貯金に回します。ボストンでは Found Study Boston という学生向けのアパートに住んでいます。大学ではなく、ホテルなどを手掛ける民間会社が運営しています。家具（e.g. ベッドや冷蔵庫）はある程度揃っていますが、机のランプやベッドのシーツなどは各自用意する必要があります。

3