La soluzione di OpenAI alle equazioni di Navier–Stokes non corrisponde alla sua verifica Lean.
-
La soluzione di OpenAI alle equazioni di Navier–Stokes non corrisponde alla sua verifica Lean.
Equazione di Navier-Stokes persa nella traduzione: perché la verifica Lean dell'autoformalizzazione dell'IA non garantisce dimostrazioni corrette in linguaggio naturale
https://arxiv.org/abs/2610.08144
Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs
Abstract page for arXiv paper 2610.08144: Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs
arXiv.org (arxiv.org)
-
Sistema ha spostato questa discussione da Mondo
-
M macfranc@poliverso.org ha condiviso questa discussione
I informapirata@mastodon.uno ha condiviso questa discussione
Ciao! Sembra che tu sia interessato a questa conversazione, ma non hai ancora un account.
Stanco di dover scorrere gli stessi post a ogni visita? Quando registri un account, tornerai sempre esattamente dove eri rimasto e potrai scegliere di essere avvisato delle nuove risposte (tramite email o notifica push). Potrai anche salvare segnalibri e votare i post per mostrare il tuo apprezzamento agli altri membri della comunità.
Con il tuo contributo, questo post potrebbe essere ancora migliore 💗
Registrati Accedi
Citiverse è un progetto che si basa su NodeBB ed è federato! | Categorie federate | Chat | 📱 Installa web app o APK | 🧡 Donazioni | Privacy Policy