Characterizing initial human-AI proof formalization workflows

Resumo Técnico: Caracterização de Fluxos de Trabalho Iniciais de Formalização Humano-IA

Declaração do Problema
Embora a inteligência artificial tenha demonstrado avanços significativos no raciocínio matemático e na prova de teoremas (por exemplo, alcançando medalhas de ouro na Olimpíada Internacional de Matemática e auxiliando em descobertas de pesquisa), permanece uma lacuna crítica na compreensão de como os matemáticos humanos realmente integram essas ferramentas em seus fluxos de trabalho diários. Historicamente, a verificação formal de provas tem sido desafiadora e, embora linguagens formais como Lean, Isabelle e Rocq tenham otimizado a verificação, escrever provas nessas linguagens continua sendo não trivial e muitas vezes não intuitivo. A literatura existente foca amplamente na avaliação de capacidades de IA; este artigo desloca o foco para a interação entre humanos e IA, investigando especificamente como as pessoas preferem delegar agência, quais barreiras percebem e como constroem fluxos de trabalho na prática.

Metodologia
Os autores empregam uma abordagem de métodos mistos compreendendo uma pesquisa qualitativa e um estudo de usuário controlado, conduzido antes da recente ascensão dos sistemas de codificação agênticos.

1. Pesquisa Qualitativa:

   • Participantes: 31 estudantes e pesquisadores de matemática (filtrados por experiência em formalização) recrutados via listas de discussão e redes sociais.
   • Escopo: A pesquisa investigou o uso de IA autorrelatado atual, preferências para integração futura (especificamente em relação à descoberta de provas vs. formalização), barreiras percebidas (confiabilidade, estilo, integração) e melhorias desejadas nas ferramentas.
   • Análise: As respostas foram codificadas através de um processo iterativo de múltiplos autores para identificar temas relativos à agência humano-IA, frustrações com ferramentas e visões de fluxo de trabalho.

2. Estudo de Usuário Controlado:

   • Participantes: 7 participantes (variando de iniciante a usuários avançados de Lean) com pelo menos uma formação de graduação em matemática.
   • Tarefa: Os participantes foram encarregados de formalizar seis problemas matemáticos informais (abrangendo domínios como teoria dos números e topologia) e suas provas no provador de teoremas Lean.
   • Design: Um design intra-sujeitos onde os participantes formalizaram três problemas em uma condição de "sem ferramentas" (humano sozinho) e três problemas em uma condição "assistida por IA" (acesso a qualquer recurso online baseado em IA, incluindo LLMs, busca semântica e ferramentas de autocompletar código). A ordem das condições foi randomizada.
   • Coleta de Dados: Os participantes gravaram suas telas, resultando em mais de 80 horas de dados de interação. Questionários pós-estudo capturaram o uso de ferramentas e estratégias de fluxo de trabalho autorrelatados.
   • Métricas: A métrica primária foi a precisão da formalização (corretude binária do enunciado e da prova) e o tempo de formalização.

Principais Resultados

• Preferências pelo Controle Humano: Os respondentes da pesquisa expressaram preferências heterogêneas, mas um consenso dominante (81,7%) pela manutenção do alto controle humano sobre o processo de descoberta da prova. Embora 70,3% desejassem a automação de aspectos centrais da formalização, apenas 33,3% queriam a automação total de todo o processo. A maioria preferia que a IA auxiliasse com o "trabalho braçal" ou recuperação de lemas enquanto os humanos mantinham a direção estratégica.
• Confiabilidade vs. Uso: Apesar de 73,3% dos usuários de IA expressarem frustração com a falta de confiabilidade das ferramentas, muitos continuaram a usá-las. A principal frustração citada foi a falta de confiabilidade, seguida por questões de integração específica para formalização e correspondência de estilo.
• Eficácia da Assistência de IA: No estudo de usuário, os participantes alcançaram uma precisão de formalização significativamente maior quando usavam ferramentas de IA em comparação com a condição sem ferramentas. Um modelo de efeitos mistos lineares mostrou que o acesso à ferramenta aumentou a probabilidade de uma resposta correta em 0,30 pontos ($p = 0,003$).
• Eficiência de Tempo: A assistência de IA não gerou uma redução estatisticamente significativa no tempo de formalização ($p = 0,797$). A economia de tempo dependeu fortemente do problema específico e dos padrões de uso da ferramenta.
• Adaptação de Fluxo de Trabalho: Os participantes demonstraram alta adaptabilidade, frequentemente construindo fluxos de trabalho de múltiplas ferramentas para compensar as limitações individuais de cada ferramenta.
  • Formalizadores Humanos com Assistência de IA: A maioria dos participantes (5/7) realizou a maior parte da formalização por conta própria, usando a IA para autocompletar, recuperação de lemas ou sugestões de estilo.
  • Formalização por IA com Ajuda Humana: Um participante dependeu fortemente da IA para geração, editando apenas ocasionalmente, embora isso tenha resultado em menores taxas de sucesso (resolvendo apenas 1/6 dos problemas).
  • Fluxos de Trabalho Híbridos: Alguns participantes engajaram-se em alternâncias intrincadas entre ferramentas (por exemplo, usando uma para descoberta de lemas, outra para boilerplate e uma terceira para reescrita de estilo), exemplificando um padrão de "formalização híbrida humano-IA".

Principais Contribuições

• Mudança de Benchmarking para Análise de Fluxo de Trabalho: O artigo vai além da avaliação do desempenho de modelos de IA para caracterizar o lado humano da integração de IA, documentando preferências, barreiras e padrões de uso reais.
• Evidência Empírica de Ganhos de Precisão: Fornece evidência experimental controlada de que, apesar das limitações atuais das ferramentas, o acesso à IA melhora a precisão da formalização para praticantes humanos.
• Caracterização de Fluxos de Trabalho Híbridos: O estudo identifica e categoriza distintos padrões de fluxo de trabalho (ex: liderado por humano vs. liderado por IA vs. híbrido), destacando que os usuários curam ativamente estratégias de múltiplas ferramentas para mitigar problemas de confiabilidade.
• Base para Pesquisas Futuras: Ao realizar o estudo antes da adoção generalizada de sistemas de codificação agênticos autônomos, o artigo oferece um panorama único de como os humanos conectam manualmente ferramentas díspares, fornecendo uma base para entender a evolução da colaboração humano-IA.

Significância e Alegações
Os autores alegam que a integração eficaz da IA depende não meramente das capacidades do modelo, mas de como os humanos se adaptam e orquestram essas ferramentas. O trabalho ressalta que:

1. A Agência Humana é Central: Existe uma preferência forte e persistente entre matemáticos para manter o controle estratégico, usando a IA para tarefas mecânicas em vez de automação total.
2. A Adaptabilidade é a Chave: Usuários desenvolvem naturalmente fluxos de trabalho flexíveis de múltiplas ferramentas para superar a falta de confiabilidade de sistemas de IA individuais.
3. A Avaliação Deve Evoluir: Avaliar a IA na matemática exige ir além de simples métricas de precisão para incluir eficiência de fluxo de trabalho, preferência do usuário e a preservação do estilo e compreensão matemática.

O artigo conclui que, à medida que as ferramentas de IA avançam, compreender esses interações iniciais humano-IA é crucial para projetar sistemas que apoiem, em vez de substituir, o entendimento humano e as relações sociais inerentes à prática matemática. Os autores reconhecem limitações, incluindo o tamanho reduzido da amostra e o foco em formalização em vez de descoberta de provas, chamando para estudos mais sistemáticos e de maior escala em diversas comunidades matemáticas.