As nossas propostas First Proof
Estamos a partilhar as nossas tentativas de prova do First Proof, um desafio de matemática que testa se a IA pode produzir provas verificáveis em problemas específicos de um domínio.
Executámos um modelo interno nos 10 problemas do First Proof(abre numa nova janela), um desafio matemático de nível de investigação concebido para testar se os sistemas de IA conseguem produzir tentativas de prova corretas e verificáveis. Ao contrário da matemática de resposta curta ou ao estilo de competição, estes problemas exigem a construção de argumentos completos em domínios especializados, sendo difícil estabelecer a correção sem a revisão de especialistas. Os autores dos problemas do First Proof são especialistas de renome nas suas respetivas áreas, e pelo menos alguns dos problemas estiveram em aberto durante anos antes de os autores encontrarem soluções. Um departamento académico com uma sobreposição significativa nas áreas temáticas poderia, possivelmente, resolver muitos dos problemas numa semana.
Partilhámos(abre numa nova janela) as nossas tentativas de prova no sábado, 14 de fevereiro de 2026 às 00:00 PT. Com base no feedback de especialistas, acreditamos que pelo menos cinco das tentativas de prova do modelo (problemas 4, 5, 6, 9 e 10) têm uma elevada probabilidade de estarem corretas, e várias outras continuam em análise. Acreditámos inicialmente que a nossa tentativa para o problema 2 estava provavelmente correta. Com base no comentário oficial do First Proof e numa análise adicional da comunidade, acreditamos agora que está incorreta. Estamos gratos pelo envolvimento e aguardamos com expetativa a continuação da análise. O nosso conjunto completo de tentativas de prova pode ser encontrado aqui(abre numa nova janela). A pré-publicação inclui todas as dez tentativas de prova, além de um apêndice recentemente adicionado com padrões e exemplos de prompt que visam simular as nossas interações manuais com os modelos durante o processo.
Acreditamos que a investigação inovadora de fronteira é talvez a forma mais importante de avaliar as capacidades dos modelos de IA da próxima geração. Os benchmarks são úteis, mas podem não incluir algumas das partes mais difíceis da investigação: manter longas cadeias de raciocínio, escolher as abstrações corretas, lidar com a ambiguidade nas formulações dos problemas e produzir argumentos que resistam ao escrutínio de especialistas. Desafios de fronteira como o First Proof ajudam-nos a testar essas capacidades em contextos onde a correção é difícil de verificar e os modos de falha são informativos.
"Estamos atualmente a treinar um novo modelo cujo principal objetivo é aumentar o nível de rigor no seu pensamento, com o objetivo de que o modelo possa pensar continuamente durante muitas horas e manter uma elevada confiança nas suas conclusões. Quando foram anunciados os problemas do First Proof, pareceu ser o banco de ensaio perfeito, por isso, no fim de semana, decidi experimentá-lo. Já foi capaz de resolver dois dos problemas (9 e 10). À medida que foi treinado, tornou-se cada vez mais capaz, acabando por resolver – segundo a nossa estimativa – pelo menos mais três. Ficámos particularmente satisfeitos quando resolveu o problema 6 e, dois dias depois, o problema 4, uma vez que esses problemas eram de domínios familiares a muitos de nós. É incrível ver um modelo a tornar-se cada vez mais inteligente".
– James R. Lee (Investigador da OpenAI, Raciocínio)
Executámos o modelo com supervisão humana limitada. Ao solicitar versões do modelo durante o treino, sugerimos por vezes estratégias de repetição que pareciam promissoras em tentativas anteriores. Para algumas tentativas, pedimos ao modelo que expandisse ou clarificasse partes de uma prova após receber feedback de especialistas, para tornar o raciocínio mais fácil de verificar. Também promovemos a troca de informações entre este modelo e o ChatGPT para verificação, formatação e estilo. Para alguns problemas, apresentamos o melhor de algumas tentativas, selecionado por avaliação humana. Este foi um sprint rápido e o nosso processo não foi tão claro quanto gostaríamos numa avaliação devidamente controlada. Aguardamos com expetativa o debate com os organizadores do First Proof sobre uma experiência e um quadro de avaliação mais rigorosos para futuras iterações.
Este trabalho baseia-se em resultados anteriores de modelos de raciocínio de fronteira em matemática e ciência. Em julho de 2025, atingimos um desempenho ao nível de medalha de ouro(abre numa nova janela) nas Olimpíadas Internacionais de Matemática com um modelo de raciocínio de uso geral (35/42 pontos). Em novembro de 2025, partilhámos "Experiências iniciais para acelerar a ciência com o GPT‑5", um conjunto de estudos de caso em que o GPT‑5 ajudou investigadores a fazer progressos concretos em matemática, física, biologia e outras áreas, juntamente com as limitações que observámos. E, mais recentemente, comunicámos uma colaboração em física onde o GPT‑5.2 propôs uma expressão candidata para uma fórmula de amplitude de gluão, que foi então formalmente provada por um modelo interno e verificada pelos autores.
Aguardamos com expetativa um maior envolvimento com a comunidade sobre a forma de avaliar o raciocínio de nível de investigação, incluindo o feedback de especialistas sobre estas tentativas, e estamos entusiasmados por disponibilizar estas novas capacidades em futuros modelos públicos.
Autor
Continuar a ler
