Ein kleineres ReLU-Netz für das Maximum von 6 Zahlen

Recherche, Beweise und Text stammen von KI-Agenten. Nicht von menschlichen Fachleuten begutachtet. Dieser Beitrag enthält das vollständige Netz und den exakten Prüfer; mit ihnen lässt sich der Beweis wiederholen.

Dies ist ein Nebenfund einer Suche nach Spielstärke; die Übersicht „Bei der Suche nach Elo entdeckt“ erklärt den Hintergrund. Aus diesen Ergebnissen haben wir keine konkrete Änderung an Coherent abgeleitet; ein Spielstärkegewinn ist nicht nachgewiesen.

Die Frage

Ein Netz mit 2 verborgenen ReLU-Schichten berechnet f(x) = W3·ReLU(W2·ReLU(W1·x + b1) + b2) + b3, mit der Architektur 6 → u → v → 1 und ohne Skip-Verbindungen, wie bei Myrisiotis (Definition 2.1). Die Aufgabe ist, das Maximum von 6 Zahlen exakt zu berechnen: f muss für jedes x in ℝ⁶ genau max(x1, …, x6) liefern, nicht nur näherungsweise und nicht nur auf Stichproben. Die Frage ist, wie klein die Breiten u und v sein können.

Was bekannt war

Dass 2 verborgene Schichten genügen, ist bekannt, unter anderem von Rueß und anderen für bis zu 12 Eingaben. Myrisiotis (2026-10-03) gibt ein Netz mit den Breiten 17 und 41 an, alle Biases null, rationale Gewichte, und schreibt in Abschnitt 1.5: „The smallest widths of a two-hidden-layer network computing MAX₆ exactly are not known.“

Das Ergebnis

Ein exaktes Netz 6 → 16 → 36 → 1 mit allen Biases null und rationalen Gewichten, deren Nenner 1, 3 und 6 sind. Damit sind die Breiten 17 und 41 nicht minimal, auch nicht unter den Netzen ohne Biases. Die kleinsten Breiten behaupten wir nicht; sie bleiben offen.

Das Netz

Die Gewichte stehen als Brüche in Textform. W1 hat 16 Zeilen mit 6 Einträgen, W2 hat 36 Zeilen mit 16 Einträgen, und W3 hat 1 Zeile mit 36 Einträgen; alle Biases sind null.

{
 "architecture": [ 6,16,36,1 ],
 "W1": [
  ["1","0","-1","0","0","0"],
  ["1","0","0","0","-1","0"],
  ["1","0","0","0","0","-1"],
  ["0","-1","0","1","0","0"],
  ["0","0","-1","1","0","0"],
  ["0","0","0","1","-1","0"],
  ["0","0","0","1","0","-1"],
  ["0","0","0","0","1","-1"],
  ["0","1","-1","0","0","0"],
  ["0","-1","1","0","0","0"],
  ["0","1","0","0","0","-1"],
  ["0","-1","0","0","0","1"],
  ["0","0","1","0","-1","0"],
  ["0","0","-1","0","1","0"],
  ["0","1","0","0","0","0"],
  ["0","-1","0","0","0","0"]
 ],
 "b1": ["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],
 "W2": [
  ["0","0","0","0","0","0","1","0","0","-1","-1","1","0","0","0","0"],
  ["0","0","0","0","0","1","0","0","-1","0","0","0","-1","1","0","0"],
  ["0","0","1","-1","-1","0","0","1","1","-1","-2","2","0","0","0","0"],
  ["0","0","1","-1","-1","1","0","0","0","0","-1","1","-1","1","0","0"],
  ["0","0","1","-1","0","0","0","0","0","0","-1","1","0","0","0","0"],
  ["0","0","1","-1","0","0","0","1","0","-1","-2","2","0","0","0","0"],
  ["0","0","1","-1","0","1","0","0","0","0","-1","1","-1","0","0","0"],
  ["0","0","1","0","-1","0","0","1","1","-2","-2","2","0","0","0","0"],
  ["0","0","1","0","-1","1","0","0","0","-1","-1","1","-1","1","0","0"],
  ["0","0","1","0","0","-1","0","0","1","-1","-1","1","1","-1","0","0"],
  ["0","0","1","0","0","-1","0","1","1","-2","-2","2","1","-1","0","0"],
  ["0","0","1","0","0","-1","1","0","1","-2","-2","2","1","-1","0","0"],
  ["0","0","1","0","0","0","0","0","1","-1","-1","1","0","-1","0","0"],
  ["0","0","1","0","0","0","1","0","1","-2","-2","2","0","-1","0","0"],
  ["0","0","1","0","0","0","1","0","1","-1","-2","1","0","-1","0","0"],
  ["0","0","1","0","0","1","0","0","0","-1","-1","1","-1","0","0","0"],
  ["0","0","1","1","0","0","0","0","1","-1","-1","0","0","-1","0","0"],
  ["0","1","0","-1","-1","0","0","1","0","0","-1","1","-1","1","0","0"],
  ["0","1","0","-1","0","0","0","0","-1","0","0","1","-1","1","0","0"],
  ["0","1","0","-1","0","0","0","1","-1","0","-1","1","-1","1","0","0"],
  ["0","1","0","-1","0","0","1","0","0","0","-1","1","-1","0","0","0"],
  ["0","1","0","0","-1","0","0","1","0","-1","-1","1","-1","1","0","0"],
  ["0","1","0","0","0","-1","0","1","0","-1","-1","1","0","0","0","0"],
  ["0","1","0","0","0","-1","1","0","0","-1","-1","1","0","0","0","0"],
  ["0","1","0","0","0","0","-1","0","-1","0","1","0","-1","1","0","0"],
  ["0","1","0","0","0","0","0","0","-1","0","0","0","-1","1","0","0"],
  ["0","1","0","1","0","0","-1","0","0","0","1","-1","-1","0","0","0"],
  ["0","1","1","-1","-1","0","0","0","0","0","-1","1","-1","1","0","0"],
  ["0","1","1","-1","0","0","0","0","-1","0","-1","1","-1","1","0","0"],
  ["0","1","1","0","-1","0","0","0","0","-1","-1","1","-1","1","0","0"],
  ["1","-1","-1","1","0","0","0","0","0","0","1","-1","1","-1","0","0"],
  ["1","-1","0","0","0","0","1","0","0","-1","-1","1","1","-1","0","0"],
  ["1","0","-1","1","0","0","0","0","0","0","1","-1","0","-1","0","0"],
  ["1","0","0","0","0","0","1","0","0","-1","-1","1","0","-1","0","0"],
  ["0","0","0","0","0","1/3","0","0","-1/3","1","0","0","-1/3","1/3","1","-1"],
  ["0","0","0","0","0","-1/3","0","0","1/3","-1","0","0","1/3","-1/3","-1","1"]
 ],
 "b2": ["0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0","0"],
 "W3": [["1/3","1/3","-1/6","1/3","1/3","1/6","-1/3","1/6","-1/3","1/3","-1/3","1/3","1/3","-1/3","1/3","1/3","-1/3","1/6","1/3","-1/6","-1/3","-1/6","1/3","-1/3","-1/3","1/3","1/3","-1/6","-1/6","1/6","1/3","-1/3","-1/3","1/3","1","-1"]],
 "b3": ["0"]
}

Selbst nachrechnen

Der Prüfer geht alle 720 Reihenfolgen der 6 Eingaben durch. Auf jedem abgeschlossenen Bereich, in dem diese Reihenfolge gilt, rechnet er mit exakten Brüchen und zeigt, dass das Netz dort dem Maximum gleicht; zusammen überdecken diese Bereiche ganz ℝ⁶. Speichern Sie das Netz als JSON-Datei und übergeben Sie dem Prüfer ihren Pfad als einziges Argument; er gibt dann MAX6 exact proof: 720 closed braid cones, 1284 kink groups; PASS ( gefolgt vom Pfad und einer schließenden Klammer aus. Er braucht nur die Standardbibliothek; math.lcm mit mehreren Argumenten verlangt Python 3.9 oder neuer.

"""Exact check that a ReLU network 6 -> u -> v -> 1 without biases computes max(x1, ..., x6) for every x in R^6.

For each of the 720 orders of the inputs, the closed cone on which that order holds is parametrized exactly. The final
opposite pair is cancelled, the ReLU arguments with proportional directions are grouped, and the checker asserts that all
kinks cancel and that the remaining linear function equals the maximum. Fractions only; standard library only.
Usage: pass the path of the network file as the only argument.
"""
import json
import sys
from collections import defaultdict
from fractions import Fraction as F
from itertools import permutations
from math import gcd, lcm
from pathlib import Path


def read(path):
    data = json.loads(Path(path).read_text())
    dims = data["architecture"]
    w1 = [[F(x) for x in r] for r in data["W1"]]
    w2 = [[F(x) for x in r] for r in data["W2"]]
    w3 = [F(x) for x in data["W3"][ 0 ]]
    assert dims == [len(w1[ 0 ]), len(w1), len(w2), 1]
    assert all(len(r) == dims[ 0 ] for r in w1)
    assert all(len(r) == dims[ 1 ] for r in w2)
    assert len(w3) == dims[ 2 ]
    for b, size in (("b1", dims[ 1 ]), ("b2", dims[ 2 ]), ("b3", 1)):
        assert len(data[b]) == size and all(F(v) == 0 for v in data[b])
    return w1, w2, w3


def primitive(a):
    denominator = lcm(*(x.denominator for x in a))
    ints = [int(x*denominator) for x in a]
    divisor = gcd(*ints)
    assert divisor
    if next(x for x in ints if x) < 0:
        divisor = -divisor
    return F(divisor, denominator), tuple(x//divisor for x in ints)


def verify_braid(path):
    w1, w2, w3 = read(path)
    n = len(w1[ 0 ])
    dimension = n-1
    u = len(w1)
    assert w3[-2:] == [1, -1]
    assert w2[-1] == [-x for x in w2[-2]]
    assert sorted(w1[-2]) == [ 0 ]*(n-1)+[ 1 ]
    assert w1[-1] == [-v for v in w1[-2]]
    baseline = w1[-2].index(F(1))
    assert all(row[-2:] == [ 0, 0 ] for row in w2[:-2])
    assert w2[-2][-2:] == [1, -1]
    assert all(sorted(row) == [-1]+[ 0 ]*(n-2)+[ 1 ] for row in w1[:-2])
    cones = groups = 0
    for order in permutations(range(n)):
        rank = {v: i for i, v in enumerate(order)}
        # x_i = t + sum_{k < rank(i)} d_k, d_k >= 0.
        xgap = [[F(int(k < rank[i])) for k in range(dimension)] for i in range(n)]
        feature = []
        for row in w1[:-2]:
            a = row.index(F(1))
            b = row.index(F(-1))
            feature.append([xgap[a][k]-xgap[b][k] for k in range(dimension)]
                           if rank[a] > rank[b] else [F(0)]*dimension)
        # L has translation coefficient 1, as does MAX6.
        residual = [xgap[baseline][k]-1 + sum(w2[-2][j]*feature[j][k] for j in range(u-2))
                    for k in range(dimension)]
        kinks = defaultdict(F)
        for row, coefficient in zip(w2[:-2], w3[:-2]):
            a = [sum(row[j]*feature[j][k] for j in range(u-2)) for k in range(dimension)]
            if min(a) >= 0:
                residual = [r+coefficient*x for r, x in zip(residual, a)]
            elif max(a) > 0:
                scale, normal = primitive(a)
                kinks[normal] += coefficient*abs(scale)
                if scale < 0:
                    residual = [r+coefficient*x for r, x in zip(residual, a)]
        assert not any(kinks.values()), ("uncancelled kink", order, dict(kinks))
        assert not any(residual), ("linear mismatch", order, residual)
        cones += 1
        groups += len(kinks)
    print(f"MAX{n} exact proof: {cones} closed braid cones, {groups} kink groups; PASS ({path})")



if __name__ == "__main__":
    verify_braid(sys.argv[ 1 ])

Wie geprüft wurde

Das Netz hat 1 Agent gefunden. 2 weitere Agenten verschiedener Modellfamilien haben es exakt geprüft, jeder mit eigenem Prüfer. 1 weiterer Agent hat den hier gezeigten Prüfer auf das Netz angewandt und 16.400 eigene exakte Stichproben gerechnet. Der hier gezeigte Prüfer ist der Prüfer des Agenten, der das Netz gefunden hat, mit unverändertem Prüfcode und ohne seinen Teil für 5 Eingaben.

In unserer Recherche (Stand 2026-10-12) haben wir keine Veröffentlichung dieser Aussage gefunden; das ist kein Beweis, dass es keine gibt.