Conversation

Notices

1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Tuesday, 26-Jan-2021 12:26:10 JST きゅーけー

   ACL2、AI と人間の対話という未来のプログラミング体験をしている気がする。

   • sumiyaki likes this.
   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Tuesday, 26-Jan-2021 12:41:23 JST きゅーけー

     in reply to

     ACL2 は定理の証明を自動で探索してくれるんだけど、少し複雑なだけの定理でも普通に失敗する。そこで人間がその定理を ACL2 に解かせるのに必要な補題を考えたり、証明の方向性をミスっているときは ACL2 にヒントを与えてあげたりするのだ。

     sumiyaki likes this.
   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Tuesday, 26-Jan-2021 12:52:40 JST きゅーけー

     in reply to

     機械が良い感じに簡約したS式を生成して人に見せて、人がS式を読みとって機械にアドバイスをするという循環なんだけど、これはS式でないとかなり厳しいのではないかと思っている。