News원문 2026년 10월 27일

PaperFormalizer, 논문을 Lean으로 형식 검증하는 저자 참여형 파이프라인 공개

PaperFormalizer: Author-in-the-Loop Autoformalization of Research Papers in Lean

PaperFormalizer는 코딩 에이전트(Claude Code 또는 Codex) 안에서 동작하는 Lean 기반 에이전트 파이프라인으로, 저자가 자신의 논문에서 증명이나 가정의 빈틈을 찾고 메워 Lean으로 검증된 버전을 만들도록 돕는다. 구현은 GitHub 저장소에서 제공되며, 사용자가 공유한 Lean 코드가 포함된 논문은 paperformalizer.org에서 볼 수 있다. 파이프라인은 LaTeX 원고를 입력받아 논문의 명제들을 의존 그래프로 옮기고, 각 명제를 자연어로 충실성, 모호성, 정확성 측면에서 점검한다. 이후 Mathlib, 선택적 도메인 라이브러리, 저자의 개인 도구 모음을 바탕으로 명제를 Lean에서 형식화하고 증명한다. 명제가 두 가지 이상으로 읽힐 여지가 있으면 파이프라인은 멈추고 저자에게 질문하며, 모든 수정안은 자연어와 TeX 기호로 제시되어 저자가 수락, 거절 또는 방향 변경을 선택할 수 있다. 출력물은 주석과 수정이 반영된 논문, 변경 내역 보고서, 그리고 각 선언이 대응하는 명제와 연결된 Lean 코드다. 더 많은 논문이 형식화될수록 저자의 도구 모음이 커지며, 저자는 검증된 논문을 공유해 후속 연구자가 Lean 코드를 재사용하도록 할 수 있다.

PaperFormalizer는 Claude Code 또는 Codex 안에서 실행되고 GitHub 저장소에서 제공되므로, 수학적 증명에 기대는 자신의 논문이나 코드를 Lean으로 검증해 보려는 개발자가 바로 시험해 볼 수 있다.

원문 출처

arXiv cs.AI (인공지능)

원문 보기 ↗

← Today

AI 리서치·논문 더 보기

NewsAI 리서치·논문고급·2026년 6월 8일

Cognition, merge 가능성 평가 벤치마크 FrontierCode 공개에 Opus 4.8도 13.4%

Cognition(Devin 개발사)이 6월 8일 정답 여부를 넘어 '실제로 머지할 코드인가'를 묻는 코딩 벤치마크 FrontierCode를 공개했다. 36개 주력 오픈소스 레포에서 추출한 150개 태스크로 구성되며, 20명 이상의 일급 메인테이너가 태스크당 40시간 넘게 투입해 설계했다. 난이도는 Extended(150)·Main(100)·Diamond(최난 50)로 중첩 구성된다. 채점은 기능 정확성에 더해 회귀 안전성, 스코프 침범(scope creep) 여부, 테스트 품질, 코드베이스 규약 준수까지 평가한다. 고전적 단위 테스트, 에이전트가 작성한 테스트가 망가진 코드에서 실제로 실패하는지 검증하는 역방향 테스트, 파일·diff 경계 검증, LLM 기반 코드 품질 리뷰를 결합한다. 'blocker' 기준을 모두 통과해야 0점을 면한다. 최고 성적은 Claude Opus 4.8로 Diamond 13.4%·Main 34.3%·Extended 51.8%, GPT-5.5는 Diamond 6.3%, Gemini 3.1 Pro는 4.7%에 그쳤다. SWE-Bench Pro 대비 오탐률(false positive)이 81% 낮다.

SWE-bench류 포화 속에서 '테스트만 통과하면 통과'라는 벤치마크의 맹점을 정면으로 겨냥했다 — METR도 고득점 패치가 메인테이너에게 거절되는 현상을 지적해왔다. Diamond 13.4%라는 낮은 천장은 에이전트 코드의 프로덕션 머지 적합성이 마케팅 수치보다 훨씬 뒤처져 있음을 보여준다. 한국 개발팀에는 코딩 에이전트 도입 시 정답률이 아니라 회귀·스코프·리뷰 통과율로 평가 기준을 재설정하라는 실무 지침이다.

Cognition원문

NewsAI 리서치·논문입문·2026년 6월 10일

Grok 5, Q1 데드라인 넘겨 Q2 베타 전망에 6T 파라미터 MoE 루머

xAI의 Grok 5가 2026년 6월 기준으로 여전히 학습 중이며 공식 출시일·스펙은 발표되지 않았다. xAI는 1월 시리즈 E 업데이트에서 학습이 진행 중임을 확인했고, 일론 머스크가 원래 노렸던 Q1 2026 출시 창은 지나갔다. 현재 xAI 공식 X 계정 기준 가장 유력한 시점은 Q2 2026 공개 베타로 좁혀진다. 스펙은 전부 루머 단계지만 일관되게 거론되는 수치는 6조(6T) 파라미터 + MoE 아키텍처로, 사실이라면 공개 발표된 모델 중 최대 규모이자 Grok 4의 약 2배다. 비교 기준으로 Grok 4는 GPQA Diamond 88%, Humanity's Last Exam 25.4%를 기록했다. 요컨대 Grok 5는 '메가스케일 + 지연'이라는 두 키워드로 정리된다 — 발표 규모는 업계 최대급이지만, 출시는 반복적으로 밀리고 있어 실측 벤치마크는 존재하지 않는다.

Grok 5는 '발표 수치'와 '실출시'를 분리해서 봐야 하는 전형적 사례다. 6T 파라미터는 화제성은 크지만 실측 벤치마크가 없는 한 의사결정 근거가 될 수 없다 — LLM 시세·스펙 환각을 경계하는 우리 함정 목록과 같은 맥락이다. 한국 팀에 주는 실무 교훈은 명확하다. 미출시 모델을 로드맵의 전제로 삼지 말 것. Grok 5는 나올 때 다시 평가하면 되고, 지금은 이미 출시된 Gemini 3.1·Command A+·Kimi K2.6으로 의사결정하는 게 합리적이다.

xAI release trackers (NxCode / WaveSpeed)

NewsAI 리서치·논문중급·2025년 9월 20일

에이전틱 RAG 이해하기: 검색에 '추론 루프'를 두르다

전통적 RAG는 질문을 임베딩해 한 번 검색하고 그 결과를 그대로 프롬프트에 붙이는 단방향 파이프라인이다. 문제는 검색 단계가 자주 실패한다는 데 있다. 단순 RAG 파이프라인이 검색에서 상당한 비율로 부정확한 결과를 낸다는 분석이 반복적으로 보고된다. 에이전틱 RAG는 검색 주위에 추론 루프를 두른다. 에이전트가 "정보가 충분한가? 관련 있나? 질의를 다시 짜서 재검색해야 하나?"를 스스로 판단하고, 필요하면 질의를 재구성해 여러 번 검색한다. 그래프 기반 검색, 계층적 검색 인터페이스, 병렬 검증 에이전트로 확장되는 흐름이다. 동시에 정적 지식엔 RAG가 여전히 유효하되, 적응형 어시스턴트에는 컨텍스트 메모리가 점점 더 큰 비중을 차지한다는 관측도 나온다. 한국 개발자에게는 "생성보다 검색이 병목"이라는 현실 인식과, 검색을 에이전트가 능동 제어하도록 설계하라는 실무 지침이 핵심이다.

RAG 실패의 대부분이 생성이 아닌 검색 단계에서 나온다는 점을 짚고, 검색을 에이전트가 제어하는 설계로 옮겨야 하는 이유를 설명한다.

arXiv (Agentic RAG Survey)원문

NewsAI 리서치·논문실전·2026년 1월 1일

MCP, 리눅스 재단 산하 표준으로: 에이전트 연결의 사실상 프로토콜이 되다

Anthropic이 2024년 11월 공개한 모델 컨텍스트 프로토콜(MCP)이 1년 반 만에 AI를 외부 도구·데이터에 연결하는 사실상의 표준으로 자리잡았다. 2025년 12월 Anthropic은 MCP를 리눅스 재단 산하 Agentic AI Foundation에 기증해 벤더 중립·커뮤니티 거버넌스 체제로 전환했고, OpenAI·Google DeepMind·Microsoft가 모두 채택했다. 보도에 따르면 2026년 3월 월간 SDK 다운로드가 9천만 건을 넘었고, 프로덕션 환경의 활성 MCP 서버는 1만 개 이상으로 집계된다. VS Code·Cursor·Claude Code 등 주요 IDE와 클라이언트가 통합을 마쳤다. 한국 개발팀에는 자체 사내 도구·DB·API를 MCP 서버로 한 번 노출하면 여러 AI 클라이언트에서 재사용할 수 있다는 점이 핵심이다. N×M 통합 비용을 N+M으로 줄이는 표준 어댑터 계층이 생긴 셈이다.

사내 시스템을 MCP 서버로 한 번만 노출하면 여러 AI 클라이언트가 공유할 수 있어, 에이전트 통합 비용 구조 자체가 바뀐다.

WorkOS원문

이 브리핑에 대한 Q&A

이 브리핑에 질문하기

이 브리핑에서 궁금한 점이 있다면 먼저 질문을 남겨보세요.

첫 댓글을 남겨보세요.

중요한 AI 소식만, 메일로 받아보세요

매일 쏟아지는 소식 중 꼭 봐야 할 것만 골라 실무 가이드와 함께 보냅니다.

핵심 뉴스 5 · 추천 가이드 3 · 인기 Q&A