Tao Zhexuan은 대규모 모델 증명 도우미인 Lean을 사용하여 자신의 선호도를 보여줍니다.

"올바르게 사용된다면 AI는 2026년까지 수학 연구 및 기타 여러 분야에서 신뢰할 수 있는 공동 저자가 될 것이라고 예측합니다." 수학자 테렌스 타오(Terence Tao)는 이전 블로그에서 말했습니다.

Tao Zhexuan이 이렇게 말하고 해냈습니다.

최근 그는 GPT-4, Copilot, Lean 등의 도구를 사용해 수학적 연구를 진행하고 있으며, AI의 도움을 받아 논문에서 숨겨진 버그도 발견했습니다.

최근 Terence Tao는 Lean4 프로젝트가 단 3주 만에 다항식 Freiman-Ruzsa 추측(PFR) 증명의 공식화를 성공적으로 완료했다고 말했습니다. 동시에 Lean 컴파일러는 추측이 표준 공리를 준수한다고 보고합니다. 이는 컴퓨터와 AI를 활용한 증명의 대성공이며 흥미진진합니다

위 연구에 대한 자세한 내용을 보려면 관심 있는 독자는 "AI를 사용한 Tao Zhexuan의 공식 증명은 무엇입니까?"를 참조할 수 있습니다. PFR 추측의 과거와 현재를 한 글로 이해해보세요.

이를 보고 주의 깊은 독자들은 타오가 수학 연구를 수행할 때 린을 여러 번 언급했을 것입니다. 간단히 말해서 Lean은 수학자들이 정리를 검증하고 사용자가 증명을 작성하고 검증할 수 있도록 돕는 프로그래밍 언어입니다. 원래 Lean과 비교하여 최신 Lean 4 버전은 더 빠른 컴파일러, 향상된 오류 처리, 외부 도구와의 더 나은 통합을 포함하여 많은 최적화가 이루어졌습니다.

린(Lean)은 수학 분야에서 널리 사용됩니다. 대형 모델(LLM)이 인기를 끄는 오늘날, 둘을 결합하는 더 좋은 방법이 있을까요?

누군가가 이미 이를 구현했습니다. 개방형 플랫폼 LeanDojo 팀(LeanDojo의 경우 "AI 대형 모델이 Tao Zhexuan의 문제 해결에 도움이 됩니다. 수학 정리도 증명할 수 있나요? "을 참조하세요.) of the California Institute of Technology 저자는 인간-기계 협업을 통해 100% 정확한 공식 수학적 증명을 제공하는 것을 목표로 LLM 및 인간 상호 작용을 위해 설계된 협업 도구인 Lean Copilot을 출시했습니다.

LeanDojo 팀의 연구가 주로 LLM을 사용하여 정리 증명을 자동화하는 데 중점을 두고 있다는 점은 주목할 가치가 있습니다. 이 시점에서 그들이 출시한 Lean Copilot이 LLM과 관련이 있다는 것을 아는 것은 어렵지 않습니다. 놀라세요.

프로젝트 주소 : https://github.com/lean-dojo/LeanCopilot

본 연구에서는 멋지다는 말과 더불어 매우 멋지다는 뜻도 있어 평가가 여전히 매우 높습니다.

Lean에서 LLM을 사용하여 수학적 증명 속도를 높이세요

자동화된 정리 증명은 항상 많은 어려움에 직면해 있습니다. 전통적으로 수학적 증명은 수동 유도에 의존하며 신중한 검증이 필요합니다. 이제 AI의 발전으로 연구자들은 인공 지능을 사용하여 심층 탐구를 수행하기 시작했지만 이 문제는 불가피합니다. 즉, LLM은 때로는 수학과 추론 작업에서 그다지 신뢰할 수 없으며 오류와 환각이 발생하기 쉽습니다.

Lean Copilot의 기능은 사용자가 대규모 언어 모델을 사용하여 Lean에서 교정 프로세스를 자동화하고 증명 합성 속도를 향상시킬 수 있도록 하는 것입니다. 사용자는 필요할 때 원활하게 개입하고 수정하여 기계 지능과 인간 지능 간의 균형 잡힌 협업을 달성할 수도 있습니다.

Lean Copilot을 사용하면 LLM을 Lean에서 사용하여 전략 제안, 전제 및 검색 증명을 포함한 증명 자동화를 달성할 수 있습니다.

사용자는 LeanDojo에서 제공하는 내장 모델을 사용하거나 자신의 모델을 가져올 수 있습니다. 이러한 모델은 로컬(GPU 유무에 관계없이) 또는 클라우드에서 실행할 수 있습니다.

간단히 Lean Copilot은 LLM 프로세스를 도입하여 Lean에서 정리 증명을 향상하고 최적화할 수 있는 유연한 방법을 사용자에게 제공합니다.

Lean Copilot의 주요 기능은 다음과 같이 요약할 수 있습니다.

• LLM은 증명 단계를 제안하고, 증명을 검색하고, 대규모 수학 라이브러리에서 유용한 기본정리를 선택할 수 있습니다.
• Lean Copilot은 Lean 패키지로 설정될 수 있으며 Lean의 VS Code 워크플로 내에서 원활하게 실행됩니다.
• 사용자는 LeanDojo에 내장된 모델을 사용하거나 로컬(GPU 유무에 관계없이) 또는 클라우드에서 실행할 수 있는 자체 모델을 사용할 수 있습니다.
• 이 도구는 Linux, macOS, Windows WSL을 포함한 다양한 플랫폼에서 실행됩니다.

Lean 사용자가 LLM에 더 쉽게 접근할 수 있도록 Lean Copilot은 긍정적인 피드백 루프를 시작하기를 희망합니다. 즉, 자동화가 더 나은 데이터로 이어지고 궁극적으로 LLM의 수학적 성능을 향상시킬 수 있음을 입증하는 것입니다.

Copilot 효과 시연

공식 튜토리얼에 따라 Lean Copilot을 구성한 후 실험을 시작할 수 있습니다. 프로젝트 작성자는 참고용으로 몇 가지 공식적인 예도 제공합니다

추천 솔루션. LeanCopilot을 가져온 후 presents_tactics를 사용하여 권장 솔루션을 생성할 수 있습니다. 사용 중 추천 솔루션을 클릭하여 증명에 사용할 수도 있습니다(아래 그림 참조)

simp와 같은 접두사를 사용하여 생성되는 전략을 제한할 수 있습니다

증거를 검색해 보세요. LLM에서 생성된 정책을 aesop(Lean 4의 화이트박스 자동화 프로젝트)와 결합하여 여러 정책 증명을 검색하려면 search_proof를 사용하세요. 증거를 찾으면 전략을 클릭하여 편집기에 삽입할 수 있습니다.

재작성된 내용: 전제를 선택하는 것은 중요한 전략입니다. 이 전략의 목적은 잠재적으로 유용한 건물 목록을 검색하는 것입니다. 현재 Lean Copilot은 LeanDojo의 검색 도구를 사용하여 Lean 및 mathlib4(예: Lean 4 수학 라이브러리)의 고정 스냅샷에서 건물을 선택합니다.

LLM을 실행할 수 있습니다. 정리 증명이든 다른 추론이든 Lean에서 LLM을 실행할 수 있습니다. 모든 모델을 로컬 또는 원격으로 실행할 수 있습니다(자신의 모델 가져오기 참조).

관심 있는 독자는 원본 프로젝트로 이동하여 자세히 알아볼 수 있습니다.

위 내용은 Tao Zhexuan은 대규모 모델 증명 도우미인 Lean을 사용하여 자신의 선호도를 보여줍니다.의 상세 내용입니다. 자세한 내용은 PHP 중국어 웹사이트의 기타 관련 기사를 참조하세요!