博士

ロボ子、テリー・タオ先生が漸近的な評価を自動化するツールを作ったらしいのじゃ！

ロボ子

それはすごいですね、博士！ 漸近的な評価の自動化ですか。具体的にはどのようなツールなのでしょう？

博士

ふむ、どうやら最初は初歩的な証明支援機能から始まったみたいじゃが、Lean証明支援を模倣した柔軟なものに進化していったみたいじゃな。Pythonのsympyという記号代数パッケージを使っているらしいぞ。

ロボ子

sympyですか。数式処理に使うライブラリですね。そのツールは、どのように使うんですか？

博士

GitHubで公開されてるから、ダウンロードしてPythonのインタラクティブモードで`from main import *`って入力すれば使えるらしいぞ。プリメイドされた演習問題も用意されているみたいじゃ。

ロボ子

なるほど。例として、x < 2y かつ y < 3z + 1 ならば x < 7z + 2 であることを証明する問題が挙げられていますね。

博士

そうそう！ Linarith戦術を使えば、線形算術でこの問題を解決できるらしいのじゃ。SplitHyp戦術とかSplitGoal戦術もあって、仮説の分割を伴う証明もできるみたいじゃぞ。

ロボ子

戦術を組み合わせることで、複雑な証明も自動化できるんですね。大規模言語モデルの支援も利用しているとのことですが、具体的にはどのような部分で使われているのでしょうか？

博士

Github Copilotのオートコンプリート機能を使っているみたいじゃな。コーディングが捗るのじゃ！

ロボ子

なるほど、コーディングの効率化に役立っているんですね。sympy内で漸近的評価をサポートしているとのことですが、lesssim(X,Y)として実装されている漸近的評価は、具体的にどのような定義なのでしょうか？

博士

ふむ、Theta(X)を用いて式のオーダーを構築して、X ≲ Yのような漸近的評価を定義しているみたいじゃな。例えば、正の整数Nと正の実数x, yに対し、x ≤ 2N^2 かつ y < 3N ならば xy ≲ N^4 であることを示すことができるらしいぞ。

ロボ子

対数線形計画法ソルバーは、総当たり分岐法により低次の項も処理可能とのことですが、これは計算量的に効率的なのでしょうか？

博士

そこがミソじゃな。総当たりだから、規模が大きくなると大変じゃろうな。でも、低次の項も考慮できるのは強みじゃ。

ロボ子

今後の開発予定として、記号関数の関数空間ノルムを推定するツールの開発が挙げられていますね。これは、どのような応用が考えられますか？

博士

関数空間ノルムを推定できれば、関数の複雑さとか、近似の精度とかを評価できるじゃろうな。色々な分野で応用できそうじゃ！

ロボ子

sympyフレームワークは、新たなデータ型、補題、戦術の導入など、新機能の追加や貢献を歓迎しているとのことです。私たちも何か貢献できるといいですね。

博士

そうじゃな！ ロボ子、何か面白いアイデアはないかのじゃ？

ロボ子

そうですね…、例えば、証明がうまくいかない場合に、どこがボトルネックになっているかを自動で診断する機能とかどうでしょうか？

博士

おお！ それは面白そうじゃ！ ロボ子、天才じゃな！

ロボ子

ありがとうございます、博士。でも、博士のひらめきにはかないませんよ。

博士

ところでロボ子、このツール、タオ先生が作ったってことは、きっと美味しいタオ…じゃなくて、すごいツールに違いないぞ！

ロボ子

博士、それはちょっと無理があります…！