[일반] 다 닥치고 제미니-알파프루프 통합이나 얘기해볼까

[익명(119.202)]

지금 방식은 형식 증명 언어를 반드시 중간에 거쳐야 되는데

그걸 LLM에 자연스레 통합해서 추론 능력을 늘리거나 최소한 수학 문제는 잘 풀게 할 수가 있는 거임?

[et(evgz6v8f9z)]

그런듯? - dc App

[익명(119.202)]

어떻게 할지 상상이 안되네

[et(evgz6v8f9z)]

수학증명할때 여러 개념에서 증명방향성을 찾아줄듯 남은건 인간이 검토만하면 됨 - dc App

[익명(119.202)]

형식 증명 언어로 작성된 증명을 검증하려면 증명에 사용되는 모든 개념, 정리가 다 이미 정의되어 있어야 하는데 올림피아드는 어느 정도 범위가 정해져 있지만 실제로는 사람이 뭘 물어볼지 전혀 예측할 수 없는데다가 아직 형식 증명 언어로는 표현이 어려운 개념도 많으니깐 극히 제한적일 것 같단 말이지

[et(evgz6v8f9z)]

엄밀성을 구현하는건 agi인거 같음. 막연한 방향만 알면 쉽지 - dc App

[익명(119.202)]

ㄴㄴ 알파프루프는 원리상 '막연한 방향'은 제시 못함. 반대로 '엄밀한 증명'만을 제시 가능한 게 알파프루프임. 모 아니면 도인 거지

[익명(119.202)]

비유하자면 알파고가 "여기에 이 수를 두세요"는 알려줄 수 있어도 "이쪽에 집을 만들고 이쪽을 공격해서 형세를 이렇게 만드는 그림을 그리세요" 하고 알려줄 수는 없는 것과 같은 거임

[et(evgz6v8f9z)]

그럼 더 좋은거네 - dc App

[익명(119.202)]

더 좋은 거라기보단 모 아니면 도인 거지 커버 가능한 범위 내에서는 완벽하나 그 밖에서는 아무 것도 못하는 거니깐

[천사다천사(jjtheman999)]

수학도 잘하는 llm 못참지 - dc App

[천사다천사(jjtheman999)]

솔직히 어떤 방식으로 작동할지 전혀 모르겠지만 그래도 ㄹㅇ 기대된다 - dc App