「せっかく記号を使った形式手法があるのに自然言語に戻るのか」というツイート - tkgshn

それはそうと、軽量な形式手法たる型システム含む形式手法は記号の世界の中での正気はちゃんと証明してくれるが、人間様が頭を捻って作られた、自然言語で書かれた仕様とやらは一体何の正気を保証してくれるんだろう

[wwolf]

自然言語から形式手法への翻訳がハードルだったんだけど、GPTくんに肩代わりさせることができるならブレイクするかも

[turanukimaru]

形式手法がお客さんやプロダクトオーナの思い込み・勘違いを指摘してくれるなら役に立つんだがな。お客様！条件を指定しない検索は役に立ちません！POも新人が書いたWhere句のないSQLをレビュー通さないで！

[strawberryhunter]

形式手法は人類には早すぎる。これは不変の事実なので、人気コメントでも指摘があるようにAIに翻訳してもらうしかない。翻訳された定義の検証にもAIの補助が無いと人類には無理だと思う。

[shunkeen]

NLUI（自然言語ユーザーインターフェース）として、自然言語の皮をかぶせて形式手法を使えばいいのかもしれない。WolframのChatGPTプラグインとか、外側は自然言語になるけど、核となる計算エンジンは形式手法だろうし。

[atsushifx]

CoQとか興味はあるけど､とっつきにくい感がある。Pamtagruel https://pantagruel-language.com/ もおもしろうそうではあるのだが

[takilog]

「日本語で正しい仕様を書けない」を仮に公理とみなしたとして、形式手法だと何を表現してるんだろう。単にsyntaxの差なのでは？って気もするし

[yuutetu]

数値計算での定理証明を見た時に、「むしろ論理式、数式からなる証明そのものを生成させた方がいいのでは？再検証できるし学びもあるし。」と考えてたけれど、もしかすると実現する日は近いのかもしれない。

[shikiarai]

自然言語を高級言語にコンパイルする、もしくはそのまま実行ファイルにするのはそんなに遠い未来じゃない。なんならその中でも差が出てきて言語マウントが始まる

[tick2tack]

形式手法のことはよくわかってないけど、個人的に静的型付け言語と動的型付け言語の関係なんかをイメージしてる。前者は後者よりも書くべきテストの量が減る

[morimarii]

結局形式言語ってプログラム書くことと同義なんでモデルをプログラミングすることと同義なんではって思う

[eggplantte]

自然言語の曖昧性をどう解決していくかが課題になって形式手法を取り入れて回帰していく未来が見えた。

[fhvbwx]

むしろ形式手法に適した日本語にするべき

[yamada_k]

自然言語も記号、という話ではなかった。

[napsucks]

記号を使った形式手法は動作の幅を狭めて人間の思考の穴や想定外を減らすためのフレームワーク。AIおいといてそいつがこぼれ球を全部拾ってくれるなら自然言語でよかろうというのはわかる。

[pribetch]

Blueprintは重いからとC++で書き直したパターンみたいな

[stracciatella]

どれだけ科学が発展しても、数式で表現できない世界がまだまだたくさんあるという論に似ている。

[Betty999]

ChatGPTは、自然言語を確率で処理してるからこそ、爆速でプログラムを吐き出す。そのプログラムは形式手法に近い存在であると見せかけて、実際のところは、確率に依る自然言語もどきであり、プログラムもどきだよね

[a-kuma3]

UMLですら読めなくて口頭で説明させられてるのが現実だ

[mayumayu_nimolove]

手法は道具と同じでしょ。絵を描く人に何でタブレットがあるのに手書きなんだって言わんだろ。

[ch1248]

形式手法に関して

[gogatsu26]

パワポ原稿みたいな形式で書かれてて読みにくいブログ

[six13]

形式手法。面白い。

[rin51]

形式手法は使ったことないけど、どの現場で使われてるんだろう

[Hiro_macchan]

メモ

[cartman0]

まあプログラムすらいろんな書き方できるよう変わって形式的でなくなっていくからな

[havanap]

自然言語表現を形式言語に変換するのに特化したファインチューニングしたモデルがあったら面白そうかも

[princo_matsuri]

ノンコードだろうが設計することからは逃れられないのだ