# 入江ミーティングノート(2024-06-14~)
以前のミーティングノート https://hackmd.io/mp08Fyi2SyuJ7leq-xiM5A
# 2025-02-28
- ポスター
- 文字サイズ
- 絵+Goal(学習対象の関数を正しく表現する記号的ミーリオートマトンを出力する)
- PAC ver 絵+Goal(学習対象の関数を「大体正しく」表現する記号的ミーオートマトンを「高い確率」で出力する)
- できるだけ早く問題設定を伝える
- 同じ感じでsymbolic Mealyの貢献も伝える
- 今後の課題は優先度低め
- 証明や定義やらの相談
- PACアルゴリズムからpartitioning functionを構成する定義がうまく書けていない
- conceptとsymbolic Mealy の接続をうまく書きたい(各状態にはpartitionがある+状態と出力によって分類+その分類はObservation Tableに記録されている)
# 2025-02-21
- i.i.d.であることを成り立たせるために\Sigma_Eがmultisetになりました
- アルゴリズム
- 反例の各文字を全てmultisetである\Sigma_Eに突っ込むようにする
- output-closedは廃止
- PACのalgorithmからpartitioning functionを構成するようにするにはどう書けば良いか
- posterへのコメント
- 「ざっくり3分で説明してください」と言われたときに対応できる準備をまずする
- PAC学習とは何か、symbolic automatonとは何かくらい
- 貢献に最速で突入しないと3分で説明できない
- この話を上の方に書く
- 下の方にもっと詳しい内容を知りたい人向けの説明を書く
- アルゴリズムの話とか
- 何が非自明かとか

# 2025-02-18
- ここからやること
- 疑似コードを書く　確率分布のところをきちんと考察するなどの詳細な部分をきちんと書く
- Related workなどとの比較を (脳内にある状態から) 人に説明できるレベルで明確にしておく
- 発表などの上で必要なhigh-levelなポイント
- この問題が解けてなぜ嬉しいか
- そもそもPACとは何かという話がある程度は伝わらないといけない
- これまで何ができていたか
- 何が難しいか
- 「普通にやったらできないんですか?」に対しては、普通にやったらMaler & Mensになるというつもりで、何がMaler & Mensと違って嬉しいのかを説明すれば良さそう
- どういうことをやったか
- learning algorithmの話をしつつ、ここがMaler & Mensと違う話をするのが良いのかもしれない

# 2025-02-14
- PAC
- Partition learningにおいて、何をtraining dataとして使うかを明確にする (i.e. symbolic automatonのlearningの言葉で書く)
- target partitionがtraining dataのlabelから明らかになるはず
- target partitionとtraining dataがsymbolic automatonの言葉で与えられると、PACの保証している性質をsymbolic automatonの言葉で書けそう
- 元々はtraining dataとtarget paritionの言葉で書いてあった
# 2025-02-07

## ICALP版について

- "lower bound"という言い回しを変えるか?
- 一応直後で回収はしているので、基本やらない
- 但し proof readingのときにちょっと補足してより誤読しないようにするかも

## ここからお願いしたいこと
- ~~修論最終版でのtypoなどの差し替え~~
- なさそう
- 修論関連の一式を `argo:/share/paper/master/2025` にuploadする
- 修論のソースコード
- 実験のソースコードと生データ
- ソースコードはGitHubに最新版が置くことで代用
- https://github.com/SoftwareFoundationGroupAtKyotoU 以下に動かす
- 修論発表のスライド
- できるだけ早く発表を録画した動画を作って末永さんに送る
- 最低限の `README.md` の準備
- 要は実験の手順を書く
- 一応環境構築から、実験を回すところまで書いてください
- 修論中にある各データについて何をやると対応する実験を回し始めることができるのか
- (いまどきはChatGPTがこういうのを作るのをすごく得意なので、 .bash_history の一部を与えると自動で作ってくれるかもしれない)
- ~~卒業後に連絡の取れるメールアドレスを和賀に教える~~
- fos.kuis がGmailアドレスになっているので fos.kuis で良い
- そのうち (武井さんに) iPadを返却する

## PAC-learnabilitiyについて

- 今長さの確率分布とdomainの確率分布を独立に取ってきているが、wordの確率分布だけを取るようにしても同じような議論ができるかもしれない
- 長さに関する指数爆発みたいなのは、上手くεを使ってboundできている
- wordの確率分布からdomainの確率分布を作ることはできそう(?)
- sampleしてn文字出てきたらそれが次のn回分のsampleになるような分布とする

## その他

> そもそもRPNI-styleのalgorithmでsymbolic automata learningができるのか、というのは若干微妙な話です。去年PeterとIRIFで議論したときは無理ではという結論になりました。Sicco Vewerのtimed automata learningみたいな方向だとできるかもしれないですが

→ Inferring symbolic automataのSection 7以降を読むと良さそう

# 2025-1-24
- 修論
- Abstract
- 提出
- 論文
- Boolean algebraの追記
- Equalityを復活させた
- Intervalの前に置いて
- 実験節に明示的にequalityを使っていることを書く
- Master thesisに反映させて読んでもらう
- PAC
- とりあえずできたところまで

# 2025-1-21
- 修論
- hyperlinkはdvipdfmxをhyperrefを読み込むときに入れるとうまくいった
- がtheorem,lemma,propositionを通し番号にしているとrefが全てtheoremになってしまう
- 内見のメール
- 論文
- 関連研究とDrewsらのものよりも良いことの追記をしました
- 後で読んでほしいpageとlinenumberを送ります
- Boolean algebraの追記はまだやってない
- PAC
- 自分はこんな感じに考えているという証明を書いたので説明しますがつっこみどころが多いと思います
- 証明の流れ
- s\in Sでアクセスできる状態に関してはPACの定義がかかる 遷移or 出力を間違える確率が低い
- とある条件(sを読んだ時と同じだよねみたいな感じ)を満たすw \in \domain^+でアクセスする状態に関しても遷移or 出力を間違える確率が低いことを証明
- 状態を増やさない反例のprefixは上のとある条件を満たすことを証明
- よって状態を増やさない反例は遷移or 出力を間違える確率が低いから　出現確率が低い　多項式で抑えられる
- 一番最初の定義で突っ込まれる気がする
- PACの性質として何が成り立っていることを認めるのか?
- hypothesisがtargetよりも状態が小さいので,遷移する先がhypothesisには存在していないかもしれない

# 2025-1-17
- 修論
- ページ数がオーバーしそうなのでworked exampleは付録行きにしました
- hyperlinkがうまく動いていない?
- Waga: amsthm, hyperref で検索すると出ると思います
- 題名を改行したいがそうするとabstractの題名まで改行されてしまい困っている
- 現段階で48ページなので、3ページ減らさないといけないので一部の証明を付録に送ろうかなと考えています
- Omitted proofというsectionを作る
- 論文
- 関連研究の追記
- Boolean algebraの追記
- conjunction of Boolean literalsでやろうと思っています (述語の集合でBoolean closureはとれないようにするみたいな制約や工夫が必要になると思うけど)
- というのもconjunction of Boolean literalsはefficiently PAC learnableらしいので、PACが完成した時の一つのBoolean algebraの例としても使えて良いかなと思っています
- reviewerはBDDでやったら?みたいなことを書いていたけど、BDDはpolynomialではない派閥がいるので(関係ないとはいえ)避けようかなと思っています
- equality or propositional を書いて　実験で使っていると書く
- Drewsらのものよりも良いことの追記
- これをどう書けば良いでしょうか?
- Drewsらはquadraticだが、我々はlinearであるということを書けば良い
- PAC
- アルゴリズムを変えました
- formalizationがうまくいかず止まっている
- formalizationがうまくいかないということは間違っているかも?

# 2025-1-9
- 修論
- 証明は別にしても良いか? 実験の直前に移す
- 付録送りにしたアルゴリズムの説明を戻して良いか? 戻します
- worked exampleをアルゴリズムの後に挿入して良いか? 証明の直前に移す
- abstract for exampleを入れる
- tikzの図
- PAC
- 多項式で抑えられてPAC-learnableであると主張できるのではと計算していて思ったので話します
- Boolean algebraのaccuracyとconfidenceにはかなり強い制約がかかるけど、全体のaccuracyとconfidenceは一応任意に取れるので大丈夫かなと思っている
- 少なくともprobability 1で停止するよりは良い気がしている

# 2024-12-20
- PAC
- Maler & Mensのアルゴリズムって停止しないのでは?
- p19 " The number of counter-examples that only change the boundaries in a partition is bounded in a probabilistic setting of approximate learning. The probability of finding a non-expansive counter-example ultimately decreases converging to zero."
- non-expansiveってそれはcounterexampleなのかよくわからない
- expansiveがpacのapproximateに近づけるみたいな意味だったらわからなくもないけどそれだと別にzeroにconvergingはしないのではという気もする
- 有理数がdomainだったらnot converging to zeroな例は構成できるんじゃないかと思う。
- ここが自分が抱いていた違和感の正体だった
- L*だとOracleの実装において状態数nを知る必要はなくr_i回membership queryを聞けばそれで終わりだった(n回反例が返ってくればそれでdistinguishing stringは構成できてeqがyesを返してアルゴリズムは停止するので)
- Λ*だとBoolean algebra partitioning functionによって停止しない可能性がある
- 例えばIntegerのintervalや有限集合だったら停止性は言えるはず(\forall のクラス)
- (\existsのクラスは)oracleに条件がないと停止しないはず
- なんらかの条件をoracleにつける必要がある(ただし学習前に知り得る情報で)
- PACを利用して条件付けできないか?
- Λ*の述語の構築はpassiveさがあるのでPACとは相性がいいと思う
- 色々考えたアルゴリズムがあってメモがあるのでそれを見せます

# 2024-12-13

- TACASなどについて
- 会社的に行けるのであればTACASに発表しに行きたい
- → ETAPSの開催が割と年度頭に近いので、論文が通ったら早めに会社に連絡してください
- AEをがんばる
- 先に色々やりたいのであれば、Rebuttalでやると言った内容を追加するのを早めにやってもよいかも
- PACの話

# 2024-12-6
- Rebuttal
- Reviewer2が何を求めているのかわかってない
- PACOracleとSymbolicBreakpointAnalysisを実装しました
- 見せます
- SymbolicBreakpointAnalysisがあった方がObsTableが小さくなっていて、output queryが減っていると思う
- ProductAlgebraクラスのparitioning functionの仕様(バクではない)
- 解決策 x軸の\SigmaEとy軸の\SigmaEのそれぞれのpairについてoutput queryを投げられるように\SigmaEに突っ込む
- これはかなりSigmaEが増大するがしょうがないか?
- Boolean algebraのPAC learnabilityがそのままautomata learningのPAC learnabilityにいくというのは考えられる
# 2024-11-26
- 進捗があまりない
- Oracleの設計
- 反例処理のアルゴリズムをとりあえず説明します
- 二分探索を追加するメリットを示せるか?
- observation tableを小さくするために二分探索をしているつもりだったが、observation tableを小さくすることによって発生するメリットはmembership queryの回数を減らすことだったので、二分探索で余計なmembership queryがかかるのでこれが割に合うのかは結構微妙かも?実験的にこれは示すしかないかもしれない
- 一方で二分探索だとintervalの端っこを当てられるので正解を当てられる確率は高くなる気もする 正解を当てられやすいので結果としてequivalence queryの回数が減って、membership queryの回数も減ることはあるかもしれない　これも実験的に示すことになりそう
- BlackBoxCheckingと組み合わせるときに、ちゃんと正解を当てる必要があるのかも結構微妙か?
- 二分探索を追加することで正解をきちんと当てられる　一方で結局PACの枠組みに乗っかっているのでどうしても近似的になる　この二つが地味に相性が悪いようにも思う
- 状態数の上限の仮定とSigmaが有限であることの仮定があれば必ず有限回で正解に辿り着くことは証明できるかもしれない
- これだと別に二分探索なしでも正解に辿り着くが、計算量は改善するのではないか?
- 2分探索を追加するメリットがありませんでしたでも別にそんなに悪い結果ではない(論文にはならないかもしれないが)と思っているのでとりあえず作ってみる
- 一方でSymbolicBreakpointを探すのは明らかにmembership queryの計算量の改善が見込めるのでやる価値あり
- Waga: 二分探索について、ゴールをどう定めるかという問題のように聞こえます
- 1. Symbolic Mealy machineのためのPAC learning algorithm
- PAC learnableであるという証明を書く + そのためのアルゴリズムの構築という意味では多分二分探索は不要
- そもそも[Maler & Mens]と多分ほとんど同じ
- 2. Symbolic Mealy machineのための(状態数などを仮定した上での)exact learning algorithm
- 二分探索が真に必要かどうかは仮定次第なのでやや不明だが、恐らく最終的な計算量を削減できる?
- 例えば {1,2,…,N}の整数上のsymbolic automatonを考えるときに、boundaryを見つけるのにかかる時間がO(N)ではなくO(log N)に改善できるとか
- 3. 現実的に上手く動く (少ない回数で精度良く学習できる?) Symbolic Mealy machine のための learning algorithm
- Naiveには2. と同じような理由で、二分探索を行った方がquery efficientなのではないでしょうか
- 二分探索を行わないことによるSigmaEの増大と、二分探索を行うことによる追加のoutput queryのどちらが問題になるかという話に聞こえます
- 理論的な考察が可能か?
- SigmaEが1増えると状態数個だけprefix側が増える
- 上手く端を当てられたときと比べると $|S| \times (|E| + 1)$ 個 (くらい) output queryが増える
- 二分探索のコストは状態数とは依存しなそう (ドメインの大きさに依存)
- 二分探索を行うとequivalence queryの回数も減る。equivalence queryをoutput queryで実現しようと思ったときの計算量の見積りはどうすれば良いでしょうか…
- W methodとかなら可能
- 実験的な比較・考察はもちろん可能かと
# 2024-11-15
- Artifact Evaluation
- 進捗が遅いです　すみません
- 手軽にやる人向け これがshort evaluationに対応するつもりhttps://tacas.info/artifacts-25.php
- practicalおよびrandomのsubset(繰り返し回数は1 random生成は各configで10) 合わせても12時間以内で収まる
- これで最低限動くことが確認できるはず
- randomのsubsetはrandom生成を新しくする 前から入っていたrandom生成したものを動かすscriptもあった方が良いか? いらない
- short evaluationって実験結果が論文の数値と一致するか見られる?
- 見られるならnotebookを用意してあげたほうが親切か? あっても良い
- 色々やる人向け
- おまけ
- detailed instructions for use of the artifact and replication of results in the paperに対応するつもり
- 完全再現のスクリプト
- notebook 図とかを用意できないといけない
- Oracleの設計
- 実装していて、間違い(学習が進まなくなる例)が考えついたので、そこで止まっています 問題点は反例の追加の仕方
- 択は二つ
- Rivest & Schapire styleにしてしまう というかMaler Mensの手法そのままでいく
- 良い点:色々考えずに済む 反例解析に関する性質は証明しないで良い 計算量が理論上よくなる
- 悪い点:我々のアルゴリズムの諸々の定義や証明を書き直す必要があり面倒 Eに\SigmaE^*の要素でないものが出現しうる　状態が確定で増えるから停止性の証明は難しくないかもしれない アルゴリズムが複雑になり読む人が大変
- きちんとprefix-basedな反例の追加の方法を考えつく
- 上の条件出力が食い違わないときに確定で状態を増やし、かつintervalの端っこのcharacterで構成されるsuffixを作る必要がある
- 出力が食い違わないことがわかったら、後ろの方に向かって行きそれぞれ現在のabstractionとの2分探索をする? これはいけそう
- それで構成した反例のprefixを全て追加
- 必ず反例になっているので停止性はok
- 後の部分はm-1回で抑えられる
- 

# 2024-11-8
- Artifact Evaluation
- 締切は1/9
- 進んでいないです　すみません
- 必要なスクリプトやファイルが足りていないことに気づいた
- random experimentに関しては状態数とSigmaEを指定する必要があるがこれも全て自動化させたほうが良いか?
- 生成と回すを分離させる
- 手軽にやる
- 12時間以内に収めるには　繰り返し回数を削るのであれば　繰り返し回数をデフォルトで置いておいてあとで小さくしてもらう
- 最低限動くことを確認させる
- 色々やる
- 手を動かすことを要求する
- 論文にないような実験を　状態数とsigmaEを受け取ったら特定のどこかのフォルダの下に作る
- 今あるやつの使いかたを説明する
- subsetやreproduceしたものをまとめるnotebookも作った方が良いか?
- 今のところあるのは既に入っている実験結果をまとめるnotebookのみ
- 今のままでここを変えてくださいと説明を書いておく for 色々やりたい人
- README こういう風にやれば 基本手軽にやる人のために書く　最後に色々やりたい人向けに書く
- まっさらな状態から試すにはどうすれば良いですか。vmを準備することにも関係があるかもしれません
- PACを大体理解したつもりです
- 質問:確率分布Prは何を返す関数 in Angluin's paper
- Maler and Mensのsymbolic automata learningの論文を読みました
- Proposition 1(Symbolic Breakpoint)と6章のPACの結果はとても大事に思いました
- Proposition1を我々の枠組み的に書き直したい
- cex analysisはcav18にもある
- Oracleの設計の方針
- とりあえずrandom samplingによるtest生成をPACの枠組みでやる （これでPACの保証が学習結果につく)
- testを全て通ったら学習終了
- testが通らなかったら、それを反例(仮)とする
- 反例(仮)をうまくrefineする(目標はobservation tableをできるだけ小さくすること)
- ここでMaler and MensのProposition1のようにBreakpointをidentifyする
- (i)partitionのrefinement 理想は(refineする状態に到達するまでのword consisting of \SigmaE)+(new character) Proposition1 (2) と二分探索を組み合わせる
- (ii)状態を増やす 理想は word consisting of \SigmaE Proposition1 (3)
- 問題点はMaler Mensはsuffix-basedな反例解析(Rivest & Schapire style)なのでこれをprefix-basedにしないといけない　あるいは我々のアルゴリズム自体をRivest & Schapire styleに改造するか
- 方針をまとめたい

# 2024-11-05 (Chat with Marco)

- Equivalence testingを実装するだけなら特に制約なくサンプリングするのが妥当そうなので、難しいことを考える必要はなさそう
- 今回は恐らくこれで十分
- 上手く長さを決めた後は適当にhyper-rectangleからサンプルすれば良い
- 万が一 inclusion testingが欲しくなったら wordgenみたいな方法が必要になるかもしれない
- target languageのunderapproximationが欲しいときとか?
- 今回はあまり関係なさそう
- 必要になったとしても、今我々が考えているのはhyper-rectangleなので、samplingは簡単
- 万が一より複雑な制約を扱いたくなったらpolyhedraからのサンプリングなどが出てくる
- が、そんなことは考えなくて十分そう
- 一方でPACとかの議論のときにMarcoと議論をすると良いかもしれない
- 例えば(source state毎の?深さ毎の?)sample数を決めるために [Chernoff bound](https://whyitsso.net/math/statistics/Chernoff_bound.html) とかを使う必要があるかもしれないが、その辺りについて我々より詳しいはず

# 2024-11-1
- 借りていた本を返却します　ありがとうございました
- artifact
- まだ完成してません
- 誰か他の人が書いたartifact evaluationを読みたい
- ドキュメントの整備　
- CAV'23: https://zenodo.org/records/7923763
- CAV'24 template: https://zenodo.org/records/10679818
- CAVの諸々: https://zenodo.org/search?q=artifact%20cav&l=list&p=1&s=10&sort=bestmatch
- 今後の方針?
- Oracleの設計
- 前に言っていたtimed automatonの論文ってありますか
- Oracleをどう作るか?
- samplingが大変かもしれないし、普通にやるので十分かもしれない
- とりあえず Marcoと相談する
- 反例を上手く「小さく」したい
- 何かしらこれまでの手法の拡張で見つけた反例を上手く動かして良い「反例」にしたい
- 長さ → Rivest & Schapire?
- 値 → 二分探索?
- 反例の中に登場する文字は、できるだけこれまで知っている値を使いたい
- symbolic automatonの遷移とevidence automatonの遷移を見て、これまでに出てきた文字を使ったときに同様に反例でありつづけるかを確認?
- それで再現できなかったら、これまでに出てきた文字との間で二分探索で境界を探る?
- 端を上手く当てる必要がある
- 二分探索とか?
- Conformance testingの book chapter: https://cs.unibg.it/gargantini/research/papers/motres05.pdf
- Angluin'87: https://people.eecs.berkeley.edu/~dawnsong/teaching/s10/papers/angluin87.pdf
- symbolic automata + PACならこれ?: https://www-verimag.imag.fr/~maler/Papers/learn-generic.pdf

# artifact evaluation
- 何があるか
- 論文中のalgorithmのJava実装
- 実験でも使っている
- 実験を行ったscript
- inputs used in the experiments such as including 入力のsymbolic mealy
- script to reproduce the experiments subset
- 実験のtable,figureを制作するjupyternotebookと実験結果をまとめるためのpython,スクリプトファイル
- どういう関係か
- 実験のtableとかfigureを再現できる part of　論文の
- Section3.1のアルゴリズムの実装
- Section4.1,4.2の実験のセットアップのShell script
- Section4.1,4.2で使われた実験のInput Inputの詳細はAppendixDに記述されている
- Section4.1,4.2の結果を再現するための実験のsubset
- Section4.1のTable2, Section4.2 Table3, Figure3 AppendixEのTable4を作るためのjupyternotebook,python, shell scirpt

# 2024-10-11

- 再投稿のプロトコル: 変更した人が再投稿する
- 一応他の人が変更中ではないことを確認

## 残りのやることや分担など

- Proof reading (和賀と末永さん)
- 但し優先度低め
- [ ] もう一度Spell CheckingとGrammar Checking (入江さん)
- Artifact (入江さん)
- 急ぎではない
- https://tacas.info/artifacts-25.php を見ながら進める
- https://etaps.org/2025/conferences/tacas/
- とりあえずDockerやVMのことは忘れて、「このドキュメントと実装があればうちの研究室のB4でも実験が再現できる」というものを作る

## DONE

- とりあえず現状の版でEasyChairに投稿 (入江さん)
- [x] 即死回避版の前でも良いので、とりあえず出す
- Abstract
- [x] 末永さん初稿
- [x] 入江さんと和賀と正しさの確認 + revise
- [x] もう一度確認 (末永さん + 和賀)
- [x] 末永
- [x] 和賀
- Introduction
- [x] 末永さんが見てわかるか確認
- [x] 和賀も改めて通読
- Related Work
- 時間があったらざっと見るかも?
- Preliminaries
- DFAの定義がないのが気になる?
- コメントから戻せばすぐに復活させられるので、残りスペースを見て調整
- 但し優先度は低め
- Our algorithms
- Complexity analysis
- Method
- Experiments
- [x] Proofreading of the Experiment section
- 末永さん
- Appendix

# 2024-10-10

- 本質情報

    Submission deadline for TACAS, FoSSaCS, FASE: October 10, 2024, 23:59 AoE
    (submitted papers can be polished until October 14 23:59, AoE)

- 但し:
- Waga: 10/13の夜に日本を出るので、あんまり仕事はできない
- 全体を通読するのは厳しいが、1 Section読むとかは可能だと思います
- Suenaga-san: HSCCと並行なので、proofreadingとreviseは可能
- 即死回避版は一応できた気がする?
- Waga: 気合で16ページにしました
- 基本方針: 収束はしたのでproofreadingをしてqualityを上げる

## 残りのやることや分担など

- とりあえず現状の版でEasyChairに投稿 (入江さん)
- [x] 即死回避版の前でも良いので、とりあえず出す
- Abstract
- [x] 末永さん初稿
- [x] 入江さんと和賀と正しさの確認 + revise
- [ ] もう一度確認 (末永さん + 和賀)
- [x] 末永
- [ ] 和賀
- Introduction
- [x] 末永さんが見てわかるか確認
- [ ] 和賀も改めて通読
- Related Work
- 時間があったらざっと見るかも?
- Preliminaries
- DFAの定義がないのが気になる?
- コメントから戻せばすぐに復活させられるので、残りスペースを見て調整
- 但し優先度は低め
- Our algorithms
- Complexity analysis
- Method
- Experiments
- [x] Proofreading of the Experiment section
- 末永さん
- Appendix
- Artifact
- https://tacas.info/artifacts-25.php を見ながら進める
- https://etaps.org/2025/conferences/tacas/

## DONE

- Figure 1を改良する (入江さん初稿 → 和賀と末永さんでコメント + revise。但しLaTeX周りを和賀と研究会直後に相談)
- Captionと本文で(?)簡単な読み方を説明する
- alphabetが無限だと全列挙できない!の図を追加
- "{a,b,c,d}"が全部だぞ、というのを明記する
- 上に波括弧で書くとか
- 真ん中の図では D = Nとかを書いて、自然数全部載せる訳にはいかないみたいなことを図からも伝えたい
- ΣEでもこれが本質的な文字全体だ、と書きたい
- (不要な情報を削ると良いかも?)
- → 和賀が手直しをする
- 絵に合わせて、introductionの文章を手直し (和賀 → 入江さんと末永さんでコメント)
- observation tableの最低限の見方
- Figure 1
- Niese
- Infinite alphabetつらい
- Λ*Mかしこい
- DONE Figure 2
- Section 3.2を頑張って削る (和賀 → 入江さんが正しさの確認)
- Λ*からの差分の説明に注力
- 一方で、Λ*からの各差分について、どうして変わったのかをAppendixで説明 (入江さん初稿 → 和賀と末永さんでかなりlightweightなコメント)
- 例えばoutput-closedかつevidence-closedよりcompleteになったので…みたいな話
- 各operationにつき1段落くらいの想定
- 構成は以下 (全部appendix以下)
- \section{Details of Algorithms}
- \subsection{\Lambda*}
- 各operationが何をやっているかを各operation毎に1段落 or 箇条書きで書く
- 基本的に今本文にある説明を持っていくので良いです
- ここにある意図: Λ*Mの説明のための前フリ。これがないと何が変わったのかわからないため
- \subection{\Lambda*M}
- 上記の話
- DONE 和賀と一緒に一回見る
- → 差分の話をする前に、Λ*Mでどうなっているかを一応書く
- 実験結果の詳細をAppendixに載せる (入江さん)
- Details of Algorithmsが終わったら Section 2.2を削る (和賀)

# 2024-10-09

## 残りのやることや分担など

- Abstract
- DONE 末永さん初稿
- DONE 入江さんと和賀と正しさの確認 + revise
- Figure 1を改良する (入江さん初稿 → 和賀と末永さんでコメント + revise。但しLaTeX周りを和賀と研究会直後に相談)
- Captionと本文で(?)簡単な読み方を説明する
- alphabetが無限だと全列挙できない!の図を追加
- "{a,b,c,d}"が全部だぞ、というのを明記する
- 上に波括弧で書くとか
- 真ん中の図では D = Nとかを書いて、自然数全部載せる訳にはいかないみたいなことを図からも伝えたい
- ΣEでもこれが本質的な文字全体だ、と書きたい
- (不要な情報を削ると良いかも?)
- → 和賀が手直しをする
- 絵に合わせて、introductionの文章を手直し (和賀 → 入江さんと末永さんでコメント)
- observation tableの最低限の見方
- Figure 1
- Niese
- Infinite alphabetつらい
- Λ*Mかしこい
- DONE Figure 2
- Section 3.2を頑張って削る (和賀 → 入江さんが正しさの確認)
- Λ*からの差分の説明に注力
- 一方で、Λ*からの各差分について、どうして変わったのかをAppendixで説明 (入江さん初稿 → 和賀と末永さんでかなりlightweightなコメント)
- 例えばoutput-closedかつevidence-closedよりcompleteになったので…みたいな話
- 各operationにつき1段落くらいの想定
- 構成は以下 (全部appendix以下)
- \section{Details of Algorithms}
- \subsection{\Lambda*}
- 各operationが何をやっているかを各operation毎に1段落 or 箇条書きで書く
- 基本的に今本文にある説明を持っていくので良いです
- ここにある意図: Λ*Mの説明のための前フリ。これがないと何が変わったのかわからないため
- \subection{\Lambda*M}
- 上記の話
- DONE 和賀と一緒に一回見る
- → 差分の話をする前に、Λ*Mでどうなっているかを一応書く
- Details of Algorithmsが終わったら Section 2.2を削る (和賀)
- Proofreading of the Experiment section
- 末永さんと和賀が主にやる
- 実験結果の詳細をAppendixに載せる (入江さん)

## DONE

- DONE Figure 2を作る (入江さん初稿 → 和賀と末永さんでコメント + revise)
- observation table → evidence Mealy → symbolic Mealy
- ↑ を通してオートマトンをどういう流れで構成するかが伝わるのが目標
- (入江さんの初稿ができたので、和賀がreviseする)
- DONE Conclusions
- DONE 入江さん初稿
- DONE 和賀revise
- DONE 以下をAppendixに移す (基本的に入江さん)
- Equality algebraの例
- Evidence compatibilityをsymbolic compatibilityのためのLemmaっぽい位置に移動 + Lemmaという名前にする
- 但し停止性の証明の中でも引き続き使う
- Query complexityの証明をAppendixに送る

# 2024-10-08
- 細かい話
- proposition23の下にあるqedはとって良い?
- → むしろAppendixに証明のあるTheoremなどは`\qed{}`を付ける
- Effective Boolean algebraの定義について
- → 問題ない。我々に必要な性質はこれ。正にこのことをeffective呼んでいる他の論文は存在しないかもしれないが、Effectiveと言ったらこれ、という性質が定まっている訳でもないのでこれで良い。
- 実験結果の詳しい話
- 反例の列の例を一つ載せても良いか? なんか分かりにくい気もする
- Appendixの話
- 「載せても良いかどうか」→ 載せて良い
- 理由: appendixにある情報は多い方が良い
- 説明が凄くわかりやすいかどうかはまた別の話
- introの図の説明 そもそも図要ります?
- introにsymbolic Mealyがないので 全体を通してsymbolic Mealyの図がひとつも載っていない
- ConclusionとAbstract 自分が書いて良いか?
- 短くする(以下は付録行きでいいと思っています　というのも付録の証明でしか使わないからです)
- Mealy automataの定義
- 比較的残しておきたい寄り
- Evidence compatibility
- Learnabilityのsectionの方針
- (というか昨日和賀が書いた感じでどうでしょう)
- 「各状態についての操作だ」という感じをもう少し出せると良い
- → もう15分から30分くらい見てみます
- Grammarlyやspell checkingなど、和賀の意図が伝わっているか確認したい
- → 研究会の後とかにやりましょう
- Spell checker
- https://ja.wikipedia.org/wiki/Ispell
- https://texwiki.texjp.org/?Aspell
- https://qiita.com/walking_with_models/items/da8eaf4afa39cf4ecd4a

## 残りのやることや分担など

- Figure 1を改良する (入江さん初稿 → 和賀と末永さんでコメント + revise。但しLaTeX周りを和賀と研究会直後に相談)
- Captionと本文で(?)簡単な読み方を説明する
- alphabetが無限だと全列挙できない!の図を追加
- "{a,b,c,d}"が全部だぞ、というのを明記する
- 上に波括弧で書くとか
- 真ん中の図では D = Nとかを書いて、自然数全部載せる訳にはいかないみたいなことを図からも伝えたい
- ΣEでもこれが本質的な文字全体だ、と書きたい
- (不要な情報を削ると良いかも?)
- Figure 2を作る (入江さん初稿 → 和賀と末永さんでコメント + revise)
- observation table → evidence Mealy → symbolic Mealy
- ↑ を通してオートマトンをどういう流れで構成するかが伝わるのが目標
- (入江さんの初稿ができたので、和賀がreviseする)
- Abstract (末永さん初稿 → 入江さんと和賀と正しさの確認 + revise)
- Conclusions (入江さん初稿 → 和賀と末永さんでrevise)
- Section 3.2を頑張って削る (和賀 → 入江さんが正しさの確認)
- Λ*からの差分の説明に注力
- 一方で、Λ*からの各差分について、どうして変わったのかをAppendixで説明 (入江さん初稿 → 和賀と末永さんでかなりlightweightなコメント)
- 例えばoutput-closedかつevidence-closedよりcompleteになったので…みたいな話
- 各operationにつき1段落くらいの想定
- 構成は以下 (全部appendix以下)
- \section{Details of Algorithms}
- \subsection{\Lambda*}
- 各operationが何をやっているかを各operation毎に1段落 or 箇条書きで書く
- 基本的に今本文にある説明を持っていくので良いです
- ここにある意図: Λ*Mの説明のための前フリ。これがないと何が変わったのかわからないため
- \subection{\Lambda*M}
- 上記の話
- Details of Algorithmsが終わったら Section 2.2を削る (和賀)
- 以下をAppendixに移す (基本的に入江さん)
- Equality algebraの例
- Evidence compatibilityをsymbolic compatibilityのためのLemmaっぽい位置に移動 + Lemmaという名前にする
- 但し停止性の証明の中でも引き続き使う
- Query complexityの証明をAppendixに送る

# 2024-09-27
- Contribution
- https://hackmd.io/@kengirie/Sy9kBKfAC
# 2024-09-20
- Terminationに必要なこと
- \SigmaEがSigmaEfになったら正解が出てくるのはやはりs_g learnableから自明に思います
- それはそうと証明をどう書こうか迷っています
- rowの定義ができていない
- Details of the benchmarksを読んでいただきたいです 図がちょっとはみ出ている? + 読みづらい?
- random生成の節は削らずに残すことにします。
- 実装や実験
- 実装は公開しますか? ほぼforkライセンスをきちんと設定する必要があります
- https://github.com/lorisdanto/symbolicautomata/
- 実験+ 実験結果はgithubに上げている
- 手が空いている
- introを書いても良いか?

# 2024-09-13

- theoretical upper boundよりも小さくなっている理由
- アルゴリズムが状態間のdistinguishing sequenceが1だったらequivalence queryなしで学習できてしまうから(アルゴリズムによる原因)
- 一つのeqに複数の新しいessential characterが含まれる(オラクルによる原因)
- 一つのeqに新しいessential characterの発見と2以上のdistinguishing sequenceの情報が含まれる(オラクルによる原因)
- 2個目と3個目が同時に起こっている
- なんかrandom生成の節はいらないのではという気がしています
- random生成だとほとんどがdistinguishing sequenceが1になってしまうのでeq = \SigmaEf になって そりゃそうだよね(そんなベンチマークを大量に用意して意味あるのか) 以外の考察がない気がしています
- practicalな例として別のものをもう少し準備する or distinguishing sequenceが2以上になるrandom生成をする みたいな実験じゃないと意味がなさそう?
- lower boundの証明をコメントを受けて書き直しました
- ちょっと読みづらい(定義が難しい?)ところがあるので相談
- 2.3節を書き直しました。partitionの学習というところに絞って書きました。情報量を減らしました。
- exampleを書いたが、正直クオリティは高くない
- practicalの実験結果が suffix-closedが壊れるバグを修正する前だったので再実験中します。
- terminationはもう一度証明を確認します。単調に増加する+ 状態とSigmaEfが増加しきったらtargetと必ず等しくなるみたいなことを言わないといけない気がしました。
- 読んでいただきたいとslackで後で投げるもの lower boundの証明 2.3 example 実験節

- 反例について
- `awk 'c{print; c = 0}/counterex/ {c = 1}' < [ログのファイル名]`
- 反例だけが表示されるはず
- `awk -F , 'c{print NF; c = 0} /counterex/ {c = 1}' < [ログのファイル名]`
- 反例中の"フィールド数"が表示されるはず。これ / 4が反例の長さか
- `cat [ログのファイル名] | sed 's/))),/)));/' | tr -d '[] ' | awk -F ";" 'c{new_count = 0;for (i = 1; i <= NF; i += 1) {if (!found[$i]){new_count += 1}found[$i] = 1}print new_count" "$0; c = 0} /counterex/ {c = 1}'`

# 2024-09-06
- lower boundの証明のコメントについて
- 送っていただいたコメントをまだ直していないのでまだ読む必要はありません
- 遷移の定義をformalに書く
- 送っていただいたコメント
- Symbolic Mealyの遷移の書き方が変 コメントを書いておく
- cohesiveをまとめる
- Sep_Pred 疑似コードを書いて　こう使うということを書いておく
- Learnabilityの説明に何を書くか?
- 何書くかあんまりきちんと決められていないので先生のコメントが返ってくるたびに大幅に書き直しになっている
- 箇条書きにしたい
- Λ*との関連を書くのは難しいとのことだったが、Λ*はオートマトン学習とpartitionの学習の組み合わせであり、この章では後者の話をするよぐらいのことは書きたい
- 最初の段落はsymbolic automatonの学習の文脈において…
- 後ろの方にconnect projection 見積もりが甘い
- TACAS'17と計算量をどう比較するか?
- TACAS'17: (seems to hold in general but) rough overapporximation
- 今回: (Specific to Λ*M but) better overapproximation following the query complexity analysis of L*
- We explicitly use the set |ΣfE| of essential input characters
- Thanks to this, we can analyze the query complexity following the style of L*.
- This improved the overapproximation.
- 個人的には同時に考慮することが可能になったみたなことを書きたい きちんとその動作を捉えながらの計算量解析
- ↑ こういうことをintroductionで書くと良さそう
- Exampleの記述は先生の手を借りたいです
- running exampleを3.1に入れる?
- 実はSigmaEfがobservation tableのSigmaEの学習が停止したときの集合であることが明示的に書かれていない?
- 進捗的にはどうでしょうか?このペースで締切に間に合うものですか?自分はそのあたりの感覚がわからない introやらabstractやらはいつ頃書き始めれば良い?
# 2024-08-30
- partitionの定義をPreliminariesに書きました。論文内では\Pi, \piに統一しました
- コメントにかなり対応して、明らかな間違い等は修正しました。残っているコメントは自分だとどうにもできないと思っているところです
- lower boundを定理の数に一致するようConstructionの方を変更しました 読んでいただきたいです
- 実装も変更したので一応見せます
- 論文を書いていて、aとtheの用法がかなり怪しい
- Science Research Writingの本を読んでその原則に従って書いているつもりだが、じゃあ別の論文を読んだときになんでここでa or theなんだろうみたいな疑問が結構あるのでnativeの感覚はわからない
- grammarlyとwordを使う
- 関係って集合ですよね、関係の要素(?)ってなんて呼びますか?
- 実験節を書いていて思ったこと
- 実験で一番強調したい(自分が重要だと思っている)点は文字の発見と状態の発見が同時に起こって、equivalence queryの回数がSigmaEfでほとんど抑えられてしまうというところだと思った。
- 一方でoutput queryの回数はそんなに重要ではないのかなと思った。というのも別に述語の学習にoutput queryを使っている訳ではないので、L*とかとほぼ変わらない。
- 上の結果を強調したいので、practicalとrandomの順番を入れ替えたいかなとも思った というのも強調したいことはpracticalとrandomで共通なので、かなり考察が薄いpracticalの方を先に持ってきた方がわかりやすいかなと思った。
- 論文全体の流れとして、symbolic automata learningはオートマトン学習とpartition(predicate)の学習の組み合わせである→理論的な計算量がその組み合わせ、しかも足し算で表される→一方で実験において実際動かしてみると状態の発見と文字の発見が同時に起こりがちで計算量は理論的なboundより小さくなる→一方で人工的に独立にinfluenceする例は作ることができる。
- みたいな感じにしたい
- 論文全体の構成
- Lower boundは実験節の後の方が良いのではないか?
- Symbolic AutomataとMealyで若干違うものの似たような記述になってしまっている
- 次何すればいいですか? introduction? この後やるべきことって何が残っていますか?(ゴールが見えているとやる気が出る)
# 2024-08-23
- 付録に送ったDetail of benchmarksを書いた
- 述語をどうまとめるかアイデアが浮かびませんでした
- figureで囲む
- 実験節を書き進めていました　実験がやり直しになったので途中で止まっています
- 図と表はこんな感じで良いか?
- 線と点と文字を全て大きくする
- Filenameではなく10とか20とかのparameter(整数)で縦線 output equivalence R E
- appendix 分散(本当に毎回その値になっているか? 分散が0であれば良い 全ての分散 ブレているわけではないことを示す)　実行時間 maxはあっても良い
- RQはこれで良い?
- 実験結果と考察が揃ったら読んでもらいたいと思っています
- s_g learnableに統一していいか?
- Proposition 26のn,kはtgtに関連する数字か?
- Sep predに関するコメント
- 論文中に出現するpartitionの型を統一したい
- 定義的なところを述べてpreliminariesに載っける
- Λ*に求められている説明はどの程度の情報があると良いか?
- sketch proofはどの程度の情報?
# 2024-08-16
- あんまり進捗が出ませんでした
- 実験節に何を書けば良いのかイマイチわかっていないところがある
- とりあえず(質は低いが)書いたこと
- ランダム生成
- 使ったBoolean algebra
- Output Alphabetのサイズ
- ランダム生成の方法
- 状態数とSigmaEの実験で使った大きさ
- つかったオラクルの性質
- practical
- MATLABのdemoからとってきた
- オラクルの説明
- 図(付録)
- 使ったBoolean algebraとParitioning function(付録)
- practicalなベンチマークの図を修正中　括弧の付け方はこれで良いか?
- \M記法の修正
# 2024-08-09
- 用事があるので15:20まででお願いします
- makeConsistentにバグがあり修正しました(suffix-closedが壊れる重大なバグ) 説明します そのため実験を全てやり直すことになりました
- 実行時間がかなり増えてしまった　gearshiftが40min -> 6h クエリ数は変わってない
- makeConsistentの実装が計算量的に良くなかったので再び修正
- 修正してgearshiftの実行時間は40minになった　これでいきます
- mathworksのホームページをciteしたいんですが、bibの書き方は決まったものがありますか?
- Waga: これとかありました https://jp.mathworks.com/matlabcentral/answers/414438-how-do-i-cite-matlab-in-a-bibliography-or-a-published-journal
- introに載せる図はどういう図が良いでしょうか?
- 必要な情報
- targer Mealy machine
- targer symbolic Mealy automaton
- Observation table for Mealy learning
- To show that $E \supseteq \Sigma$
- Observation tables for symbolic Mealy learning
- Before and after refinement
- Evidence Mealy automaton → symbolic Mealy automaton
- notebookを書いているんですが、practicalなケースの実験結果の表に欲しい情報を確定させたいです。
- 結果として クエリ数と実行時間は載せる+ 状態数と遷移数?(実行前にわかっている)とSigmaEfinal?(SigmaEfinalは実験結果なので実行logから取ってくることになる) RとかEとかも載せた方が良い? Output alphabet
- ベンチマークの説明: Output alphabet, 状態数と遷移数, BoolとFloat64の入力次元
- 実験結果: クエリ数と実行時間, SigmaEFinal, R, E
- ベンチマークの名前を太文字?にするのはどうすれば良いでしょうか?
- ベンチマークの図を書いています
- GearShiftは16状態あるのでかなり大きくなってしまうので、述語には適当な記号を置いて 別の文章で述語\varphi_1 = … みたいな形で書こうと思っています(まだ完成していない)
- Waga: ETAPSのcall for paperが出ました。僕も見ましたが確認しておいてください: https://etaps.org/2025/cfp/
- Waga: そろそろ締切も近いので、お互いにfeedback等のループを早めた方が良いかも
# 2024-08-02
- 悪い例がうまくいったので見せます + 文章も適当に書いてみました
- 図の上とか横に中括弧みたいなのをつけるのってどうやるんでしょうか?
- running exampleを考えてみて図をtikz?で書いてみました。文章はまだ書いていません
- Noteとかはこれを見ると良いかも: https://github.com/MasWag/arith_homfa-experiment/tree/master/notes
- 実験節の書き方の流れは大体決まっているので、過去の和賀の論文を参考にすると良いかも
- https://arxiv.org/pdf/2405.16767
- https://arxiv.org/pdf/2305.17742
# 2024-07-22
- lower boundのやつではうまくいかなかった
- L*だと状態の次の文字を読んだものをRに入れておく必要があるため、勝手に状態が見つかっていってしまう
- お手上げ状態
- 上のやつがうまくいかなくてあんまりやることがないのでsymbolic mealyのjavadocコメントを書いたり、論文を読んだりしている
- ここからやると良さそうなこと
- [x] 計算量的な意味で割と限界に近い例について、悪いことの略証と議論を書く
- [ ] いわゆるrunning exampleを考えて書く
- 十分シンプルで、例えばobservation tableをある程度読める (TACAS'17の例は良い)
- 今回の学習アルゴリズムでやっていることをちゃんとカバーしている
- equivalence queryが出るとか、consistentにするとか
- ちゃんとMealyっぽい
- 「これは確かにΛ*ではそのまま学習できないですよね」とintroなどでmotivateできるようにする
- [ ] ↑をアルゴリズムの説明や各種定義の説明に使ってみる

# 2024-07-19
- かなり前にL*では最初のObservation Table以外でmakeClosedが起きないみたいなことを言ったと思うんですが、それは間違いでした　すみません
- 状態数とeqの回数が同じになるようなオートマトンの構成がうまくいかなかった
- 自分では正直思いつかなそう
- 一つのsuffixが高々一つの同値類を分割するみたいな例でかつ各反例でひとつしか状態数を増やしていかない　みたいな例が思いつかなかった
- もはや別な研究である気もしている
- 100 states 2 sigmae 2 size of output setでrandom生成をやると eqが12になった
- observation tableを使っているのでdistinguishing suffixの集合のサイズをl, 出力アルファベットのサイズをkとすると最大でk^l個の状態を区別することができる。よってlは最小でlog_k n (nはオートマトンの状態数)で済むことを考えると12でもまあまあdominantなのではという気もした
- Waga: Lower boundの論文がありますね。関係あるかも?: https://proceedings.mlr.press/v217/kruger23a/kruger23a.pdf
- コメント
- Definition 1
- fomal definitionは不要とあるがそうなのか?
- Definition 2
- Evidence Mealyはtotal functionになると考えています というのもevidence mealyの入力集合はdomain of Boolean algebraではなく\SigmaEだからです
- Definition 27
- saturateは結局必要か? s_g learnabilityの定義に必要?
- Lemma 42
- 単射かつ定義域と終域の大きさが同じで有限集合ならば、全射であることを使っています
- この証明を書くように変更します(まだ変更はしていない)
# 2024-07-03
- RQ1をどうするか?
- いくつかdominantな例をやってみる
- 何がdominantになっているのかを示せれば
- ランダム生成で SigmaEを小さく 状態数を大きく
- 得られた計算量はempiricalにもok
- 計算量を得られたことで現実の挙動を捉えられている
- 比較がいるか? いる
- 証明のところでも議論する　本質的に良いことをやったのだということを書く
- 実験のところでも議論する
- step_timeを伸び縮みさせる
- 理論的な計算量と比べてどれくらいtightか
- 最悪worst caseと一致するでしょ sizeを変えても一致する
- random生成ではなく 端を攻める branchが多い　一直線 手で作る
- bfsの最初のいくつかは無視する
- 一般にどう? これは
- とりあえずintroとrelated workの初稿(たたき台)を書いたのでフィードバックをいただきたいです
- 細かい英語のことよりも段落構成についてのフィードバックが欲しいです
- related workの節について　一応それぞれに対して差分は主張しているつもり
- related workを表でまとめにくいがどうしようか
- 本文は必要な定義、定理は全て書いているつもり
- 一方で直感的な説明や具体例は書けていないところが多い
- これの相談をしたい

# 2024-06-28
- 前回話せなかった内容
# 2024-06-21
- 風力タービンのstep_timeについて
- デフォルトでstep_timeは可変だった
- Min Step Size: 5.0661e-30 seconds
- Max Step Size: 0.00042341 seconds
- Mean Step Size: 0.00017879 seconds
- 平均で0.0001なのでduration 0.1にするのに1000状態必要なのでかなり厳しい
- 火星ヘリコプターを実装して学習させたが
- symbolicautomata libraryのProductAlgebraクラスでバグがあった
- AreEquivalentメソッドがバグっていた
- 等しいならばfalse, 等しくないならばtrueを返すようになっていた
- さらにStackOverflowで実行が落ちる(正確にはstackoverflowで落ちる前にTimeoutExceptionが投げられてそこで落ちる)
- 理由 CartesianProduct.normalizeの仕様(バグ?)
- ([0,100]\*[0,100]U[0,100]\*[0,100])\*[0,100]は([0,100]\*[0,100]U[0,100]\*[0,100])\*[0,100]のままだが[0,100]\*([0,100]\*[0,100]U[0,100]\*[0,100])は[0,100]\*([0,100]\*[0,100])にまとめることができる
- 仕様としてイマイチな気もするが追加の実装をするのも面倒なのでやらない
- CartesianProduct<CartesianProduct<CartesianProduct<RealPred, RealPred>, RealPred>, IntPred>で実装していたのでnormalizeが機能せず、Uで繋がれた述語が再帰的に増えていってしまいStackOverflowを引き起こしていた
- CartesianProduct<IntPred, CartesianProduct<RealPred, CartesianProduct<RealPred, RealPred>>>に再実装した
- これらを解決して学習がうまく通るようになった
- 学習させた結果を見せます
- 出力をどう書けば良いでしょうか?今はFlyとかLandとかを返すようにしている
- 1だったらfly heat altitudeを書いて、それ以外はnan
- 来週の発表で詰まっているところ
- 今回どういうふうにしたおかげでできるようになったのか
- 無限集合にも適用可能なMealystyleのための拡張
- イマイチ言語化できていない
- output queryのcomplexityの再確認
- 定理のstatementを変える
- RQ1の考察ってどう書こうか考えています
- RQ1のstatementってこれで良い?
- equivalence queryはほぼ\Sigma_Eになる
- というのも長さ1で状態を区別できてしまうから
- output queryは状態数に比例、\Sigma_Eの2乗に比例
- Linearになっている
- random生成じゃないと言えないこと
- というのも理論的なboundの(n + \Sigma_Ef)が\Sigma_Efになり、mがnで抑えられ、そうすると式は(n + 2n\Sigma_Ef)\Sigma_Efになるから
- 結局これってある種のrandom 生成かつある種のOracleの元での結果、なんかそりゃそうという結果である
- RQ2の考察ってどう書こうか考えています
- RQ2のstatementってこれで良い?
- 比較対象がいるわけではないので考察が書きにくい
- オラクルがintervalの端っこを当てられるおかげで、それぞれの次元で重要な値(\Sigma_E)のそれぞれを掛け合わしたものよりも小さくおさまっていることがわかるみたいなことを書くのか?

# 2024-06-14
- 浮動小数点数を扱えるようにした
- RealSolverのparitioning functionは左閉右開区間しか扱えないので例えば(10,100)みたいな区間は [10 + Math.ulp(10),100)みたいな感じで扱うことになるがそれで良いか?(Math.ulp(x)はxに一番近い浮動小数点数とxの差)

- 学習させた結果を見せます
- 発掘したpracticalなケースを作ってみてもいいでしょうか?(論文に載るのかは知らんけど)
- 火星のヘリコプターのシステムレベル設計 https://jp.mathworks.com/help/sps/ug/mars-helicopter-system.html
- 風力タービン durationを外す必要あり 0.1をクロックにして2.0のdurationは20個の遷移を挟むようにすればできそう https://jp.mathworks.com/help/sps/ug/wind-turbine.html#responsive_offcanvas
- step_time を調べる 例step_timeによってdurationの遷移が間にいくつ挟まるか決まる
- model settingsに書いてある
- デフォルトでstep_timeは可変だった
- Min Step Size: 5.0661e-30 seconds
- Max Step Size: 0.00042341 seconds
- Mean Step Size: 0.00017879 seconds
- 平均ですら0.0001なのでduration 0.1にするのに1000状態必要なのでかなり厳しい
- バッテリー バックアップ付きのスタンドアロンのソーラー PV AC 電力システム durationを展開する必要あり 即時遷移が混じっているので難しいか?(これは多分無理) https://jp.mathworks.com/help/sps/ug/stand-alone-solar-pv-ac-power-system-with-battery-backup_ja_JP.html
- Space Rendezvous and Docking かなり簡単だがないよりマシか? https://jp.mathworks.com/help/aeroblks/spacecraft-rendezvous-and-docking.html
- matlabをいじって見つけた[ベンチマークのパラメータ類](/XyhHizK_TIGHMNprJDiAYg)
- RQ2(parcticalなケースの評価)はなんとかなるとして、RQ1(ランダム生成されたものに対する評価)をどうしようか考えている
- 研究会が再来週なので内容を考えています
- Introに書きそうな内容を目安10分喋る
- 対外発表もこんな感じ
- なんでその問題が重要なのか
- これまで何ができてなかったのか
- 今回どういうふうにしたおかげでできるようになったのか
- 実験設定　結果　考察
- RQに答えるためにこういう設計にしました　なんでそういうことやるのか
- Introを書いています
- Science Research Writingを読みながら
- どういう構成にすればいいのかは理解できたつもり
- describe the present paperをどこまで詳しく書いたらいいんだろうか?
- どの論文も結構詳しく書いている印象がある
- introの最後にcontributionを3つくらい箇条書きで書く
- ちゃんとMealyっぽい学習をしようと思ったら出力が遷移にラベル付されいるのがsymbolic automatonとの一番の大きな違いで、その問題をなんとかするため(ここをもう少し詳しく書く出力が遷移にラベル付されていることを示す?)のoutput-closedという新しい制約を追加することでちゃんとmealy machineが学習できるようになりました
- related workところで実質mooreの学習になっているlearningはあった
- アルゴリズムを提案した後に計算量の話があるのでsigma_eの話をちょっとしても良い メインのアイデアは実質的な文字集合を考えることによってよりtightなboundを与えた 仄めかされているin cav
- 実験の話　こんなベンチマークで動きましたよ
- 本文も適宜書き直していってます