新しいブログ記事: 私が書いたいくつかのふざけたZ3スクリプト
本文の状態
日本語全文を表示中
詳細モードで約2分の本文を読めます。
同じ出来事の情報源
この情報源を基点に整理
Andrej Karpathy 厳選
5ヶ月ぶりのブログ更新で、著者が書いたZ3定理証明器を使ったユーモラスなスクリプトを紹介しています。
Source Article
元記事を日本語で読む
本文に関係しない購読案内、埋め込み通知、サイト内プロモーションは除いています。
新しいブログ記事: 私が書いたいくつかのくだらないZ3スクリプト
『プログラマーのための論理学』に全ての時間を費やさなくなった今、私は再び自分のウェブサイトを更新する時間ができました！ というわけで、5か月ぶりの最初のブログ記事です: 私が書いたいくつかのくだらないZ3スクリプト。
通常であればPatreonのノートへのリンクも載せるのですが、有料コンテンツを公開することは好きではないと判断し、その仕組み全体を終わらせることにしました。 ですので、この投稿に関する簡単なメモをいくつか:
認めざるを得ないのは、この投稿の目的の一部は、最終的にリリースされる『LfP』を盛り上げることです。 本のマーケティングを始めたいのですが、マーケティング資料が面白みのないものになるのは避けたいので、間接的に関連しているが独立したブログ記事は良い出発点です。
この投稿では、「籾殻」の概念、つまり本に収まらなかった膨大な量の素材（コードサンプルと文章の両方）について論じています。 本は約5万語ですが… 籾殻の総量よりもかなり短いのです！ そのほとんどが有益な公開記事に変えられるとは思いませんが、その考えに全く反対しているわけでもありません。 古い章のいくつかは何かに生まれ変われるかもしれませんか？
証明するための条件付き数学的特性を思いつくのは苦労しました。 2つの候補がありました: a == b * c => a / b == c
a != 0 => ある b について: b * a == 1
なぜ配列の例が2を返すのか、さっぱりわかりません。
うまく動作させることができなかった例が一つあり、残念でした。それは、ゴールドバッハ予想をSMT問題としてエンコードすることで、SMTソルバーが決定不能であることを示すデモンストレーションです。 複数のネストされた量化子を持つものは何でも厄介です。
これをウェブでお読みの方は、こちらから購読できます。 更新は週に一度です。 私のメインウェブサイトはこちらです。
私の新しい本『プログラマーのための論理学』は、現在アーリーアクセス中です！ こちらからお求めください。
原文を表示
New Blog Post: Some Silly Z3 Scripts I Wrote
Now that I'm not spending all my time on Logic for Programmers, I have time to update my website again! So here's the first blog post in five months: Some Silly Z3 Scripts I Wrote.
Normally I'd also put a link to the Patreon notes but I've decided I don't like publishing gated content and am going to wind that whole thing down. So some quick notes about this post:
Part of the point is admittedly to hype up the eventual release of LfP. I want to start marketing the book, but don't want the marketing material to be devoid of interest, so tangentially-related-but-independent blog posts are a good place to start.
The post discusses the concept of "chaff", the enormous quantity of material (both code samples and prose) that didn't make it into the book. The book is about 50,000 words… and considerably shorter than the total volume of chaff! I don't think most of it can be turned into useful public posts, but I'm not entirely opposed to the idea. Maybe some of the old chapters could be made into something?
Coming up with a conditioned mathematical property to prove was a struggle. I had two candidates: a == b * c => a / b == c
a != 0 => some b: b * a == 1
I have no idea why the array example returns 2
One example I could not get working, which is unfortunate, was a demonstration of how SMT solvers are undecidable via encoding Goldbach's conjecture as an SMT problem. Anything with multiple nested quantifiers is a pain.
If you're reading this on the web, you can subscribe here. Updates are once a week. My main website is here.
My new book, Logic for Programmers, is now in early access! Get it here.
今日のまとめ
AIデイリーブリーフで今日の重要ニュースをまとめ読み