Kazuki Okamoto kakkun61

結城浩

こんにちは。今後、GPT-4を使ったアプリケーションやサービスがたくさん登場してくると思います。その中には、たとえばSNSを利用したbotもたくさん出てくるでしょう（現在でもすでにありますけれど）。そこで質問なんですが、SNSでおしゃべりしている相手が、人間なのか、GPT-4などの技術を使ったAIなのかを識別するにはどのような会話をしてみればいいでしょうか。一般的なAIでは難しいかもしれないので、GPT-4に限ってもいいです。あなたの考えを聞かせてください。

ChatGPT Model: GPT-4

GPT-4のような高度なAIと人間を識別するのは、時に難しいことがあります。しかし、いくつかの方法を試してみることで、相手が人間かAIかを見極めることができるかもしれません。

複雑な感情やニュアンスについて尋ねる: AIは感情やニュアンスを理解するのが苦手です。複雑な感情を表現する文章やシチュエーションについて尋ねてみて、その反応を見てください。

並置による関数適用

並置による関数適用の善し悪しについて盛り上っているので、自分の意見を表明しておく。以下の2本立て。

純粋に構文論的な議論 (構文拡張の余地を残す)
意味論との関係での議論 (副作用の表示)

先に結論だけ書くと、私はどちらかといえば括弧による関数適用のほうが好みです。

そもそも並置による関数適用とは

Getting Started on the M5Stack Core2

This is a short guide to getting the M5Stack Core2 running on MacOS Catalina.

Setting Up the Environment

The following commands get us set up with arduino-cli

brew install arduino-cli

名古屋モデル検査勉強会 #2

前回の勉強会では Promela の文法要素と基本的な SPIN の使い方を眺めたので、今回は LTL 式を用いた性質検査およびハンズオンを行う。

LTL 式による検査

LTL 式の構文

SPIN の LTL は命題論理の拡張となっており、各論理式の真偽が状態に依存する。

λ式とクロージャ

手続きと閉包

前提

ここでは手続きまたは関数ともに純粋なものを扱う。

関数は渡される引数が同じであれば常に同じ値を返す
関数は変動する外部の変数を参照しない
関数には副作用がない

go 1.1 scheduler

where

src/pkg/runtime proc.c asm_*.s

	{-# LANGUAGE DataKinds #-}

	-- \| My database API.

	module DBAPI where

	import Data.Defaults

	data ConnSpec p = ConnSpec
	{ username :: !(Required p String)

	module WhatIsInstance where

	data Hoge = Foo \| Bar

	-- 型aが同値関係を持つということを示す型
	data ThisIsEq a = ThisIsEq { op :: a -> a -> Bool }

	-- 型Hogeが同値関係を持つ証拠となる値
	hogeIsEq :: ThisIsEq Hoge
	hogeIsEq = ThisIsEq go where

	open import Relation.Binary.PropositionalEquality

	-- 存在型
	data ∃ {A : Set} (B : A → Set) : Set where
	_,_ : (x₁ : A) → B x₁ → ∃ \(x : A) → B x

	-- ORの定義
	infixl 8 _∨_
	data _∨_ (P Q : Set) : Set where
	or-introl : P → P ∨ Q

	{-# LANGUAGE GADTs #-}
	{-# LANGUAGE ExplicitForAll #-}
	{-# LANGUAGE ScopedTypeVariables #-}
	{-# LANGUAGE MultiParamTypeClasses #-}
	{-# LANGUAGE FlexibleInstances #-}
	{-# LANGUAGE FunctionalDependencies #-}
	{-# LANGUAGE UndecidableInstances #-}

	module Main where