概要 Egisonのパターンマッチの動作を定理証明支援系Coq上で定義し、「Egisonの処理系が項Mを値vに評価する」という命題をCoq上で表現できるようにしました。 動機 Egisonの中核的な機能はユーザが拡張可能なパターンマッチ機構です。例えば以下に示すように…

概要 MNISTの分類をする学習済みモデルを軽量化し、 更にSIMD命令を使った高速化を行うことで、 onnxruntimeより高速なMNISTの分類が可能になりました。(シングルスレッドで) 前回までのあらすじ この記事は前回の続きです。 前回はMNISTを分類する学習済み…

前回の続きです。 概要 前回の記事ではWebAssemblyを出力するMLのサブセットコンパイラを作りました。しかし、WebAssemblyにはGabage Collection (GC) が未だに実装されていないため(2019/7/8時点)、メモリ管理は全て自分で行う必要があります。前回は超適当…

この記事の中のソースコードは全てhttps://github.com/akawashiro/sonnxにあります。 概要 ニューラルネットワークから要らなそうな枝を80%削除しても精度が変わらなかった ONNXの中身をいじるのが大変だった onnxruntimeには勝てなかった 背景 機械学習の学…

高階関数をQuickCheckでテストしてみる QuickCheckを知っていますか? QuickCheckと言うのはHaskellのデータ駆動型のテスト用ライブラリで テストしたい関数を指定するとその引数に合わせて適当なテストデータを生成してくれます。 では高階関数(関数を引数に…

概要 WebAssemblyを出力するMinCamlコンパイラml2wasmをフルスクラッチで実装しました。 github.com マンデルブロ集合を計算するこんな↓感じのMinCamlのソースコードが マンデルブロ集合を出力するMinCamlソースコード こんな↓感じのWebAssemblyに変換されて…