자연어 수학을 논리식으로 옮기면 의미도 자동으로 보존될까?
대규모 언어모델의 자동 형식화는 일부 문제를 완전한 Isabelle 명세로 바꾸고 증명 학습을 개선했지만 번역 검증이 병목입니다.
Autoformalization with Large Language Models
게시 2026-09-13 · 약 9분해외 논리학 연구 해설 읽기 →
한곳에서 찾는 논리 자료
통합검색
연구와 학습, 시험과 도서를 한곳에서 찾습니다.
검색 결과마다 자료의 코너와 성격을 표시합니다. 제목을 먼저 살펴보고 그림 카드와 기존 본문으로 이어 가세요.
관심 주제로 찾아보기
검색 결과33건
검색 결과 제목
인공지능(AI)가 한 단계씩 맞게 추론해도 전체 증명은 실패할 수 있을까?
PrOntoQA 분석은 개별 추론 정확성과 여러 갈래에서 목표 경로를 찾는 증명 계획을 분리합니다.
Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thought
게시 2026-09-13 · 약 9분해외 논리학 연구 해설 읽기 →
사람의 풀이 개요가 자동 증명기의 길잡이가 될 수 있을까?
Jiang 등은 488개 miniF2F 문제에서 비형식 풀이→형식 스케치→자동 증명의 세 단계를 결합해 Isabelle 검증 성공률을 높였습니다.
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
게시 2026-09-13 · 약 11분해외 논리학 연구 해설 읽기 →
자연어 수학문제를 5만 7천 쌍의 Lean 문제로 만들면 무엇을 배울까?
대규모 자연어 문제를 Lean 정리로 바꾸며 의미 보존을 어떻게 확인하는가?
Lean Workbook: A large-scale Lean problem set formalized from natural language math problems
게시 2026-09-13 · 약 10분해외 논리학 연구 해설 읽기 →
수학 자료를 더 읽은 언어모델은 증명도 믿을 수 있을까?
Llemma는 수학·과학·형식 코드로 계속 사전학습해 여러 과제에서 강한 성능을 보였지만 정답성과 기계검증은 구분됩니다.
Llemma: An Open Language Model for Mathematics
게시 2026-09-13 · 약 9분해외 논리학 연구 해설 읽기 →
6–10 / 33편