[🔍후기] AI로 수학증명하기 후기

[익명(orangestar1122)]

https://demo.projectnumina.ai/

Kimina Prover Demo – AI-Powered Proof Validation in Action

문제를 넣어주면 Lean으로 번역하는놈 하나에 푸는놈 하나 붙어서 풀어주고

마지막에 구문검사로 제대로 증명했는지 검증함

수능문제 몇개 넣어봤어요

그대로는 못넣고 제미나이로 영어번역 + "답이 ~임을 증명하시오" 형식으로 바까줘야함

3모 킬러 22번

pass@16 넣어봤지만 개같이 실패

기하를 담당하는 20번

기하는 약할것같다고 예상했고 예상대로 pass@16 실패

나름 생각잘해야하는 15번

Lean으로 나타내기 좋을것같아서 기대했으나 pass@16 실패

계산만 우다다다 해주면되는 4점초반 쉬운문제

pass@16 실패

여기서부터 뭔가 잘못됨을 느낌

같은 4점 초반라인 두개

둘다 실패

내가 뭔가 잘못쓰고있나를 생각하며 3점 개쉬운문제까지 내려옴

성공 하긴했는데

정답률이 엄

한 200트 돌릴생각으로 해야하나? 수학 문항제작할때 검증기정도는 만들수있지않을까 생각했는데

생각보다 더 참담하네요 이걸로 퍼트넘 10문제는 어케푼거지

대학수학은 좀 나을수있음 아마 추상대수쪽...

[ㅇㅇ 1(218.154)]

Lean을 사용하는거라면 번역 단계에서 문제 생겼을 가능성이 높은 거 가튼데

[익명(orangestar1122)]

대충봤을때 번역문제는 없어보였음 쉬운문제들은 읽으면되고 추론이라 thinking 나오는데 문제제대로푸는지 볼수있으니까 그보다 결과에 구문오류나 goal을 다 증명하지 않고 끝내거나 하는게 대부분문제인거같아요

[Protactinium(comic9287)]

퍼트넘은 pass@128 아니었나

[Protactinium(comic9287)]

그리고 수능문제랑 퍼트넘이랑은 결이 좀 다르니

[약팔이아님(vital7966)]

o3는어때

[ㅇㅇ 2(27.115)]

무슨 모델로 푼거임? o1 pro? o3? o4-mini-high?