통합검색

인공지능(AI)가 쓸 만한 정리를 찾으면 증명도 끝난 걸까?

린도조 연구에서 전제 검색, 다음 단계 제안, 형식 검증의 역할을 나눕니다. 증명의 빈칸이 어떻게 드러나는지 살펴봅니다.

LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

조건을 못 맞추는 퍼즐은 인공지능(AI)에게 왜 더 어려울까?

SATBench의 2,100개 문제는 해 찾기와 불가능성 판정 사이의 비대칭을 드러냅니다.

SATBench: Benchmarking LLMs’ Logical Reasoning via Automated Puzzle Generation from SAT Formulas

정리증명 인공지능(AI)를 시험할 ‘환경’은 왜 필요할까?

HOList는 HOL Light의 수학 말뭉치를 기계학습 환경과 벤치마크로 공개해 증명 모델을 같은 조건에서 훈련·재생·검증하도록 했습니다.

HOList: An Environment for Machine Learning of Higher-Order Theorem Proving

문장을 논리식으로 잘 옮기면 인공지능(AI) 추론도 끝난 걸까?

FOLIO는 자연어를 1차 논리로 옮기는 정확성과 실제 결론을 실행하는 정확성이 다를 수 있음을 보여 줍니다.

FOLIO: Natural Language Reasoning with First-Order Logic

인공지능(AI)가 정답을 맞히면 근거 사슬도 맞았을까?

라온 등록 사실과 첫 규칙이 합류해 확인 메일 결론을 만들고, 그 결론과 둘째 규칙이 합류해 입장 가능 결론을 만드는 두 단계 증명 그래프.