データナード

機械学習と自然言語処理についての備忘録 (旧ナード戦隊データマン)

スクレイピングの13の手法

スクレイピングに関するいくつかの経験則をまとめました。特定のプログラミング言語に依存する話は少なくしてあります。 スクレイピングの困難点 1. ターゲットサイトのhtml構造に依存する。 2. スクレイピングの効率を上げるとDoS攻撃的な挙動になる。 3. …

deepholの設計の抽出 - 自動定理証明のお勉強 (8)

今回はdeepholの実際のコードから設計を抽出します。 tensorflow/deepmath deephol/main.py deephol/prover_runner.py#L46 deephol/prover.py#L132 deephol/prover.py#L110 考察 参考 追記 2020-07-04 X:Y 2020-07-04 12:57 tensorflow/deepmath github.com …

HOL Lightで「sqrt(2)は無理数」を証明 - 自動定理証明のお勉強 (7)

HOL Lightの使い方を学んできて、実際の証明手順がどうなるのかを確かめるために、 の証明を試します。 ※ HOL LightはITPであり、そのままではATPとして使えません。 HOL Lightで実行 まず、ゴールを定義する必要があります。HOL Lightはgoal-taticベースの…

HOL Lightを選ぶ理由 - 自動定理証明のお勉強 (6)

これまで、主にdeepmathに関する勉強をしてきたため、HOListベンチマークやdeepholで使われているものがHOL Lightであるという理由でHOL Lightを学ぼうと考えていた。ただ、ITPに関する比較論文(お勉強(1)で見たもの)をちゃんと読んでいなかったため、一応比…

自動定理証明についての疑問点/妄想 (2)

deephol-zero 1 などを調べ、HOListベンチマーク 2 のデモを動かし、長い証明に対応するための手法についての論文 3 を読む、などしてきました。まだ自分自身で実装できる段階にはありませんが、現時点での疑問点などを整理します。 有用な定理を発見したい …

より長い証明の発見 - 自動定理証明のお勉強 (5)

DeepHOL-zeroでは強化学習を使っていたが、その前のDeepHOLの模倣のコストが高かったらしく、それ無しで行うことで効率が上がっているようなものだった。他にアプローチはないかと探したところ。一つ論文を見つけたため、それを勉強してみる。 オリジナル情…

DeepHOL-zero - 自動定理証明のお勉強 (4)

前回の勉強では、Autfoformalizationが、自然言語文からの形式化という壮大な目標を持っていることがわかったが、その中でDeepHOL-zeroという、HOL Lightでの人間のログを必要としない手法のようなものを見つけたため、これを掘り下げる。 オリジナル情報源 …

Autoformalization - 自動定理証明のお勉強 (3)

前回の勉強で、HOLを解く試みとしてITPから訓練・評価のデータを得て、それを使って定義されたタスクをディープ系手法で解くことで人間が行う証明を模倣するような試みがあるということがわかりました。このタスクに関するもっと抽象的なこと、あるいは全体…

HOLに対する機械学習の適用 - 自動定理証明のお勉強 (2)

前回の勉強では、形式的手法と数理論理学について大雑把に学び、HOLをルールベースで解くのは計算困難であるらしいということがわかった。しかし、任意の数学理論の形式化という点に興味があるため「HOLを解くのは難しい」だけでは満足できない。そこで、「…

形式的手法と数学的論理 - 自動定理証明のお勉強 (1)

自動定理証明について学んだことをメモします。 はじめに 概要 形式的手法 model checker theorem proving 数学的論理 Propositional Logic First-Order Logic High-Order Logic 疑問点 参考 追記 2020-05-18 6:38 はじめに 前回、この分野についてほとんど…

自動定理証明についての疑問点/妄想

自動定理証明は、数学的定理に対する証明をコンピュータによって与えることです。 はじめに 思考実験 次回 はじめに 「趣味レベルでやるにはちょうどよくて、勉強にもなるし、面白そうだし、そのひとつだけを趣味にしても退屈はしなそう」というトピックを探…

決定木と説明可能性

決定木とは、if then形式で表すことの出来るルールをデータから学習することで予測を行う機械学習アルゴリズムの一つです。 概要 titanicデータで検証 3つのモデルの比較 一つの巨大な木 max_leaf_nodesを制限した木 複数の木をアンサンブルする ノイズの影…

特徴量設計とロジスティック回帰

特徴量設計とロジスティック回帰の組み合わせは、説明性が高いシンプルなモデルの一つです。 特徴量設計とは何か ロジスティック回帰 特徴量設計とロジスティック回帰 ディープラーニングとロジスティック回帰 各モデルの検証 特徴量設計モデル Keras版ロジ…

自然言語処理でできること

「自然言語処理でできることは何か」という問いは有用性の観点から考えると自然に思えます。自然言語処理を研究して論文で発表したいのではなく、それを現実の機能要件1 に対して利用したい人もいます。ここでは、自然言語処理でできることについて、有用性…

お知らせ: githubとブログ内容について

これまで記事内でgithubページへのリンクを載せましたが、いくつかのリポジトリを非公開にします。 sugiyamath · GitHub 基本的には、以下の種類のプロジェクトをprivateに変更しました: 実験のために作成したもの。(keras-laser等) ほとんど役に立たず、ゴ…

HConvNetの実装

HConvNetは、Convレイヤーを積み上げ、各ConvレイヤーのMax Poolingを結合することでSentence Embeddingを生成する方法です。 概要 コード 考察 参考 概要 https://research.fb.com/wp-content/uploads/2017/09/emnlp2017.pdf LASERは、エンコーダで複数のBi…

keras-tunerを使う

keras-tunerとは、kerasのハイパーパラメータチューニングのためのツールです。 概要 コード サマリーの出力 考察 参考 追記 2020-04-15 13:10 2020-04-16 9:12 概要 問題: kerasでlaserを実装する際に、論文内に記述のない部分があり、その部分のパラメータ…

keras-laserの修正: ミニバッチ戦略の変更

ミニバッチとは、訓練イテレーションごとに全データの中から部分集合を抽出することです。ミニバッチ戦略は、そのミニバッチの生成方法に対する戦略です。 概要 適用したミニバッチ戦略 コードの主要部分 問題は解決できたのか この手法についての考慮点 次…

keras-laserのいくつかの修正

問題点 kerasでlaserを実装中だが、文Embeddingを使ってみると、どんな文ペアでも殆どが1に近い類似度になってしまう。 現状の解決策 build_model関数でモデルの主要な部分を引数から設定できるようにする。 問題点 現状の解決策 いくつかの仮説 問題に関連…

機械学習研究のためのREADME.mdテンプレート

開発者は、研究者と呼ばれる人々の研究成果をしばしば利用します。そのため、それらの研究成果の再現性は重要です。今回、Papers with Codeが機械学習コードの完全性のためのチェックリストを作成したようなので、それを見てみます。 英語読める人向け 概要 …

OPUSからデータを得てアラインメントする

OPUSとは、継続的に更新を続けている公開パラレルコーパスのコレクションです。 概要 コード 参考 概要 LASERの訓練時に、WikiMatrixを使っていましたが、データの質が悪いらしく、Sentence Embeddingがまともに機能しませんでした。そのため、LASERの論文内…

keras-laser: LASERをkerasで実装

LASERはマルチリンガルのSentence Embeddingを獲得するためのモデルで、facebook researchによって開発されています。 概要 事前準備 主要なコード 現状のモデル 現時点での考察 参考 LASERのオリジナルの事前訓練済みモデルはfairseqを用いて訓練されている…

Semantic Retrievalとは

Semantic Retrievalは、情報検索(IR)タスクの一つで、コーパスからクエリに類似するすべての文を探すタスクです。最近の手法は、主にエンコードされた対象の探索をANN(近似最近傍法)によって行い、その検索精度を評価します。ANNの手法が固定だと仮定すると…

sentence embeddingとdeep metric learning

paraphrase retrievalは、大量の文を保存したシステムに対してクエリを投げて、パラフレーズを高速に検索するタスクを指します。今回は、ベクトル検索のためにパラフレーズコーパスからsentence embeddingを学習する方法についてのメモを書きます。 triplet …

パラフレーズ獲得のbilingual pivotingを実装

bilingual pivotingは、対訳コーパスからパラフレーズを獲得する方法です。 概要 事前準備 mosesで対訳フレーズのアラインメント word2vecとkenlm コード 出力の一部 追記 2020-03-04 15:05 2020-03-05 9:34 2020-03-08 22:53 参考 github.com 概要 ググった…

edict2をjsonに変換

edict2は、JMdict/EDICTプロジェクトで作られている日英辞書です。この辞書を、英語をキー、キーに対応した日本語の単語リストをバリューとしたjsonに変換します。 事前準備 edict2のダウンロード edict2をutf-8化 pythonコード 出力の一部 追記 2020-02-27 …

PAWS-Xに対してhuggingfaceのBERTを使う

PAWSデータセットは、パラフレーズ検出のための英語データセットの一つですが、PAWS-Xはその多言語版です。 概要 ベースライン コード 訓練 テスト 結果 考察 参考 今回は、huggingfaceのBERTをPAWS-Xに使います。 概要 huggingface/transformersというプロ…

wordnetをベクトル化: 意味の外延的定義

意味の外延的定義とは、語の意味を、その語が表すすべてのもので表す方法です。例えば、乗り物={車, 電車, 自転車, 飛行機,...} など、全乗り物の集合で乗り物の意味を表します。 今回は、この外延的定義のアイデアを借りてwordnetをベクトル化します。 概要…

paraphrase retrievalをfaiss+laserで試す

paraphrase retrievalの概念的なメモを前回の記事で行いましたが、今回はベースラインモデルとしてfaiss+laserを使います。 説明 事前準備 データのダウンロード faissのインストール laserのインストール laserencoderのインストール 実行 データの分離 タ…

paraphrase retrievalについてのメモ

paraphrase retrievalは、クエリ文と同等の意味を持つ文をシステムから検索するタスクです。 整理 ベクトル検索 具体例 参考 整理 パラフレーズとはある文の言い換えのことですが、paraphrase retrievalではクエリと同等の意味を持つ文をシステムから検索す…