Olá João, Eu poderia escrever muito sobre o tema aqui… Vou tentar arriscar alguns ponteiros e se te interessar conversamos mais depois.
Na área de linguistica computacional e NLP (bem, NLP hoje é apenas LLM infelizmente) temos vários nomes para esta tradução: semantic parsing, semantic analysis etc. Os trabalhos de QA onde perguntas em NL são convertidas em SPARQL ou SQL também poderiam ser colocados nesta lista, estou trabalhando na IBM com isso. Também temos a subárea de https://en.wikipedia.org/wiki/Formal_semantics_(natural_language). Algumas referências: Capitulo 19 do https://web.stanford.edu/~jurafsky/slp3/ introduz o assunto, mas nos meus cursos de NLP tento ir um pouco além. Daqui a algumas semanas vou apresentar um artigo sobre transformação de sentenças em NL para HOL. Neste trabalho usamos a gramática computacional em HPSG para o inglês ERG, a representação semântica MRS da Ann Copestake e outras ferramentas do grupo DELPH-IN (https://github.com/delph-in/docs/wiki) com que colaboro. No topo destas ferramentas, desenvolvemos duas bibliotecas em Python: uma implementação de HOL (que vamos apresentar no SMBF) e a tradução de MRS para HOL ("Extracting higher-order logic formulas from English sentences" aceito no ICNLP, se quiser te mando). Estou agora trabalhando na migração dos códigos para Lean. Mas o trabalho que me pareceu mais relevante para seu contexto é Flickinger (2017): ``Generating English Paraphrases from Logic,'' in Martijn Wieling, Gosse Bouma and Gertjan van Noord, eds., "From Semantics to Dialectometry". Springer. Vide http://svn.delph-in.net/erg/trunk/openproof/README. Este projeto foi feito pelo Dan Flickinger em Stanford. O projeto foi feito para apoiar cursos de lógica em Stanford. Semana passada, inspirado pelo texto do Geoff Surcliffe (do TPTP), https://aarinc.org/Newsletters/141-2023-06.html#geoff, comecei a brincar com a formalização automática do puzzle https://www.tptp.org/cgi-bin/SeeTPTP?Category=Problems&Domain=PUZ&File=PUZ001+1.p. A discussão no forum do Lean acabou gerando questões interessantes sobre como a escolha dos axiomas iniciais - nada surpreendentemente - determina o fragmento necessário para prova (construtiva vs clássica), vide https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/'Who.20Killed.20Aunt.20Agatha'.20puzzle. Estou tentando achar tempo para continuar a brincadeira no https://github.com/arademaker/agatha. Este exercício é interessante e mostra como a maior dificuldade não é necessariamente obter representações lógicas a partir de sentenças de NL, mas como adeguar o nível de abstração da representação ao problema em questão. Uma discussão antiga é sobre qual a linguagem lógica mais adequada para NL. E como diz a Ann Copestake em https://delphinqa.ling.washington.edu/t/converting-mrs-output-to-a-logical-form/413/14 “… there is no existing logic which is adequate for all the phenomena of natural language …" Dito isso, gosto dos trabalhos de dependent types para NL, https://ncatlab.org/nlab/show/dependent+type+theoretic+methods+in+natural+language+semantics onde dois nomes são interessantes. Do Aarne Ranta que tem a http://www.grammaticalframework.org/ e Christian Retoré https://scholar.google.com/citations?user=N48HSh4AAAAJ&hl=pt-BR. Embora reconheça que precisamos de algum tipo de default reasoning. Mas existem muitas abordagens para NL to Logic e vice-versa, algumas shallow (e.g. https://github.com/sivareddyg/UDepLambda) e outras mais profundas como as que me interessam e são apresentadas em livros como https://www.amazon.com/Natural-Language-Understanding-James-Allen/dp/0805303340 A Valeria tem um trabalho inspirado no framework do PARC, https://aclanthology.org/W19-3305/. Acho que tem demo online. Outro nome interessante na área é o Johan Bos com alguns projetos como o https://pmb.let.rug.nl/ e https://gmb.let.rug.nl/. Cara muito gente fina. Ele usa Discourse Representation Theory, baseada em FOL e uma alternativa à MRS que uso. O Johan Bos e o Patrick Blackburn (que estava no UNILOG 2015 em Istanbul) tem um outro livro clássico com código prolog (http://www.let.rug.nl/bos/comsem/book1.html) e um artigo bem bacana https://www.jstor.org/stable/23918435 Bom, é o que consigo contar aqui nos 30 minutos que tinha para responder seu email! Mas me avisa se os ponteiros fizerem sentido.. podemos conversar mais. Espero não ter desviado muito da sua questão. Especificamente para uso didático, certamente o projeto do Dan Flickinger e o livro do Johan Bos são os mais relevantes. E como esta área muito me interessa… não deixa de me atualizar com seus progressos! ;-) Ab., Alexandre Rademaker > On 16 Nov 2023, at 10:29, Joao Marcos <[email protected]> wrote: > > PessoALL: > > Por razões pedagógicas, estive buscando por exercícios de _tradução_ > entre "a" linguagem natural (qualquer uma que eu seja capaz de ler) e > linguagens formais de teorias lógicas apropriadas. Também estive > buscando exercícios na direção oposta, isto é, envolvendo _leituras > naturais_ de asserções descritas em linguagens formais. Ambas > categorias de exercícios parecem ser extremamente importantes para os > estudantes curiosos em saber *pra quê serve tudo isso*. > > Agradeço desde já por quaisquer sugestões que vocês puderem > compartilhar comigo de material (de qualquer nível) para a prática > destas tarefas. Tenho interesse particular por materiais que *não* > tratem de teorias matemáticas, mas que, ao invés, envolvam a > formalização de outros fragmentos interessantes da linguagem natural. > Materiais envolvendo _erros_ de tradução, numa direção ou na outra, > são particularmente bem-vindos! > > Caso seja de interesse dos colegas, posso ao final compilar aqui as > referências recebidas, na lista ou fora dela. > > Saudações lógico-naturais, > Joao Marcos > > -- > http://sequiturquodlibet.googlepages.com/ > > -- > LOGICA-L > Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica > <[email protected]> > --- > Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos > Grupos do Google. > Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um > e-mail para [email protected]. > Para acessar esta discussão na web, acesse > https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LgSXODHR0OMA6c-VUELwn3MrhOggxB8LgCoOwrCqJb-og%40mail.gmail.com. -- LOGICA-L Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica <[email protected]> --- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para [email protected]. Para acessar esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CF88BB05-9510-4504-B1A9-DBDAAC880AD4%40gmail.com.
