문서 둘러보기
HELM 언어 모델 평가
HELM은 언어 모델을 다양한 사용 상황과 여러 지표로 평가하는 프레임워크다. 정확도 외의 특성과 지표 사이의 상충 관계도 함께 드러내는 것을 목표로 제안됐다.
LiveBench
LiveBench는 최근 자료를 바탕으로 질문을 갱신하고 객관적인 정답으로 자동 채점하는 언어 모델 평가다. 시험 자료가 학습에 들어가는 오염 위험과 평가자의 편향을 줄이려는 접근이다.
WildBench
WildBench는 실제 사용자의 어려운 요청으로 언어 모델을 평가하는 프레임워크다. 과제별 점검표와 구조화된 설명으로 응답의 점수와 비교 결과를 판단하도록 구성했다.
InFoBench
InFoBench는 복잡한 지시를 여러 개의 작은 요구로 나눠 언어 모델의 이행 능력을 평가하는 벤치마크다. 개별 요구의 충족 비율을 보는 DRFR 지표를 함께 제안했다.
FollowBench
FollowBench는 지시의 세부 제약을 단계별로 추가해 언어 모델의 조건 이행 능력을 평가하는 벤치마크다. 내용과 상황 및 문체와 형식과 예시라는 다섯 종류의 제약을 다룬다.
IFEval
IFEval은 응답이 검증 가능한 지시를 따랐는지 평가하는 벤치마크다. 주관적인 전체 품질 점수 대신 확인 가능한 조건을 중심으로 재현 가능한 평가를 제안했다.
LLMBar
LLMBar는 언어 모델 평가자가 지시를 제대로 따른 응답을 구별하는지 검사하는 메타 평가 벤치마크다. 내용이 더 매력적으로 보이더라도 지시를 어긴 응답을 가려내는 능력을 다룬다.
RewardBench
RewardBench는 언어 모델의 응답을 평가하는 보상 모델 자체의 능력을 비교하는 벤치마크다. 지시와 선택할 응답 및 배제할 응답의 세 요소로 비교 자료를 구성했다.
길이 제어 AlpacaEval
길이 제어 AlpacaEval은 응답을 길게 쓰는 모델이 유리해지는 자동 평가의 편향을 줄이는 방법이다. 비교할 두 응답의 길이가 같았을 때의 선호를 회귀 모델로 추정한다.
언어 모델 심사자
언어 모델 심사자는 다른 모델이 만든 응답의 품질이나 선호를 언어 모델로 평가하는 접근이다. 정답이 하나로 고정되지 않는 대화 응답의 평가 등에 사용된다.
Prometheus 평가 모델
Prometheus는 사용자가 제시한 세부 채점 기준에 따라 긴 응답을 평가하도록 학습한 언어 모델이다. 참조 답변과 채점표 같은 자료를 함께 사용하는 평가를 연구했다.
G-Eval
G-Eval은 언어 모델의 추론과 구조화된 평가 양식을 활용해 생성 텍스트의 품질을 판단하는 프레임워크다. 요약과 대화 생성에서 사람의 판단과 얼마나 관련되는지 연구했다.
chrF
chrF는 문자 n그램의 일치를 이용해 기계 번역을 평가하는 F점수 기반 지표다. 단어 경계보다 작은 단위에서 번역문과 참조 문장의 겹침을 비교한다.
SacreBLEU
SacreBLEU는 기계 번역 평가의 BLEU 점수를 일관된 조건으로 계산하고 보고하도록 제안된 도구다. 참조 번역의 토큰화와 정규화 차이로 점수가 달라지는 문제를 다룬다.
MAUVE
MAUVE는 모델이 생성한 텍스트와 사람이 쓴 텍스트의 분포 차이를 비교하는 평가 척도다. 열린 형태의 텍스트 생성에서 개별 정답과의 일치 외에 전체적인 생성 분포를 살핀다.
Prism 번역 평가
Prism은 다언어 번역 모델을 제로샷 바꿔쓰기 모델로 활용해 번역 품질을 평가하는 방법이다. 사람의 참조 번역을 조건으로 생성된 번역의 점수를 계산한다.
BERTScore
BERTScore는 문맥 임베딩을 이용해 생성 문장과 참조 문장의 토큰 유사도를 비교하는 자동 평가 지표다. 같은 문자열이 등장하는지만 세는 방식과 달리 문맥 속 표현을 활용한다.
MoverScore
MoverScore는 문맥화된 표현과 Earth Mover Distance를 활용해 생성 텍스트를 참조 텍스트와 비교하는 평가 지표다. 표면적인 형태보다 의미를 반영하는 평가를 목표로 제안됐다.
BLEURT
BLEURT는 사람의 텍스트 품질 판단을 예측하도록 학습하는 BERT 기반 평가 지표다. 많은 합성 예시로 사전 학습해 제한된 사람 평가 자료에 대한 일반화를 돕는 접근이다.
COMET 번역 평가
COMET은 여러 언어의 기계 번역 품질을 평가하는 신경망 모델 학습 프레임워크다. 원문과 목표 언어의 참조 번역을 활용해 사람이 판단하는 품질을 예측한다.
BARTScore
BARTScore는 생성된 텍스트의 평가를 텍스트 생성 문제로 다루는 지표다. 사전 학습한 BART를 이용해 원문과 참조 답변 및 생성 결과 사이의 변환을 평가에 활용한다.
UniEval
UniEval은 생성된 텍스트를 여러 품질 관점에서 평가하는 통합 평가 모델이다. 평가를 예와 아니오로 답하는 질의응답 형태로 바꿔 하나의 모델이 여러 차원을 다루도록 했다.
FactCC
FactCC는 원문과 생성 요약의 사실적 일관성을 판별하는 모델과 연구 자료다. 문장을 규칙으로 변형해 학습 자료를 만들고 근거와 충돌 구간의 식별도 연구했다.
SummaC
SummaC는 요약의 사실적 불일치를 평가하는 데이터셋 모음과 관련 방법을 제시한 연구다. 문장 수준 자연어 추론을 문서 수준 판단에 적용할 때의 단위 차이를 다룬다.
QAFactEval
QAFactEval은 질의응답을 이용해 요약의 사실적 일관성을 평가하는 지표다. 질문 생성과 답변 가능성 판별 등 구성 요소의 선택이 평가 성능에 미치는 영향을 분석했다.
SummEval
SummEval은 요약 모델과 자동 평가 지표를 사람의 판단과 함께 비교한 연구다. 서로 다른 평가 조건을 통일해 요약 평가 방법의 신뢰성을 살펴보려 했다.
BookSum
BookSum은 긴 문학 작품의 서사를 요약하는 능력을 평가하는 데이터셋 모음이다. 사람이 작성한 요약을 문단과 장 및 책 전체의 세 수준으로 제공한다.
Multi-News
Multi-News는 여러 뉴스 기사를 함께 읽고 요약하는 능력을 평가하는 데이터셋이다. 단일 문서 요약과 다른 다중 문서 요약의 학습과 비교를 위해 제안됐다.
GovReport
GovReport는 긴 정부 보고서와 전문가가 작성한 요약을 짝지은 문서 요약 데이터셋이다. 중요한 내용이 문서 전반에 퍼져 있는 긴 입력을 다루는 평가에 사용된다.
QMSum
QMSum은 사용자의 질문에 맞춰 긴 회의록의 관련 부분을 고르고 요약하는 평가 데이터셋이다. 여러 사람과 주제가 등장하는 회의에서 필요한 정보만 정리하는 과제를 다룬다.
InfiniteBench
InfiniteBench는 평균 입력 길이가 10만 토큰을 넘는 과제로 긴 문맥의 이해와 추론을 평가하는 벤치마크다. 영어와 중국어의 합성 과제 및 현실적인 과제를 포함한다.
Lost in the Middle
Lost in the Middle은 긴 입력에서 필요한 정보의 위치가 언어 모델의 성능에 미치는 영향을 분석한 연구다. 문맥의 길이뿐 아니라 정보가 어디에 놓였는지를 함께 평가한다.
LongBench
LongBench는 영어와 중국어의 여러 과제를 통해 언어 모델의 긴 문맥 이해를 평가하는 벤치마크다. 질의응답과 요약 및 코드 완성 등 서로 다른 긴 입력 과제를 통합했다.
RULER
RULER는 입력 길이와 과제 복잡도를 조절해 언어 모델의 긴 문맥 활용 능력을 평가하는 합성 벤치마크다. 단일 정보 검색을 넘어 다중 홉 추적과 집계 과제를 포함한다.
NarrativeQA
NarrativeQA는 책이나 영화 대본의 전체 이야기를 읽고 질문에 답하는 독해 평가다. 문서 전반의 사건과 인물 및 관계를 통합해 이해하는 능력을 다룬다.
QuALITY
QuALITY는 긴 영어 지문을 읽고 객관식 질문에 답하는 독해 데이터셋이다. 전체 지문을 읽은 사람이 질문을 작성하고 검증하는 방식으로 수집했다.
AVeriTeC
AVeriTeC는 실제로 유통된 주장을 웹의 근거와 여러 질문과 답변 단계로 검증하는 데이터셋이다. 근거가 최종 판단으로 어떻게 이어지는지를 설명하는 주석을 제공한다.
QASPER
QASPER는 연구 논문의 전체 본문에서 정보를 찾아 질문에 답하는 평가 데이터셋이다. 제목과 초록만 읽고 만든 질문에 다른 사람이 본문의 근거를 찾아 답하도록 수집했다.
HoVer
HoVer는 여러 문서에서 근거를 모아 주장이 뒷받침되는지 판단하는 사실 검증 데이터셋이다. 최대 네 문서에 걸친 다중 홉 검색과 추론을 다룬다.
VitaminC 사실 검증
VitaminC는 근거에 담긴 작은 사실 변화에 검증 모델이 민감하게 반응하는지 평가하는 데이터셋이다. 표현이 거의 같지만 같은 주장을 뒷받침하는지는 다른 근거 쌍을 활용한다.
FEVER
FEVER는 텍스트 근거를 찾아 주장을 지지하거나 반박하는 능력을 평가하는 데이터셋이다. 판단에 필요한 근거 문장을 찾는 일과 주장의 분류를 함께 다룬다.
SciFact
SciFact는 과학적 주장을 뒷받침하거나 반박하는 연구 초록을 찾고 판단 근거를 식별하는 평가 데이터셋이다. 전문 지식이 담긴 문헌을 검색하고 추론하는 능력을 다룬다.
FinQA
FinQA는 재무 보고서의 정보를 이용해 여러 단계의 수치 추론 질문에 답하는 능력을 평가하는 데이터셋이다. 전문가가 작성한 질문과 답에 추론 프로그램의 주석을 더했다.
TAT-QA
TAT-QA는 재무 보고서의 표와 본문을 함께 읽고 수치 추론으로 답하는 질의응답 데이터셋이다. 서로 다른 형식에서 근거를 고르고 연산을 결합하는 능력을 다룬다.
HybridQA
HybridQA는 표와 연결된 텍스트에서 정보를 함께 모아 질문에 답하는 데이터셋이다. 한 가지 형식의 자료만으로는 풀기 어려운 다중 홉 질의응답을 다룬다.
TabFact
TabFact는 표를 근거로 자연어 문장이 성립하는지 판단하는 사실 검증 데이터셋이다. 언어적 의미 이해와 표의 구조에 대한 기호적 추론을 함께 요구한다.
TAPEX
TAPEX는 SQL 질의와 실행 출력을 합성해 언어 모델이 SQL 실행기의 동작을 학습하도록 하는 표 사전 학습 방법이다. 표 학습 자료의 부족을 실행 가능한 프로그램으로 다룬다.
TURL
TURL은 관계형 웹 표의 문맥 표현을 사전 학습하고 여러 표 이해 과제에 적용하는 프레임워크다. 행과 열의 구조를 반영하는 인코더와 가려진 개체를 복원하는 학습 목표를 제안했다.
TAPAS
TAPAS는 논리 형식을 별도로 생성하지 않고 표의 셀을 선택해 자연어 질문에 답하는 모델이다. 필요할 때 선택한 셀에 집계 연산을 적용하는 방식으로 답을 예측한다.
TaBERT
TaBERT는 자연어 문장과 표 구조의 표현을 함께 학습하는 사전 학습 언어 모델이다. 질문의 문장과 데이터베이스 표를 함께 이해해야 하는 의미 분석 과제를 위해 제안됐다.
Seq2SQL
Seq2SQL은 자연어 질문을 SQL 질의로 변환하는 신경망 모델이다. SQL의 구조를 활용해 출력 공간을 줄이고 질의 실행에서 얻은 보상을 학습에 사용하는 방법을 제안했다.
SParC
SParC는 앞선 질문의 문맥을 이어받아 자연어 질문을 SQL로 바꾸는 능력을 평가하는 데이터셋이다. 질문 시퀀스의 이해와 처음 보는 데이터베이스에 대한 일반화를 함께 다룬다.
CoSQL
CoSQL은 대화로 데이터베이스를 탐색하고 질문을 SQL에 연결하는 시스템을 위한 데이터셋이다. 단일 질문의 변환 외에도 모호한 질문의 확인과 결과 설명을 다룬다.
Spider SQL 평가
Spider는 자연어 질문을 복잡한 SQL 질의로 변환하는 능력을 평가하는 데이터셋이다. 학습 때 보지 못한 데이터베이스 구조와 질의에 일반화하는 능력을 중점적으로 살핀다.
PICARD
PICARD는 언어 모델이 형식 언어를 생성할 때 점진적 파싱으로 허용되지 않는 토큰을 제외하는 디코딩 방법이다. SQL처럼 출력 형식에 제약이 있는 생성 과제에 적용됐다.
RAT-SQL
RAT-SQL은 자연어 질문을 SQL로 바꿀 때 데이터베이스의 관계와 질문 속 언급을 함께 표현하는 모델이다. 처음 보는 데이터베이스 구조에 일반화하는 문제를 다룬다.
LEVER 코드 검증
LEVER는 자연어로 생성한 코드를 실행한 뒤 입력과 프로그램 및 실행 결과를 함께 평가하는 검증기를 학습하는 방법이다. 검증 점수와 생성 확률을 결합해 후보의 순위를 다시 매긴다.
Self-Debugging
Self-Debugging은 언어 모델이 생성한 프로그램의 실행 결과와 자연어 설명을 살펴보며 오류를 찾도록 하는 방법이다. 소수의 시범 예시로 프로그램을 점검하고 수정하는 과정을 제시한다.
CodeRL
CodeRL은 사전 학습한 코드 언어 모델과 강화 학습을 결합하는 프로그램 합성 프레임워크다. 생성 코드의 기능적 정확성을 예측하는 비평기를 학습과 재생성에 활용한다.
CodeT
CodeT는 생성한 테스트 사례로 여러 코드 후보를 실행하고 결과의 일치 관계를 이용해 답을 고르는 방법이다. 코드 후보의 생성과 최종 후보의 선택을 구분해 다룬다.
Magicoder
Magicoder는 공개 코드 조각을 참고해 합성 지시 자료를 만들고 이를 학습한 코드 언어 모델 계열이다. 자료 생성 방법인 OSS-Instruct가 연구의 중심이다.
WizardCoder
WizardCoder는 코드 분야에 맞게 지시를 복잡하게 발전시키는 Code Evol-Instruct로 학습한 코드 언어 모델 계열이다. 원시 코드의 사전 학습에 지시 미세 조정을 더하는 접근이다.
SelfCodeAlign
SelfCodeAlign은 코드 언어 모델이 직접 만든 과제와 답을 실행 검사로 선별해 지시 조정에 사용하는 방법이다. 데이터 생성 과정에서 같은 기반 모델을 활용하는 파이프라인을 제안했다.
OctoPack
OctoPack은 Git 커밋의 코드 변경과 사람이 작성한 지시의 관계를 활용해 코드 언어 모델을 지시 조정하는 연구다. 자연스럽게 쌓인 개발 이력을 학습 자료로 사용하는 접근을 다룬다.
Granite Code
Granite Code는 코드 생성과 수정 및 설명 같은 작업을 위해 제안된 디코더 전용 언어 모델 계열이다. 2024년 연구는 여러 규모의 모델과 다양한 프로그래밍 언어의 학습 자료를 다뤘다.
GReduce
GReduce는 입력 생성기의 실행 경로를 줄여 버그를 재현하는 작은 입력을 찾는 델타 디버깅 방법이다. 입력을 줄이는 과정에서 필요한 유효성 조건을 유지하는 데 초점을 둔다.
OpenCodeInterpreter
OpenCodeInterpreter는 코드 생성과 실행 및 반복 수정을 결합한 코드 시스템 계열이다. 실행 결과와 피드백을 활용해 처음 생성한 프로그램을 개선하는 과정을 다룬다.
PACT 증명 학습
PACT는 형식 증명의 내부 표현에서 자기 지도 학습 자료를 추출해 증명 전술 예측과 함께 학습하는 방법이다. 사람이 작성한 전술 데이터가 부족한 문제를 다루기 위해 제안됐다.
Self-Discover
Self-Discover는 언어 모델이 과제에 맞는 추론 요소를 선택하고 결합해 명시적인 추론 구조를 만드는 프레임워크다. 답을 생성할 때 따라갈 구조를 먼저 구성한다.
Successive Prompting
Successive Prompting은 복잡한 질문을 간단한 문제로 나누고 해결하는 과정을 반복해 최종 답에 도달하는 방법이다. 질문 분해와 개별 질문에 답하는 학습 신호를 분리한다.
복잡도 기반 프롬프팅
복잡도 기반 프롬프팅은 여러 단계의 추론이 담긴 예시를 선택해 언어 모델에 제시하는 방법이다. 추론 단계가 많은 예시와 생성 결과를 활용하는 기준을 연구했다.
COMBO 질의응답
COMBO는 검색한 문단과 언어 모델이 생성한 문단을 함께 활용하는 개방형 질의응답 방법이다. 두 종류의 문맥이 서로 양립하는지를 고려해 답변에 사용할 조합을 만든다.
Atlas 검색 증강 모델
Atlas는 적은 학습 예시로 지식이 필요한 과제를 익히도록 설계한 검색 증강 언어 모델이다. 답변 생성에 사용하는 외부 문서 색인과 모델의 학습을 함께 연구했다.
FiD
FiD는 여러 검색 문단을 각각 읽은 뒤 디코더에서 정보를 결합해 답을 생성하는 질의응답 모델이다. 이름은 Fusion-in-Decoder의 약칭이다.
RETRO 검색 언어 모델
RETRO는 외부 문서 조각을 검색해 다음 내용을 생성하는 언어 모델이다. 모델의 매개변수와 별도로 큰 텍스트 데이터베이스를 활용하는 구조를 제안했다.
REALM
REALM은 언어 모델의 사전 학습에 지식 검색기를 결합하는 방법이다. 지식을 모델의 매개변수 안에만 저장하는 대신 큰 문서 집합에서 필요한 내용을 찾아 참고하도록 제안됐다.
검색 증강 생성
검색 증강 생성은 언어 모델이 외부에서 검색한 내용을 활용해 출력을 만드는 접근이다. 2020년 RAG 연구는 모델의 매개변수에 담긴 지식과 문서 색인의 지식을 결합하는 생성 모델을 제시했다.
Plan-and-Solve 프롬프팅
Plan-and-Solve 프롬프팅은 먼저 문제의 해결 계획을 세우고 그 계획에 따라 하위 과제를 수행하는 제로샷 추론 방법이다. 단계적인 풀이에서 필요한 단계를 빠뜨리는 오류를 줄이려는 접근으로 제안됐다.
Self-Ask
Self-Ask는 원래 질문에 답하기 전에 필요한 후속 질문을 스스로 만들고 답하는 프롬프팅 방법이다. 개별 사실을 알고도 그 답들을 결합하지 못하는 조합적 추론의 차이를 줄이려는 연구에서 제안됐다.
Decomposed Prompting
Decomposed Prompting은 복잡한 과제를 더 간단한 하위 과제로 나누고 각각의 전용 처리 방식에 맡기는 모듈식 접근이다. 하위 프롬프트를 따로 개선하거나 필요한 부분을 다른 모델과 기호 함수로 바꿀 수 있도록 제안했다.
Least-to-Most 프롬프팅
Least-to-Most 프롬프팅은 복잡한 문제를 쉬운 하위 문제로 나누고 차례로 해결하는 방법이다. 앞서 구한 답을 다음 문제의 풀이에 활용해 예시보다 어려운 문제로 일반화하는 능력을 높이려 했다.
PAL 프로그램 보조 추론
PAL은 언어 모델이 문제를 실행 가능한 프로그램 단계로 바꾸고 인터프리터가 계산을 수행하는 추론 방법이다. 문제의 분해와 실제 계산을 서로 다른 구성 요소에 맡겨 풀이의 정확성을 높이려 했다.
Program of Thoughts
Program of Thoughts는 수치 추론 과정을 프로그램으로 표현하고 계산은 외부 실행기에 맡기는 방법이다. 언어 모델의 추론과 계산을 분리하며 수학 서술형과 금융 질의응답 자료에서 평가했다.
Reflexion
Reflexion은 과제의 피드백을 언어로 정리해 다음 시도의 판단에 활용하는 프레임워크다. 모델의 가중치를 갱신하는 대신 반성 내용을 기억 버퍼에 보관해 시행착오를 다음 수행에 반영한다.
Self-Refine
Self-Refine는 언어 모델이 처음 만든 결과에 스스로 피드백을 주고 반복해서 수정하는 방법이다. 하나의 모델을 생성자와 피드백 제공자 및 수정자로 사용해 추론 시점에 결과를 개선하려고 했다.
ReAct 추론과 행동
ReAct는 언어 모델의 추론과 과제 수행 행동을 번갈아 생성하는 접근이다. 추론으로 계획을 관리하고 행동으로 외부 환경의 정보를 얻어 다음 판단에 반영한다.
Toolformer
Toolformer는 언어 모델이 외부 도구를 언제 어떻게 사용할지 학습하는 연구 모델이다. 호출할 API와 전달 인자, 결과를 이후 예측에 반영하는 방식을 자기 지도 학습으로 익히도록 제안했다.
Graph of Thoughts
Graph of Thoughts는 언어 모델이 만든 정보를 임의의 그래프로 연결하는 추론 프레임워크다. 중간 정보 사이의 의존 관계를 표현해 여러 결과를 결합하거나 피드백을 통해 보완하는 방식을 다룬다.
Tree of Thoughts
Tree of Thoughts는 언어 모델이 여러 중간 풀이를 탐색하고 평가하도록 하는 추론 프레임워크다. 한 경로를 계속 이어 쓰는 대신 필요하면 다른 분기를 살피거나 이전 선택으로 돌아가는 문제 해결을 제안했다.
사고 사슬 프롬프팅
사고 사슬 프롬프팅은 답에 이르는 중간 추론 단계를 예시로 제시해 언어 모델의 문제 해결을 유도하는 방법이다. 최종 답만 보여 주는 예시와 달리 풀이의 전개를 프롬프트에 포함한다.
제로샷 사고 사슬
제로샷 사고 사슬은 풀이 예시 없이 단계적인 추론을 요청해 언어 모델의 문제 해결을 유도하는 방식이다. 과제마다 사람이 만든 소수 예제를 제시하는 조건과 구분해 단순한 프롬프트의 효과를 평가했다.
STaR 추론 학습
STaR는 모델이 생성한 풀이 가운데 정답에 도달한 사례로 다시 학습하는 반복적 추론 학습 방법이다. 적은 수의 풀이 예와 풀이가 없는 큰 질문 자료를 함께 사용해 추론 능력을 높이려 했다.
자기 일관성 디코딩
자기 일관성 디코딩은 여러 추론 경로를 생성하고 그 경로들이 도달한 답을 종합해 선택하는 방법이다. 한 번의 탐욕적 풀이만 따르는 대신 서로 다른 풀이에서 일관되게 나타나는 답을 활용한다.
Minerva 수학 모델
Minerva는 일반 자연어로 사전 학습한 모델을 기술적 내용으로 더 학습한 언어 모델이다. 수학과 과학 및 공학의 정량적 추론 문제를 외부 도구 없이 해결하는 능력을 연구했다.
수학 추론의 과정 감독
수학 추론의 과정 감독은 최종 답뿐 아니라 풀이의 중간 단계마다 피드백을 주는 학습 방식이다. 결과만 평가하는 감독과 비교해 논리적 오류를 줄이고 더 신뢰할 수 있는 풀이를 학습하려는 접근이다.
DeepSeekMath
DeepSeekMath는 코드 기반 모델에 수학 자료의 추가 학습과 강화 학습을 적용한 수학 추론 모델이다. 웹 자료 선택과 그룹 상대 정책 최적화를 주요 요소로 제시하며 여러 풀이 후보를 쓰는 조건도 따로 평가했다.
Llemma
Llemma는 Code Llama를 수학 자료로 추가 사전 학습한 언어 모델이다. 논문과 수학 웹 자료 및 수학 코드를 섞은 Proof-Pile-2를 이용해 수학 문제 해결과 형식 증명 능력을 연구했다.
GPT-f
GPT-f는 Transformer 언어 모델을 자동 정리 증명에 적용한 연구 시스템이다. Metamath 형식 언어를 대상으로 수학적 표현을 생성하는 능력이 증명 탐색에 도움이 되는지 살폈다.
HyperTree Proof Search
HyperTree Proof Search는 신경망 기반 정리 증명을 위한 탐색 알고리즘이다. 관련 연구는 이전 증명 탐색에서 얻은 결과를 온라인으로 학습하는 절차와 결합해 새로운 정리에 대한 증명 능력을 높이려 했다.
GamePad 증명 환경
GamePad는 Coq 증명 도구에서 기계 학습 기반 정리 증명을 연구하기 위한 환경이다. 사람이 단계적으로 만든 증명을 활용해 다음 증명 단계와 남은 단계 수를 예측하는 과제를 다뤘다.