테렌스 타오(Terence Tao)가 그것을 보고 전문가라고 불렀습니다! Google 및 기타 업체에서는 LLM을 사용하여 정리를 자동으로 증명했으며, 맥락이 더 완전할수록 증명이 더 좋아졌습니다.

Transformer의 스킬 트리가 점점 더 강력해지고 있습니다.

매사추세츠 대학교, Google, 일리노이 대학교 어바나 샴페인(UIUC)의 연구원들은 최근 대규모 언어 모델을 사용하여 완전한 정리 증명을 자동으로 생성하는 목표를 성공적으로 달성한 논문을 발표했습니다.

논문 주소: https://arxiv.org/pdf/2303.04910.pdf

이 작품은 발두르(북유럽 신화에 나오는 토르의 형제)의 이름을 따서 명명되었으며, Transformer는 전체 증명을 생성할 수 있으며 모델에 추가 컨텍스트를 제공할 때 모델의 이전 증명이 향상될 수 있음을 보여줍니다.

본 논문은 2023년 12월 ESEC/FSE(ACM European Joint Conference on Software Engineering and Symposium on Fundamentals of Software Engineering)에서 게재되었으며, 우수 논문상을 수상했습니다.

우리 모두 알고 있듯이 소프트웨어에서 버그는 피할 수 없으며 일반 응용 프로그램이나 웹 사이트에는 큰 문제를 일으키지 않을 수도 있습니다. 그러나 암호화 프로토콜, 의료 기기, 우주 왕복선과 같은 중요한 시스템 뒤에 있는 소프트웨어의 경우 버그가 없는지 확인해야 합니다.

- 일반 코드 검토 및 테스트에서는 이러한 보증을 제공할 수 없으며 공식적인 확인이 필요합니다.

정형 검증을 위해 ScienceDirect에서 제공하는 설명은 다음과 같습니다.

정형 모델을 사용하여 설명된 시스템의 동작이 지정된 속성을 만족하는지 수학적으로 확인하는 프로세스(또한 정형 모델을 사용하여 설명됨)

은 정형 모델을 사용하여 설명된 시스템의 동작이 주어진 속성을 만족하는지 수학적으로 확인하는 프로세스를 말합니다.

간단히 말하면, 수학적 분석 방법을 사용하여 알고리즘 엔진을 통해 모델을 구축하고 테스트할 설계의 상태 공간에 대한 철저한 분석 및 검증을 수행합니다.

공식적인 소프트웨어 검증은 소프트웨어 엔지니어에게 가장 어려운 작업 중 하나입니다. 예를 들어, Coq 대화형 정리 증명으로 검증된 C 컴파일러인 CompCert는 특히 유비쿼터스 GCC 및 LLVM에서 사용되는 유일한 컴파일러입니다.

그러나 수동 공식 검증(교정 작성) 비용은 상당히 큽니다. C 컴파일러의 증명은 컴파일러 코드 자체의 3배 이상입니다.

그래서 정식 검증 자체가 '노동 집약적인' 작업이고, 연구자들도 자동화된 방법을 모색하고 있습니다.

Coq 및 Isabelle과 같은 증명 보조자는 한 번에 하나의 증명 단계를 예측하도록 모델을 훈련하고 모델을 사용하여 가능한 증명 공간을 검색합니다.

이 기사의 Baldur는 이 분야에서 처음으로 대규모 언어 모델의 기능을 도입하고, 자연어 텍스트 및 코드에 대한 교육을 수행하고, 증명을 미세 조정합니다.

Baldur는 완전한 증거를 생성할 수 있습니다. 한 번에 한 단계씩 정리를 진행하는 것이 아니라, 한 번에 정리를 진행합니다.

위 그림에서 볼 수 있듯이 증명 생성 모델의 입력으로 정리문만 사용한 다음 모델에서 증명 시도를 추출하고 Isabelle을 사용하여 증명 검사를 수행합니다.

Isabelle이 오류 없이 증명 시도를 수락하면 증명이 성공한 것입니다. 그렇지 않으면 증명 생성 모델에서 또 다른 증명 시도가 추출됩니다.

Baldur는 6336 Isabelle/HOL 정리 및 그 증명의 벤치마크에서 평가되어 완전한 증명 생성, 복구 및 컨텍스트 추가의 효율성을 경험적으로 보여줍니다.

그리고 이 도구를 Baldur라고 부르는 이유는 아마도 현재 최고의 자동 증명 생성 도구가 Thor라고 불리기 때문일 것입니다.

Thor는 더 높은 증명률(57%)을 가지고 있으며, 가능한 증명 공간을 검색하는 방법과 결합된 작은 언어 모델을 사용하여 증명의 다음 단계를 예측하는 반면 Baldur의 장점은 완전한 증명을 생성하는 능력입니다.

하지만 Thor와 Baldur 두 형제도 함께 일할 수 있으므로 증명률이 66%에 가깝게 높아질 수 있습니다.

자동으로 완전한 증명 생성

Baldur는 Google의 대규모 언어 모델인 Minerva를 기반으로 합니다. Minerva는 수학적 표현이 포함된 과학 논문과 웹페이지에 대해 훈련을 받고 증명과 정리에 대한 데이터를 미세 조정합니다.

Baldur는 증명 결과를 확인하는 정리 증명 조수 Isabelle과 함께 작업할 수 있습니다. 정리문이 주어졌을 때 Baldur는 거의 41%의 시간 동안 완전한 증명을 생성할 수 있었습니다.

Baldur의 성능을 더욱 향상시키기 위해 연구원들은 모델에 추가 상황 정보(예: 다른 정의 또는 이론 문서의 정리 설명)를 제공하여 증명률을 47.5%로 높였습니다.

이는 Baldur가 맥락을 파악하고 이를 사용하여 새로운 올바른 증명을 예측할 수 있다는 것을 의미합니다. 프로그래머가 관련 방법과 코드를 이해할 때 프로그램의 버그를 수정할 가능성이 더 높은 것과 유사합니다.

다음은 예입니다(fun_sum_commute 정리):

이 정리는 형식 증명 아카이브의 다항식이라는 프로젝트에서 나온 것입니다.

수동으로 증명을 작성할 때 두 가지 경우가 구별됩니다: 집합이 유한하거나 유한하지 않음:

따라서 모델의 경우 입력은 정리문이고 대상 출력은 다음과 같습니다. - 서면 증거.

Baldur는 여기서 귀납법의 필요성을 인식하고 Infinite_finite_induct라는 특별한 귀납법을 적용했습니다. 이는 인간이 작성한 증명과 동일한 일반적인 접근 방식을 따르지만 더 간결합니다.

그리고 귀납법이 필요하기 때문에 이자벨이 사용하는 큰 망치로는 기본적으로 이 정리를 증명할 수 없습니다.

Training

증명 생성 모델을 훈련하기 위해 연구원들은 새로운 증명 생성 데이터 세트를 구축했습니다.

기존 데이터세트에는 단일 증명 단계의 예가 포함되어 있으며, 각 훈련 예에는 증명 상태(입력)와 적용할 다음 증명 단계(목표)가 포함되어 있습니다.

단일 증명 단계가 포함된 데이터 세트가 있는 경우 전체 증명을 한 번에 예측하도록 모델을 훈련하려면 여기에서 새 데이터 세트를 생성해야 합니다.

연구원들은 데이터 세트에서 각 정리의 증명 단계를 추출하고 이를 연결하여 원래 증명을 재구성했습니다.

Proof fix

위의 fun_sum_commute를 예로 들면,

Baldur의 첫 번째 생성된 증명 시도가 증명 검사기에서 실패했습니다.

Baldur는 귀납법을 적용하려고 시도했지만 먼저 증명을 두 가지 경우(유한 집합 대 무한 집합)로 나누는 데 실패했습니다. Isabelle은 다음 오류 메시지를 반환합니다.

이러한 문자열에서 증명 복구 훈련 예제를 도출하기 위해 여기서 정리문, 실패한 증명 시도 및 오류 메시지가 입력으로 연결되고 사람이 작성한 올바른 증명이 대상으로 사용됩니다.

위 그림은 학습 데이터 생성 과정을 자세히 보여줍니다.

증명 생성 모델을 사용하여 원래 훈련 세트의 각 질문에 대해 온도가 0인 증명을 샘플링합니다.

교정 도우미를 사용하여 실패한 모든 교정과 해당 오류 메시지를 기록한 다음 새로운 교정 훈련 세트 구축을 진행하세요.

각 원본 훈련 예제에 대해 정리문, 증명 생성 모델에서 생성된 (잘못된) 후보 증명 및 해당 오류 메시지를 연결하여 새 훈련 예제의 입력 시퀀스를 얻습니다.

컨텍스트 추가

정리 문 앞에 이론 파일의 줄을 추가 컨텍스트로 추가합니다. 예를 들어 아래 그림은 다음과 같습니다. Baldur의 컨텍스트가 있는 증명 생성 모델은 이 추가 정보를 활용할 수 있습니다. fun_sum_commute 정리 문에 나타나는 문자열은 이 맥락에서 다시 나타나므로 문자열 주변의 추가 정보는 모델이 더 나은 예측을 하는 데 도움이 될 수 있습니다.

컨텍스트는 진술(정리, 정의, 증명) 또는 자연어 주석이 될 수 있습니다.

LLM의 사용 가능한 입력 길이를 활용하기 위해 연구원들은 먼저 동일한 이론 파일에서 최대 50개의 문장을 추가했습니다.

훈련 중에 이러한 모든 명령문은 먼저 토큰화된 다음 입력 길이에 맞게 시퀀스의 왼쪽이 잘립니다.

위 그림은 컨텍스트 및 컨텍스트 프리 생성 모델에 대한 증명 성공률과 증명 시도 횟수 간의 관계를 보여줍니다. 컨텍스트가 있는 증명 생성 모델이 일반 생성 모델보다 지속적으로 성능이 우수하다는 것을 알 수 있습니다.

위 그래프는 다양한 크기와 온도의 모델에 대한 추론 비용에 대한 검증된 정리의 비율을 보여줍니다.

생성된 모델의 증명 성공률, 8B 모델과 62B 모델의 컨텍스트, 증명 시도 횟수의 관계를 확인할 수 있습니다.

컨텍스트가 있는 62B 모델은 생성 모델이 컨텍스트가 있는 8B 모델보다 성능이 우수하다는 것을 증명합니다.

그러나 저자는 이러한 실험에 드는 비용이 높고 하이퍼 매개변수를 조정할 수 없기 때문에 62B 모델이 최적화되면 더 나은 성능을 발휘할 수 있다고 여기서 강조합니다.

위 내용은 테렌스 타오(Terence Tao)가 그것을 보고 전문가라고 불렀습니다! Google 및 기타 업체에서는 LLM을 사용하여 정리를 자동으로 증명했으며, 맥락이 더 완전할수록 증명이 더 좋아졌습니다.의 상세 내용입니다. 자세한 내용은 PHP 중국어 웹사이트의 기타 관련 기사를 참조하세요!