💻 computer science

Nonlinear Arithmetic with SMTLIB Division is Undecidable

L'article démontre que l'arithmétique réelle non linéaire (NRA) telle que définie dans la norme SMTLIB est indécidable, car son traitement de la division par zéro comme une fonction non interprétée permet le codage de problèmes d'arithmétique entière indécidables.

Auteurs originaux : Dejan Jovanovic

Publié 2026-05-27

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Dejan Jovanovic

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous soyez un détective tentant de résoudre un mystère en utilisant un ensemble de règles très strictes. Dans le monde de l'informatique, ces règles sont appelées des « théories », et elles aident les ordinateurs à déterminer si une énigme mathématique possède une solution ou non.

Ce document traite d'un ensemble spécifique de règles appelé Arithmétique Réelle Non Linéaire (NRA). Considérez cela comme un jeu joué avec des nombres réels (comme 3,14, -5 ou 0,001) où vous pouvez les additionner, les soustraire, les multiplier et les diviser.

La règle « magique » qui brise le jeu

Pendant longtemps, les mathématiciens ont cru que ce jeu était parfaitement résoluble. Si vous donniez à un ordinateur une énigme utilisant ces nombres, il pouvait éventuellement dire : « Oui, il y a une solution » ou « Non, il n'y en a pas ».

Cependant, l'auteur, Dejan Jovanović, a découvert un piège caché dans le manuel de règles officiel (la norme SMTLIB). Le piège réside dans la façon dont les règles gèrent la division par zéro.

En mathématiques normales, diviser par zéro est un grand « Non ». Mais dans ce manuel de règles informatique spécifique, les règles disent : « Si vous divisez par zéro, peu importe la réponse. Cela peut être n'importe quoi, tant que cela se comporte comme un nombre normal lorsque vous ne divisez pas par zéro. »

L'auteur appelle cela une « fonction non interprétée ». Pour utiliser une analogie : imaginez un distributeur automatique qui fonctionne parfaitement pour chaque collation que vous achetez. Mais si vous essayez d'acheter une « Collation Zéro », la machine ne plante pas ; elle recrache simplement quelque chose — peut-être une barre chocolatée, peut-être un caillou, peut-être un nuage. Les règles ne vous disent pas ce que ce sera ; elles disent simplement : « Ce sera quelque chose. »

Comment cela rend le jeu insoluble

L'article soutient que cette règle « tout est permis » pour la division par zéro est la clé qui ouvre une porte vers le chaos.

Voici la logique, simplifiée :

L'objectif : L'auteur veut prouver que si vous avez cette règle de division « magique », vous pouvez tromper l'ordinateur pour qu'il résolve des énigmes entières (des énigmes avec des nombres entiers comme 1, 2, 3).
Le problème : Résoudre des énigmes entières est célèbre pour être impossible pour les ordinateurs de faire parfaitement dans tous les cas (c'est ce qu'on appelle le 10e problème de Hilbert). C'est comme essayer de trouver une aiguille dans une botte de foin qui ne cesse de grandir indéfiniment.
L'astuce : L'auteur montre qu'en utilisant la division « magique » par zéro, vous pouvez construire un pont mathématique. Vous pouvez prendre une énigme entière difficile et la traduire en une énigme de nombres réels en utilisant cette astuce de division.
- Analogie : Imaginez que vous avez un code secret écrit dans une langue que seuls les humains comprennent (les entiers). Vous construisez une machine (l'astuce de division) qui traduit ce code dans une langue que les ordinateurs comprennent (les nombres réels). Parce que la langue de l'ordinateur possède cette règle « magique » de division par zéro, l'ordinateur peut accidentellement résoudre le code humain.
Le résultat : Puisque nous savons que les ordinateurs ne peuvent pas résoudre toutes les énigmes entières, et que cette astuce leur permet d'essayer de résoudre des énigmes entières en utilisant des nombres réels, cela signifie que l'ordinateur ne peut pas résoudre toutes les énigmes de nombres réels non plus. Le jeu devient indécidable.

L'analogie de la fonction « partie entière »

Pour prouver cela, l'auteur utilise une astuce ingénieuse. Il montre que si vous avez cette division « magique », vous pouvez forcer l'ordinateur à agir comme une fonction partie entière (une fonction qui arrondit un nombre à l'entier inférieur le plus proche, comme transformer 3,9 en 3).

Une fois que l'ordinateur peut arrondir les nombres vers le bas, il peut commencer à compter les entiers. Une fois qu'il peut compter les entiers, il peut essayer de résoudre ces énigmes entières impossibles. Puisque ces énigmes sont impossibles à résoudre en général, tout le système de mathématiques à nombres réels avec cette règle de division devient impossible à résoudre en général.

Ce que cela signifie pour le monde réel (selon l'article)

L'article ne parle pas d'IA future ou d'applications médicales. Il se concentre sur l'état actuel des benchmarks informatiques (problèmes de test) :

Le piège : De nombreux problèmes de test existants dans la bibliothèque SMTLIB (une vaste collection d'énigmes mathématiques utilisées pour tester les ordinateurs) utilisent la division avec des variables (comme x / y). Si y se trouve être zéro, ces énigmes tombent dans le piège « indécidable ».
La solution ? L'auteur suggère deux façons de réparer le manuel de règles :
1. Choisir une réponse spécifique : Décider que diviser par zéro toujours égal à un nombre spécifique (comme 0 ou 1), tout comme certains systèmes informatiques le gèrent pour les nombres binaires.
2. Diviser le jeu : Créer une nouvelle catégorie séparée pour les problèmes où vous divisez par des variables, et garder la catégorie « sûre » pour les problèmes où vous ne divisez que par des nombres connus (constantes).

L'essentiel

L'article affirme qu'une règle spécifique, apparemment inoffensive, sur la façon dont les ordinateurs gèrent la « division par zéro » brise accidentellement la capacité des ordinateurs à résoudre tous les problèmes mathématiques impliquant des nombres réels. Elle transforme un jeu résoluble en un jeu insoluble en permettant à l'ordinateur de résoudre subrepticement des problèmes qu'il ne devrait pas être capable de résoudre.

Résumé technique : L'arithmétique non linéaire avec la division SMTLIB est indécidable

Énoncé du problème
L'article examine le statut de décidabilité de la théorie de l'arithmétique réelle non linéaire (NRA) telle que définie formellement dans la norme SMTLIB. Alors que la théorie des corps réels clos (comprenant les égalités et les inégalités sur les polynômes) constitue un fragment décidable bien établi de la logique mathématique (Tarski [7]), la définition SMTLIB de la NRA étend cette signature pour inclure la division. La question critique découle du traitement de la division par zéro. Dans la norme SMTLIB, la division est interprétée comme prévu pour les diviseurs non nuls, mais reste une fonction non interprétée lorsque le diviseur est nul. Plus précisément, l'axiome $(\forall x, y \in \mathbb{R}) (y \neq 0) \Rightarrow (x = \frac{x}{y} \cdot y)$ autorise n'importe quelle valeur pour $\frac{x}{0}$ , à condition que le comportement standard soit maintenu par ailleurs. L'article examine si ce traitement spécifique de la division par zéro préserve la décidabilité de la théorie.

Méthodologie
L'auteur recourt à une preuve par réduction pour démontrer l'indécidabilité. La méthodologie procède en deux étapes logiques :

Réduction depuis l'arithmétique entière : L'article établit d'abord que l'arithmétique réelle augmentée d'une seule fonction unaire non interprétée est indécidable. Cela est obtenu en axiomatisant la fonction non interprétée $f$ $f$ pour qu'elle se comporte comme la fonction partie entière $\lfloor \cdot \rfloor$ $⌊ \cdot ⌋$ en utilisant les axiomes :
- $(\forall x \in \mathbb{R}) f(x) + 1 = f(x + 1)$
- $(\forall x \in \mathbb{R}) (0 \le x < 1) \Rightarrow (f(x) = 0)$
  En imposant ces axiomes, toute formule sur des variables entières peut être équivalente satisfaisable à une formule sur des variables réelles impliquant $f$ . Puisque l'arithmétique entière est indécidable (10e problème de Hilbert [4]), la théorie de l'arithmétique réelle étendue devient indécidable.
Mise en correspondance avec la division par zéro : L'article associe ensuite la fonction non interprétée $f$ de l'étape précédente directement à l'opération de division par zéro ( $\frac{x}{0}$ ). En traitant $\frac{x}{0}$ comme une fonction non interprétée, les axiomes nécessaires pour simuler la fonction partie entière peuvent être encodés au sein de la théorie NRA. Par conséquent, la satisfiabilité de formules entières arbitraires peut être réduite à la satisfiabilité de formules NRA impliquant une division par zéro.

Contributions et résultats clés

Preuve d'indécidabilité : Le résultat principal est la démonstration que la théorie SMTLIB de l'arithmétique réelle non linéaire (NRA) est indécidable. Cela découle directement de l'inclusion de la division où le diviseur est une fonction non interprétée à zéro.
Mécanisme d'encodage : L'article fournit un encodage concret (Exemple 1) montrant comment traduire la satisfiabilité d'équations diophantiennes (par exemple, $a^3 + b^3 = c^3$ sur les entiers) en formules NRA. Cela s'effectue en affirmant que les variables agissent comme des entiers via la simulation de la fonction partie entière utilisant $\frac{x}{0}$ , puis en appliquant les contraintes polynomiales.
Impact sur les benchmarks existants : L'analyse révèle que, bien que de nombreux benchmarks de la catégorie NRA de SMTLIB n'utilisent la division qu'avec des diviseurs constants (un fragment décidable), ceux qui utilisent des diviseurs non constants tombent dans le fragment indécidable nouvellement identifié.

Portée et affirmations
L'article affirme que ce résultat est « inattendu » étant donné que le fragment décidable des contraintes polynomiales est un résultat majeur en logique mathématique. La portée réside dans la clarification des limites théoriques de la norme SMTLIB : l'inclusion de la division en tant que fonction non interprétée à zéro modifie fondamentalement le paysage de la décidabilité, rendant la théorie complète indécidable.

L'auteur note que cette limitation empêche l'extension des techniques complètes d'élimination des quantificateurs (telles que celles utilisées dans CAD ou les approches d'élimination paresseuse des quantificateurs [3, 5, 6]) à la théorie NRA complète en présence de division par zéro.

Atténuations proposées
L'article conclut en décrivant deux approches potentielles pour remédier à cette indécidabilité, sans prétendre avoir résolu le problème dans le cadre de la norme actuelle :

Division totale : Assigner une valeur spécifique à la division par zéro (similaire à la théorie des vecteurs de bits [1]), bien que cela présente des défis dans le choix d'une valeur appropriée.
Séparation des théories : Déplacer la division avec des diviseurs non constants vers une théorie séparée (proposée sous le nom UFNRA) et restreindre la NRA aux contraintes polynomiales plus la division par des constantes non nulles. L'auteur reconnaît que cela nécessiterait de reclassifier les benchmarks existants.