동차 Beating 모니터링에 따르면, OpenAI가 차기 주력 모델 Astra를 처음으로 공식 발표했습니다. 내부 버전은 10개의 장기 미해결 수학 및 이론 컴퓨터 과학 문제에서 새로운 결과를 도출했습니다. 이 문제들의 핵심 결론은 최소 10년간 진전이 없었으며, 대부분은 더 오랜 기간 정체 상태였습니다.
그중 일부 문제는 직접 해결되거나 반박되었습니다. Astra는 최초로 비sofic 군을 구성하여 군론의 핵심 미해결 문제에 답했으며, Connes 강성 추측을 반박하고 3개의 Erdős 문제를 해결했습니다. 나머지 성과로는 구체 패킹, 부호 이론, 양자 복잡성 및 양자 후 암호화 관련 문제의 새로운 상하한과 난이도 증명이 포함됩니다.
OpenAI는 모델이 이 10가지 결과를 도출하는 데 사용한 토큰이 Sol API 가격 기준으로 약 2000달러에 해당한다고 밝혔습니다.
이 수학적 논증은 Astra가 생성했습니다. 이후 인간이 논문 정리를 도왔고, 모델은 각 증명을 Lean 인증서로 변환하여 컴퓨터가 단계별로 추론의 타당성을 검증할 수 있게 했습니다. OpenAI는 논문, 증명 인증서 및 모델의 추론 과정을 공개했습니다.