tradução entre linguagem natural e linguagem formal

[Joao Marcos]

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/

[Francisco Miraglia Neto]

Caro João,

O livro do Kleene, “Mathematical Logic” (John Wiley) nas sessões 14 e 15 do capítulo I tem exemplos e exercícios que achei pertinentes (Applications to ordinary language, p. 58ff e 67ff.) Mas talvez eu esteja chovendo no molhado.

Abraços,

Chico Miraglia 

--
LOGICA-L
Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica <logi...@dimap.ufrn.br>
---
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 logica-l+u...@dimap.ufrn.br.
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.

[Elaine Pimentel]

Oi, João!

Ótima iniciativa!!

Se depois você quiser divulgar os seus achados na página da SBL seria super bem vindo!

Abraços,

Elaine.

[Eduardo Ochs]

Oi João,

acho que 1) o que você está procurando tem muito a ver com o livro do
Ganesalingam, que é de 2013, 2) o pessoal do Lean tem trabalhado muito
pra implementar sintaxes que pareçam com certos modos de organizar
definições e provas em linguagem natural, 3) quem entende mesmo de
Lean aqui é o Adolfo Neto, eu só consegui fazer coisas muito básicas
nele... será que a gente consegue que o Adolfo nos ajude com pitacos e
links? Adolfo, plz?

Meus links:

Mohan Ganesalingam: "The Language of Mathematics"
https://www.springer.com/gp/book/9783642370113

Alguns blog posts sobre o livro do Ganesalingam:
https://gowers.wordpress.com/2013/03/25/an-experiment-concerning-mathematical-writing/
https://gowers.wordpress.com/2013/04/02/a-second-experiment-concerning-mathematical-writing/
https://gowers.wordpress.com/2013/04/14/answers-results-of-polls-and-a-brief-description-of-the-program/

Lean - um formato pra provas com justificativas:
https://lean-lang.org/theorem_proving_in_lean/theorem_proving_in_lean.pdf#page=48

Alguns slides sobre "elaboration":
http://math.andrej.com/asset/data/the-dawn-of-formalized-mathematics.pdf#page=20

  [[]],
    Eduardo

[Adolfo Neto]

Eduardo,

Na verdade estou aprendendo Lean ainda. Meu objetivo é ver Lean como uma ferramenta para a escrita de programas mesmo. Por isso não vi nada ainda nesta direção.

João,

Eu uso o texto A Estrutura de um Argumento com meus alunos.

Não é nada muito avançado.

O link está no Guia de Estudos da Prova 1 na página

http://logicaparacomputacao.github.io

Você recebeu essa mensagem porque está inscrito 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 logica-l+u...@dimap.ufrn.br.

Para acessar essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CADs%2B%2B6jUsgTQcThMJ%2BF9uf77o-2TpnaDX-%3Dor%3DHOoo4LvtFd4g%40mail.gmail.com.

[Vivek Nigam]

Oi Joao,

Se for para engenheiros, vc pode se inspirar no EARS para a escrita de requisitos. 

É basicamente uma linguagem controlada que pode ser traduzida para LTL e usada para a verificação formal e síntese de sistemas.  

Achei a seguinte referência, mas existem muitas outras. 

https://www.researchgate.net/publication/316972696_Just_Formal_Enough_Automated_Analysis_of_EARS_Requirements

Essa metodologia tem sido usada com algum sucesso no desenvolvimento de sistemas críticos. 

My two cents,

Vivek

Para acessar essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CANspyYXmx6Uw8TYNb5ViL7ThEetsMrxHrRymfJ2jpJyMqG9iJA%40mail.gmail.com.

[Marcelo Finger]

--
LOGICA-L
Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica <logi...@dimap.ufrn.br>
---
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 logica-l+u...@dimap.ufrn.br.
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.

--

Marcelo Finger
 Departament of Computer Science, IME-USP   
 http://www.ime.usp.br/~mfinger

 ORCID: https://orcid.org/0000-0002-1391-1175
 ResearcherID: A-4670-2009

Instituto de Matemática e Estatística,

Universidade de São Paulo

Rua do Matão, 1010 - CEP 05508-090 - São Paulo, SP

[Alexandre Rademaker]

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

[Adolfo Neto]

Função?

Você recebeu essa mensagem porque está inscrito 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 logica-l+u...@dimap.ufrn.br.

Para acessar essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAGG7Aw2K%3DBR%3DPN38dAS96of4u6M5EX07O5WyQyTsNa86XWTfpQ%40mail.gmail.com.

[Alexandre Rademaker]

Em Calculus of Constructions seriam… onde não temos a distinção de termos e fórmulas. Um predicado é uma função com domínio em Prop. Mas dúvido que o chatGPT iria responder com esta argumentação se o Marcelo criticar a resposta recebida.

Marcelo, dá uma olhada no artigo do Geoff https://aarinc.org/Newsletters/141-2023-06.html#geoff

Ab.,
Alexandre

> On 16 Nov 2023, at 16:51, Adolfo Neto <adolf...@gmail.com> wrote:
>
> Função?
>
> On Thu, 16 Nov, 2023, 2:35 pm Marcelo Finger, <mfi...@ime.usp.br> wrote:

> <image.png>
>

[Joao Marcos]

--

http://sequiturquodlibet.googlepages.com/

[Juan Carlos Agudelo Agudelo]

Olá Joao,

Um livro que tem bastantes exemplos de tradução entre linguagem natural e linguagem formal é https://dorshon.com/wp-content/uploads/2018/03/Introduction-to-Logic.pdf. Tem versão em espanhol, e acho que também deve alguma versão traduzida ao portugues.

Abs,

Juan Carlos

Você recebeu essa mensagem porque está inscrito 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 logica-l+u...@dimap.ufrn.br.

Para acessar essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LhpK5UTc1RdAJ5g6WZPa%2BJm9XH4DyU9sFSb5jqhXTqmxA%40mail.gmail.com.

[Marcelo Finger]

Engraçado que, para um gerador de linguagem natural, o chatGPT gerou bem em linguagem formal mas teve um desempenho pífio naquilo que supostamente deveria ser sua especialidade.

Explicação padrão: faltam dados ...

[Alexandre Rademaker]

Mas porque acha isso Marcelo? A tradução foi literal, o chatGPT ‘leu’ a fórmula. Não está ruim, o problema é como caracterizar para ele que queríamos uma leitura não literal, mas uma interpretação da fórmula.

[]s
Alexandre

[Marcelo Finger]

Oi Alexandre.

>> o problema é como caracterizar para ele que queríamos uma leitura não literal, mas uma interpretação da fórmula.

Exatamente!  Ele não tem senso comum pra saber que era isso que se desejava.

[]s

[Joao Marcos]

Não é só isso, né?  Mesmo a "leitura em voz alta", pouco _natural', pode ser corrigida pelo próprio ChatGPT se o usuário assim o pedir.  Mas nada justifica ele escrever "para todo cisne x, se x é um cisne..."

[]s, JM

[Alexandre Rademaker]

Verdade João, não prestei a devida atenção. Bem mais sério, mostra como o modelo não sabe nada sobre a semântica da linguagem formal.

Alexandre 

[Alexandre Rademaker]

Suspeito que ele possa ter se confundido com textos que apresentem a formalização com quantificadores generalizados. Então juntou tudo e fez uma grande confusão. 

Alexandre

[Alexandre Rademaker]

Oi Marcos,

Este é um exemplo interessante para discutir com alunos:

% python test.py convert "No one hates everyone.”

[ TOP: h0
INDEX: e2 [ e SF: prop TENSE: pres MOOD: indicative PROG: - PERF: - ]
RELS: < [ person<0:6> LBL: h4 ARG0: x3 [ x PERS: 3 NUM: sg ] ]
[ _no_q<0:6> LBL: h5 ARG0: x3 RSTR: h6 BODY: h7 ]
[ _hate_v_1<7:12> LBL: h1 ARG0: e2 ARG1: x3 ARG2: x8 [ x PERS: 3 NUM: sg ] ]
[ person<13:21> LBL: h9 ARG0: x8 ]
[ every_q<13:21> LBL: h10 ARG0: x8 RSTR: h11 BODY: h12 ] >
HCONS: < h0 qeq h1 h6 qeq h4 h11 qeq h9 > ]

I have 2 solutions
take_equivs init
take_equivs exausted

(0/2) (∀ x8, person x8 → (∀ x3, person x3 → ¬(∃ e2, _hate_v_1 e2 x3 x8)))
(1/2) (∀ x3, person x3 → ¬(∀ x8, person x8 → (∃ e2, _hate_v_1 e2 x3 x8)))

[Valeria de Paiva]

Oi João Marcos,

obrigada por levantar a bola para esse assunto interessantíssimo! e muito obrigada Alexandre por falar do meu trabalho com a Katerina e o Dick

>A Valeria tem um trabalho inspirado no framework do PARC, https://aclanthology.org/W19-3305/. Acho que tem demo online.

Isso! Tem demo online sim,

http://gkrparser.nlitoolkit.de/

onde você pode escrever uma sentença em linguagem natural e ver sua representação logica, usando vários grafos diferentes (pra sintax, pros conceitos em wordnet, pros contextos, pra semântica neo-Davidsoniana).

Mas tudo pra inglês, ne'?

eu adoraria ter alguém que quisesse fazer a versão do sistema em português! se alguém se candidatar, vou ficar super feliz. O sistema no momento usa Java e BERT pra  análise sintáctica.

Eduardo, o sistema do Mohan 'e mais pra linguagem natural (somente) para escrever matemática, não pra falar de coisas como "Vovó viu a uva", que os sistemas que o Alexandre descreveu fazem. Me parece que o João Marcos quer  quaisquer tipos de sentenças, não somente as matemáticas.

o nosso sistema também tem um aspecto legal de não ficar preso ao sistema puramente logico, ele pode usar machine learning totalmente, se a gente preferir. isto e', o sistema e' hibrido, logico-neural.  eu falei  sobre ele em https://www.youtube.com/watch?v=lhQP-I2EBB4&t=53s.

Se alguem se interessar, fique a vontade pra perguntar mais.

abracos

Valeria

--
LOGICA-L
Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica <logi...@dimap.ufrn.br>
---
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 logica-l+u...@dimap.ufrn.br.

Para acessar esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/408935BD-1346-4346-B19C-14B2F261AE1F%40gmail.com.

[Daniel Durante]

Oi João,

Os exercícios dos capítulos 5, 16, 17, 18 e 19 do "Para Todxs: Natal" têm vários desses de tradução. Mas todos do português para a linguagem formal. O Introduction to Logic, do Harry Gensler, tem muitos exercícios de tradução nos dois sentidos, e o livro do Mortari (cap 6, 7) também.

link do Para Todxs:

Saudações,

Daniel.

-----
Departamento de Filosofia - (UFRN)
http://danieldurante.weebly.com

On 16 Nov 2023, at 10:29, Joao Marcos <boto...@gmail.com> wrote:

--
LOGICA-L
Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica <logi...@dimap.ufrn.br>
---
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 logica-l+u...@dimap.ufrn.br.

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.

[Anderson Nakano]

Olá João Marcos, tudo bem?

São exemplos para alunos de filosofia? Há alguns anos eu formalizem em FOL, também para fins pedagógicos, a teoria do tempo de Russell encontrada no capítulo VI do manuscrito Theory of Knowledge de 1913. É provável que contenha alguns erros, mas vou compartilhar, pois pode vir a ser útil...Está neste link aqui:  Formalization - On the experience of time.pdf - Google Drive. Se precisar do arquivo em LaTeX, me escreva que eu disponibilizo para você.

Abraço,

Anderson

[Joao Marcos]

PessoALL:

Agradeço ao Chico M, ao Eduardo O, ao Adolfo N, ao Vivek N, ao Marcelo F, ao Alexandre R, ao Juan Carlos AA, à Valeria dP, ao Daniel DPA, e ao João Nunes dS por todos os ponteiros e indicações de material pedagógico sobre traduções entre linguagem formal e linguagem natural.  Seguirei tomando nota, claro, se chegar algo mais!

Tudo de bom, Joao Marcos

--

http://sequiturquodlibet.googlepages.com/

[Joao Marcos]

> Agradeço ao Chico M, ao Eduardo O, ao Adolfo N, ao Vivek N, ao Marcelo F, ao Alexandre R, ao Juan Carlos AA, à Valeria dP, ao Daniel DPA, e ao João Nunes dS por todos os ponteiros e indicações de material pedagógico sobre traduções entre linguagem formal e linguagem natural. Seguirei tomando nota, claro, se chegar algo mais!

Como toda lista deixa alguém de fora... esqueci-me logo à partida de
incluir o Anderson N nos agradecimentos.

Obrigado, pessoALL!
JMarcos

--
http://sequiturquodlibet.googlepages.com/