같은 수학문제를 여러 증명 언어로 옮기면 인공지능(AI) 비교가 더 공정해질까?
PutnamBench는 640개 대학 수학문제를 Lean 4·Isabelle과 일부 Coq로 1,692회 형식화해 언어별 자동증명기의 강점과 난도를 비교했습니다.
PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
개별 글보다 주제 전체를 따라 읽고 싶다면 대표 글과 연관 자료를 함께 보세요.
그림으로 이해하고, 원문으로 깊이 읽습니다.
관심 주제와 난이도로 필요한 글을 찾아보세요. 개념을 익히는 학습과 원문에 근거한 연구 해설을 구분했습니다.

해외 학술 연구의 7개 분야
PutnamBench는 640개 대학 수학문제를 Lean 4·Isabelle과 일부 Coq로 1,692회 형식화해 언어별 자동증명기의 강점과 난도를 비교했습니다.
PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
숙의 대화에서는 최종 권고뿐 아니라 선택지를 제안한 사람도 그 선택지가 가능한지 보일 책임을 질 수 있습니다.
Burdens of Proposing: On the Burden of Proof in Deliberation Dialogues
핀란드 무작위 설문실험은 자기 이익에 반하는 ‘마지못한 출처’가 중립 출처보다 자동으로 신뢰받지 않았음을 보여 줍니다.
The Force of the Argument Source: The Partiality of the Source Influences the Evaluation of Political Arguments
타당화 논증은 관찰에서 채점, 일반화, 실제 수행, 활용 결정으로 넘어가는 근거를 살핍니다. 점수의 정확성과 점수 사용의 정당성을 구별합니다.
A contemporary approach to validity arguments: a practical guide to Kane’s framework
Colquhoun의 계산은 p값과 발견의 사후 오류확률이 다른 양임을 보이며, 사전가능성·검정력·관측 증거를 함께 명시해야 한다고 주장합니다.
An Investigation of the False Discovery Rate and the Misinterpretation of p-values
156–160 / 417묶음