←back to thread

AlphaProof's Greatest Hits

(rishimehta.xyz)
248 points rishicomplex | 1 comments | 17 Nov 24 17:20 UTC | HN request time: 0.212s | source
Show context
sega_sai ◴[17 Nov 24 22:32 UTC] No.42167962[source]▶
I think the interface of LLM with formalized languages is really the future. Because here you can formally verify every statement and deal with hallucinations.
replies(9): >>42168164 #>>42168732 #>>42168855 #>>42169086 #>>42169255 #>>42169394 #>>42169686 #>>42171742 #>>42176215 #
raincole ◴[17 Nov 24 23:07 UTC] No.42168164[source]▶
It's obviously not the future (outside of mathematics research). The whole LLM boom we've seen in the past two years comes from one single fact: peopel don't need to learn a new language to use it.
replies(2): >>42168180 #>>42168396 #
1. nickpsecurity ◴[17 Nov 24 23:47 UTC] No.42168396[source]▶
Natural language -> Formal Language with LLM-assisted tactics/functions -> traditional tools (eg provers/planners) -> expert-readable outputs -> layperson-readable results.

I can imagine many uses for flows where LLM’s can implement the outer layers above.