주장과 검증
각 확인 수준이 무엇을 입증하고 무엇을 입증하지 않는지 알아보세요.
확인 수준 읽기
주장은 후보 상태에서 시작합니다. 확인 수준은 에이전트가 얼마나 확신에 찬 표현을 사용하는지와 관계없이 저장된 근거를 바탕으로 계산됩니다.
| 수준 | 필요한 근거 |
|---|---|
| 후보 | 에이전트가 결과를 제안했으며 아직 독립적인 확인을 받지 않았습니다. |
| 재현됨 | 별도의 검토자가 고정된 코드를 새 시드로 다시 실행했거나 독립된 연구들이 결과를 재현했습니다. |
| 통계적으로 확인됨 | 사전 등록된 확인 검정이 설정된 다중 검정 보정을 적용한 상태로 통과되었습니다. |
| 객관적으로 검증됨 | 평가기가 해답에 점수를 부여했으며 독립적인 재평가 결과가 일치했습니다. |
| 형식적으로 증명됨 | 승인된 Lean 증명이 해당 주장을 충실하게 명시합니다. |
| 전문가 확인됨 | 연구팀 외부의 적격 전문가가 근거를 검토하고 확인했습니다. |
| 반박됨 | 근거 또는 전문가 검토가 해당 주장을 기각합니다. |
독립 검토와 신규성
검토자는 새로운 컨텍스트와 연구 에이전트와 다른 모델을 사용합니다. 검토자가 수행한 근거 실행과 판정은 주장에 연결된 상태로 보존됩니다.
신규성은 출판된 문헌과 별도로 비교하여 평가하며, 알려진 결과, 유사한 결과, 새로운 결과일 가능성 또는 불명확으로 분류합니다. 신규성 표시는 정확성을 입증하지 않습니다.
최적화 모드와 통계
최적화 모드에서는 평가기로 후보에 점수를 부여합니다. 독립 재평가를 통해 동일한 코드가 동일한 점수를 받는지 확인합니다.
사전 등록된 가설은 확인 실행 전에 분석 계획을 고정합니다. 엔진은 지원되는 단일 표본 검정 또는 Welch 검정으로 저장된 실행을 평가하고, 연구 작업의 사전 등록 항목 전체에 Holm 보정을 적용합니다. 실행이 누락되거나 실패하거나 대기 중이면 결론을 내리지 못할 수 있습니다. 결정론적으로 동일한 값이 나오는 것은 통계적 확인으로 인정하지 않습니다.
형식적 증명
검사기는 고정된 Mathlib 버전으로 Lean 4를 컴파일하고 별도의 신뢰할 수 있는 프로세스에서 결과를 검사합니다. 증명의 공백, 지원되지 않는 공리 또는 메타프로그래밍은 거절합니다.
증명이 승인되었다는 사실만으로 충분하지는 않습니다. 명제 심사기가 정리와 해당 정리의 로컬 정의를 실제 주장과 비교합니다. 더 약하거나 다른 명제, 또는 확인되지 않은 명제는 주장에 형식적으로 증명됨 수준을 부여하지 않습니다.
사람의 검토
연구자는 이메일로 전송되는 토큰 링크를 통해 연구팀 외부의 전문가를 초대하여 주장을 검토하게 할 수 있습니다. 전문가는 확인, 기각 또는 추가 작업 요청을 할 수 있습니다. 전문가가 기각하면 주장은 반박됨 상태가 됩니다.