←back to thread

AlphaProof's Greatest Hits

(rishimehta.xyz)
248 points rishicomplex | 2 comments | 17 Nov 24 17:20 UTC | HN request time: 0.396s | 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 #
thesz ◴[18 Nov 24 04:20 UTC] No.42169686[source]▶
So, you looking for Cyc [1], practically.

[1] https://en.wikipedia.org/wiki/Cyc

replies(3): >>42170205 #>>42171090 #>>42172165 #
auggierose ◴[18 Nov 24 06:22 UTC] No.42170205[source]▶
Does Cyc have proofs?
replies(1): >>42171072 #
cess11 ◴[18 Nov 24 09:50 UTC] No.42171072[source]▶
In a sense, yes, since it has a foundation in Prolog style facts and rules, and supposedly can output its reasoning.
replies(1): >>42171103 #
auggierose ◴[18 Nov 24 10:00 UTC] No.42171103[source]▶
Ok, sounds like in principle you could have proofs, but in practice, you don't?

Are there any checks for the consistency of all facts?

replies(1): >>42171126 #
cess11 ◴[18 Nov 24 10:06 UTC] No.42171126[source]▶
How could there be? Gödel gets in the way.
replies(1): >>42171489 #
auggierose ◴[18 Nov 24 11:28 UTC] No.42171489[source]▶
In most interactive theorem provers the check is simple: you single out the axioms you believe, and all other stuff you do is guaranteed to preserve consistency. That works in an ITP system because there are only a few axioms.

If Cyc has 100000 axioms/facts, then that's a problem.

replies(2): >>42172161 #>>42172261 #
1. thesz ◴[18 Nov 24 13:35 UTC] No.42172161[source]▶
If axioms, facts and rules have types, these types can guide choice.
replies(1): >>42172835 #
2. auggierose ◴[18 Nov 24 14:55 UTC] No.42172835[source]▶
Not a believer in types here, sorry. I'd rather have simple theorems instead without wading through a swamp of types first. And I am sure AI will be able to handle theorems just fine.