背景 機械学習を用いたシステムの信頼性・安全性を検証するためにはデータセットが必要となる。データセットの品質に偏りがあり、ノイズが入っているような低品質のデータセットに対する精度は低くなることがある。そのため、 高品質のデータセットと低品質のデータセットが混在している場合、機械学習を用いたシステムを一律に評価しても妥当性が不明瞭になるという問題がある。 …

私は2020年の10月に北陸先端科学技術大学院大学（Japan Advanced Institute of Science and Technology）先端情報科学 博士前期課程の東京社会人コースに入学しました。緒方研究室に所属しています。形式検証が主な研究テーマです。 修了するためには研究以外で20単位以上必要なので、この半年は講義の受講がメインでした。受講した講義は以下のとおりです。 システム最適化 オペレーティングシステム特論 データサイエンス論 機械学習工学 高機能コンピュータネットワーク 遠隔教育システム工学 人間力イノベーション論 創出力イノベーション論 優が7つ、良が1つでした。良があったのはとても残念でした。自習と比べると、必死に勉強しようと自然と思える点、テストやレポートを通して理解度が明確になる点、先生から興味深い話を聞ける点が良かったです。未経験のことを短期間で習得しようとすることも楽しいです。

In Maude, a module can be imported as a submodule of another in three different modes: protecting, extending, including. This is done with the syntax declarations protecting ⟨ModuleExpression⟩ . extending ⟨ModuleExpression⟩ . including ⟨ModuleExpression⟩ . which can be abbreviated, respectively, to pr ⟨ModuleExpression⟩ . ex ⟨ModuleExpression⟩ . inc ⟨ModuleExpression⟩ . The different modes of importation can be understood as promises by the user, which would need to be proved by him/herself. Before explaining each difference, I clarify no junk and no confusion. No junk is that extra values should not be added. No confusion is that different values should not be made equal.

誰? 大学では経済学を専攻していたが、大学院では情報科学の分野で研究をしたい人 社会人 プログラミング歴は約5年 受験の流れ 2020-04-19 オンラインでJapan Advanced Institute of Science and Technology(JAIST)の東京社会人コース説明会に参加した。 2020–04–22 関心のある研究室に受け入れが可能かを問うメールを送った。COVID-19のため、対面でなく、メールでやり取りすることになった。教授が発表した論文や担当している講義の資料のリンクが送られてきた。講義の単位を取得できそうとかなどについて確認するため課題を出していただくことになった。講義の資料はi217 Functional Programmingという講義のものだった。 2020–04–27 講義資料の指定された箇所を読み終わったという旨のメールを送った。1つ目の課題を出していただいた。

Let R@ be {(@1),(@2),(r1),(r2)} such that nil @ L2 = L2 (@1) (E | L1) @ L2 = E | (L1 @ L2) (@2) rev(nil) = nil (r1) rev(E | L) = rev(L) @ (E | nil) (r2) Theorem1 rev(rev(L)) = L Proof of Theorem1 by structural induction on L. Let e…

RustでBFSを練習するために、AtCoder AGC 033 A — Darker and Darker を解きました。 問題概要 「白」「黒」に塗られているH × Wのマスがあります。1 秒ごとに、各黒マスに対し、その上下左右に隣接したマスが存在するならば、そのマスを黒で塗りつぶします。全マスを黒で塗りつぶすのに何秒必要かを求めます。HとWには 1≤H,W≤1000 という制約があります。 解法 「各白マスに対して最も近い黒マスまでの距離」の中で最大の値を求めます。キューを使いたかったので、Rustでの標準ライブラリのstd::collections::VecDeque を使いました。std::collections::VecDeque にはpop_frontとpush_back があり、FIFOできます。 コードは以下のような感じで書きました。入力のマクロに関してはhttps://qiita.com/tanakh/items/0ba42c7ca36cd29d0ac8 を参照ください。

The aim of this blog post is to examine type-driven development with Rust. Type-driven development is an approach to develop robust and verified software, using a type system. The first section gives a brief overview of a type system. What is a type system? A type system is defined in the “Types and Programming Languages”…

In Layered Architecture (e.g., Clean Architecture, or Hexagonal architecture), the key idea is to use the dependency inversion principle. This blog post provides the dependency inversion principle in Rust, skipping the details of Layered Architecture. The sample in this blog post is a news app which gets news asynchronously. I…

まず、Berkeley Packet FilterとBPF Compiler Collectionについて簡単に説明していきます。(以下ではそれぞれをBPFとBCCと略します。) BPFとは BPFは独自の命令セットを持つVMです。ユーザーランドのコードをカーネル内で安全に実行することができます。”The BSD Packet Filter: A New Architecture for User-Level Packet Captur”によると、1992年時点ではパケットフィルタリングのためのものだったようです。現在はセキュリティやトレーシングのためにも使用されています。 BCCとは BPFでカーネルのトレーシングやフィルダリングなどを行うためのツール郡です。Python用のバインディングもあり、BPFを容易に扱うことができます。(実際にはC言語も書くことになりますが…) インストール方法はこちらをご覧ください。