Profile cover photo
Profile photo
Masahiro Sakai
799 followers
799 followers
About
Posts

Post has attachment
自分自身の無矛盾性が証明できる強い自然数の理論体系
https://yoriyukiy.com/2018/10/17/%E8%87%AA%E5%88%86%E8%87%AA%E8%BA%AB%E3%81%AE%E7%84%A1%E7%9F%9B%E7%9B%BE%E6%80%A7%E3%81%8C%E8%A8%BC%E6%98%8E%E3%81%A7%E3%81%8D%E3%82%8B%E5%BC%B7%E3%81%84%E8%87%AA%E7%84%B6%E6%95%B0%E3%81%AE%E7%90%86/

Löbの条件の二つ目 T ⊢ Prov(⌜φ→ψ⌝)∧Prov(⌜φ⌝)→Prov(⌜ψ⌝) 、もしカットありの二階算術で成り立つなら、カット除去すればカットなしの二階算術でも成り立つのではと思ってしまって、ちょっと混乱。

⊢ だけでなく Prov もカットを許容するかで二種類あるんだな。
これらを ⊢_{cut}, Prov_{cut} と ⊢_{cut-free}, Prov_{cut-free} と書き分けることにして、
T ⊢_{cut} Prov_{cut}(⌜φ→ψ⌝)∧Prov_{cut}(⌜φ⌝) → Prov_{cut}(⌜ψ⌝) … (1)
は成り立つのだろうし、
T ⊢_{cut} Prov_{cut-free}(⌜χ⌝) → Prov_{cut}(⌜χ⌝) … (2)
は自明だ。ここで更に
T ⊢_{cut} Prov_{cut}(⌜χ⌝) → Prov_{cut-free}(⌜χ⌝) … (3)
も成り立つのであれば、これらから
T ⊢_{cut} Prov_{cut-free}(⌜φ→ψ⌝)∧Prov_{cut-free}(⌜φ⌝) → Prov_{cut-free}(⌜ψ⌝) … (4)
が導けて、これにカット除去を適用して、
T ⊢_{cut-free} Prov_{cut-free}(⌜φ→ψ⌝)∧Prov_{cut-free}(⌜φ⌝) → Prov_{cut-free}(⌜ψ⌝) … (5)
が言えてしまう。

これが言えないという話だから、何が間違っているのかと考えてみると、怪しいのは (3) で、もしそうだとすると「竹内予想は(カットあり)二階算術の内部では証明できない」ということなのだろうか(適当)。

#ns
Add a comment...

Post has attachment
Happy Halloween! githubのcontributionがハロウィン仕様になってた🎃#ns

Photo
Add a comment...

Post has attachment
Safe Exploration in Continuous Action Spaces https://arxiv.org/abs/1801.08757 現実の機器の制御などを考えると、強化学習は安全な範囲で動作する必要があるが、これは訓練時の探索とは相反する面がある。 この安全な強化学習という課題に対して、この論文では元の方策ネットワークの最後にくっついて Safety-Signal の値を範囲内に収めるようアクションを修正する層である Safety Layer というものを提案している。

これはどうやるかというと、まずは Linear Safety-Signal Model として、現在の状態を入力として、「アクション値から系の1ステップでの Safety-Signal の値の変化の線形近似」の係数を返すようなモデルを学習する。 これは過去のデータなどから学習できる。

次に Safety Layer はこの係数を使って、Safety-Signal の値が範囲内であって、元のアクション値からの距離が最小であるようなアクションを求めて出力する。 これは凸最適化なので普通に解くのは可能だけど、問題は Safety Layer を追加したポリシーネットワーク全体を学習するためには微分可能でないといけないこと。 一つの方法は OptNet https://plus.google.com/+MasahiroSakai/posts/4rHUAKeueTH のような微分可能な最適化層を使うことだけど、ここでは最適解では制約条件のうち高々一つしかアクティブ(制約条件の不等号がイコールで成り立つこと)ではないと仮定して、最適解(候補)を解析的に表すことで、この問題を解決している。 この方法は反復法を用いるよりも実時間の制御に向いているという利点もある。

実験では、制約違反が発生するとエピソードが終了してしまうような問題設定で、素のDDPG、DDPGで制約違反をペナルティとして報酬に反映した場合と比較して、それらと異なって全く制約違反せず、かつよりよい報酬のポリシーを学習できた(しかも収束が早い)。

#ns
Add a comment...

Post has attachment
Machine Learning-Based Restart Policy for CDCL SAT Solvers https://link.springer.com/chapter/10.1007/978-3-319-94144-8_6
SATソルバでリスタートが何故性能向上につながるのかの仮説の検証と、それに基づいた機械学習ベースのリスタート方策の提案。

前者に関しては、これまで乱択での実行時間の分布の裾の重い部分を引いてしまったのを回避できるという仮説などがあったけど、ここではリスタートが割当スタックをコンパクト化することを通じて、良い節が学習できているからという仮説に立っている。この仮説を検証するために、リスタート間隔の短さとコンフリクト時の割当スタックのサイズの相関、割当スタックのサイズと(良い節の尺度である)LBDの短さの間に相関があること、LBDの短さと(リスタートに要する時間を除いた)ソルバ時間の短さの間の相関を実験的に確認。

これに基づいて機械学習ベースのリスタート方策として、過去のLBDの系列から次のLBDを予測して、それがLBD分布の99.9%分位点を超えていたらリスタートするという方策を提案。 LBDの真の分布は分からないので過去のLBDから正規分布で近似、次のLBDの予測に関しては過去の3回のコンフリクトのLBDを用いた二次多項式回帰なんだけど、コンフリクトの度に全データを使って回帰をし直すのではなく、新しく得られた1サンプルだけを使ってAdamを1ステップ実行する形で学習していく。

実装はGlucoseを改造して実装。 性能的にはLuby数列を用いたリスタートよりは良いが、Glucoseのデフォルトの方策(直近50コンフリクトの平均×定数(デフォルト0.8) が全LBDの平均を超えた時にリスタート)よりは悪いという結果(その間くらい)。

accepted papers のリストが出た時にタイトルから連想したものとはちょっと違ったけれど、面白かった。
あと、スライドの方には Research Question (RQ) と書いてあるけれど、ソフトウェア工学系の論文以外で RQ と書いてあるの初めてみたかも…… (^^;

スライド https://easychair.org/smart-slide/slide/nTSR
ソースコード https://sites.google.com/a/gsd.uwaterloo.ca/maplesat/mlr

#ns
Add a comment...

Post has attachment
ug[SCIP-Jack, MPI]: A Massively Parallel Steiner Tree Solver (Yuji Shinano): Steiner Tree Problem とその変種のためのソルバ、古いJack-IIIというソルバとSCIPを組み合わせたのがSCIP-Jackで、並列化フレームワークUGで並列化。 並列化自体は簡単にできるけど、性能を出すにはUGとSCIP-Jackの両方を拡張する必要があった。 参考: http://mpc.zib.de/index.php/MPC/article/view/196
Add a comment...

Post has attachment
Adaptive Algorithmic Behavior for Solving Mixed Integer Programs Using Bandit Algorithms (Gregor Hendel): https://opus4.kobv.de/opus4-zib/files/6956/paper.pdf の話。 ソルバでの各ヒューリスティクスをどれだけ使うかをBanditアルゴリズムでやる話。 対象は Large Neighborhood Search と diving heuristics と LP のpricingで、 LNSの(?)は SCIP 5 に含まれているらしい。
Add a comment...

Post has attachment
Verified Solutions to Integer Programming Problems (Daniel Steffy): https://github.com/ambros-gleixner/VIPR の話。 個人的にはDRAT-trimをresolutionからcutting-plane proof systemへ一般化するようなアプローチとの類似や違いが気になった。 あと、生成されるcertificateは数百GBくらいのようで、SATで200TBとか言っていたの https://plus.google.com/+MasahiroSakai/posts/dddK6XDk2A3 とくらべるとだいぶ小さな気はして、単に実験した問題が小さかったのか、本質的に小さくなる理由があるのかも、ちょっと気になった。
Add a comment...

Post has attachment
What is algebraic about algebraic effects and handlers? https://arxiv.org/abs/1807.05923 algebraic effect のどの辺りが代数的なのかという観点からの入門テキスト。 大体想像通りの方向性だったけど、実際の形式化はこんな感じなのね。 あと、Comodelの話とか面白かった。
Add a comment...

Post has attachment
The Shape of Art History in the Eyes of the Machine https://arxiv.org/abs/1801.07729 絵画データをスタイルで分類するCNNを学習し、その表現を次元縮約して分析してみたら、(年代を明示的に与えていないにも関わらず)年代の遷移が綺麗に埋め込まれていたり、美術史分野でスタイルをスタイルの同定に用いられる手法の比較軸に対応する(相関する)ような成分がみられたりとか。 図が楽しい。
Photo
Add a comment...

Post has attachment
なんか Macbook (Early 2016) の↑キーのキートップが外れてしまって、どう固定されていたのかよく分からん。
まあ、とりあえず乗せておけば押せるんで使えるんだけど……
Photo
Add a comment...
Wait while more posts are being loaded