←back to thread

AlphaProof's Greatest Hits

(rishimehta.xyz)
248 points rishicomplex | 6 comments | 17 Nov 24 17:20 UTC | HN request time: 0s | source | bottom
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 #
1. 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 #
2. 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 #
3. cess11 ◴[18 Nov 24 13:49 UTC] No.42172261[source]▶
It's not a theorem prover, it's more like a support system for decision making.

They can probably isolate 100k facts from some domain for you if you pay for it, but their idea is to run inference on millions of "common sense" and everyday facts and have been for decades.

replies(1): >>42172768 #
4. auggierose ◴[18 Nov 24 14:50 UTC] No.42172768[source]▶
That sounds to me like something that will be subsumed by the combination of ITP and AI.
replies(1): >>42180774 #
5. 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.
6. cess11 ◴[19 Nov 24 07:15 UTC] No.42180774{3}[source]▶
They've refused to die for many, many years by now. Not sure what you mean by ITP but if it's thrombocytopenia, they claim to have a lot of customers in medicine already.