one of my students who works on program synthesis is playing around with GPT-4 which is actually kind of a great use of AI -- we have an SMT solver to check everything it emits, we would never trust it for a millisecond otherwise
and also, our current synthesis strategy (enumeration) is so painfully boneheaded that even random-ass LLM magic seems like an improvement
John Regehr /
npub15x…e5a5k
2024-02-20 23:12:29
Author Public Key
npub15xjwk4qzx56p5tdsmzsge7m5ahztkp4nzmrmkw2cp324t888rwsswe5a5kPublished at
2024-02-20 23:12:29Event JSON
{
"id": "81a05fa3952772995ec9598e0ae8f0d99cc9647735631e3ff38ac9e98d8457a2",
"pubkey": "a1a4eb540235341a2db0d8a08cfb74edc4bb06b316c7bb39580c55559ce71ba1",
"created_at": 1708470749,
"kind": 1,
"tags": [
[
"proxy",
"https://mastodon.social/users/regehr/statuses/111966339066415874",
"activitypub"
]
],
"content": "one of my students who works on program synthesis is playing around with GPT-4 which is actually kind of a great use of AI -- we have an SMT solver to check everything it emits, we would never trust it for a millisecond otherwise\n\nand also, our current synthesis strategy (enumeration) is so painfully boneheaded that even random-ass LLM magic seems like an improvement",
"sig": "c8db4cc86becc4d3e078dac05416b7efaa58dde5e9b802eb3b9e6cddd6afde7c2391b55cf662597bb58a1c47f5b103aec02c42b0ec6405614e1d7b183a6cd762"
}