Update.

diff --git a/grid.py b/grid.py
index d06802d..ac0ebe0 100755 (executable)
--- a/grid.py
+++ b/grid.py
@@ -9,7 +9,7 @@
 # This code implement a simple system to manipulate formal
 # specifications of tokens on a grid.
 
 # This code implement a simple system to manipulate formal
 # specifications of tokens on a grid.
 

-import math, re
+import math, re, random

 
 import torch
 
 
 import torch
 


@@ -61,6 +61,7 @@ class FormalGrid:
 
     def constraint_to_fun(self, constraint):
         a, b, c = None, None, None
 
     def constraint_to_fun(self, constraint):
         a, b, c = None, None, None

+        col, row = self.col, self.row

 
         def match(pattern):
             nonlocal a, b, c
 
         def match(pattern):
             nonlocal a, b, c


@@ -73,79 +74,70 @@ class FormalGrid:
                 return False
 
         if match("([1-9]) is_in_top_half"):
                 return False
 
         if match("([1-9]) is_in_top_half"):

-            return self.row[:, a] < self.grid_height // 2
+            return row[:, a] < self.grid_height // 2

 
         elif match("([1-9]) is_in_bottom_half"):
 
         elif match("([1-9]) is_in_bottom_half"):

-            return self.row[:, a] >= self.grid_height // 2
+            return row[:, a] >= self.grid_height // 2

 
         elif match("([1-9]) is_on_left_side"):
 
         elif match("([1-9]) is_on_left_side"):

-            return self.col[:, a] < self.grid_width // 2
+            return col[:, a] < self.grid_width // 2

 
         elif match("([1-9]) is_on_right_side"):
 
         elif match("([1-9]) is_on_right_side"):

-            return self.col[:, a] >= self.grid_width // 2
+            return col[:, a] >= self.grid_width // 2

 
         elif match("([1-9]) next_to ([1-9])"):
 
         elif match("([1-9]) next_to ([1-9])"):

-            return (self.row[:, a] - self.row[:, b]).abs() + (
-                self.col[:, a] - self.col[:, b]
-            ).abs() <= 1
+            return (row[:, a] - row[:, b]).abs() + (col[:, a] - col[:, b]).abs() == 1

 
         elif match("([1-9]) is_below ([1-9])"):
 
         elif match("([1-9]) is_below ([1-9])"):

-            return self.row[:, a] > self.row[:, b]
+            return row[:, a] > row[:, b]

 
         elif match("([1-9]) is_above ([1-9])"):
 
         elif match("([1-9]) is_above ([1-9])"):

-            return self.row[:, a] < self.row[:, b]
+            return row[:, a] < row[:, b]

 
         elif match("([1-9]) is_left_of ([1-9])"):
 
         elif match("([1-9]) is_left_of ([1-9])"):

-            return self.col[:, a] < self.col[:, b]
+            return col[:, a] < col[:, b]

 
         elif match("([1-9]) is_right_of ([1-9])"):
 
         elif match("([1-9]) is_right_of ([1-9])"):

-            return self.col[:, a] > self.col[:, b]
+            return col[:, a] > col[:, b]

 
         elif match("([1-9]) ([1-9]) is_parallel_to_diagonal"):
 
         elif match("([1-9]) ([1-9]) is_parallel_to_diagonal"):

-            return (self.col[:, a] - self.col[:, b]).abs() == (
-                self.row[:, a] - self.row[:, b]
-            ).abs()
+            return (col[:, a] - col[:, b]).abs() == (row[:, a] - row[:, b]).abs()

 
         elif match("([1-9]) ([1-9]) is_vertical"):
 
         elif match("([1-9]) ([1-9]) is_vertical"):

-            return self.col[:, a] == self.col[:, b]
+            return col[:, a] == col[:, b]

 
         elif match("([1-9]) ([1-9]) is_horizontal"):
 
         elif match("([1-9]) ([1-9]) is_horizontal"):

-            return self.row[:, a] == self.row[:, b]
+            return row[:, a] == row[:, b]

 
         elif match("([1-9]) ([1-9]) ([1-9]) are_aligned"):
 
         elif match("([1-9]) ([1-9]) ([1-9]) are_aligned"):

-            return (self.col[:, a] - self.col[:, b]) * (
-                self.row[:, a] - self.row[:, c]
-            ) - (self.row[:, a] - self.row[:, b]) * (
-                self.col[:, a] - self.col[:, c]
-            ) == 0
+            return (col[:, a] - col[:, b]) * (row[:, a] - row[:, c]) - (
+                row[:, a] - row[:, b]
+            ) * (col[:, a] - col[:, c]) == 0

 
         elif match("([1-9]) middle_of ([1-9]) ([1-9])"):
 
         elif match("([1-9]) middle_of ([1-9]) ([1-9])"):

-            return (
-                grid_set
-                & (self.col[:, a] + self.col[:, c] == 2 * self.col[:, b])
-                & (self.row[:, a] + self.row[:, c] == 2 * self.row[:, b])
+            return (col[:, b] + col[:, a] == 2 * col[:, b]) & (
+                row[:, b] + row[:, a] == 2 * row[:, b]

             )
 
         elif match("([1-9]) is_equidistant_from ([1-9]) and ([1-9])"):
             )
 
         elif match("([1-9]) is_equidistant_from ([1-9]) and ([1-9])"):

-            return (self.col[:, a] - self.col[:, b]) ** 2 + (
-                self.row[:, a] - self.row[:, b]
-            ) ** 2 == (self.col[:, a] - self.col[:, c]) ** 2 + (
-                self.row[:, a] - self.row[:, c]
-            ) ** 2
-
-        elif match("([1-9]) is_further_away_from ([1-9]) than ([1-9])"):
-            return (self.col[:, a] - self.col[:, b]) ** 2 + (
-                self.row[:, a] - self.row[:, b]
-            ) ** 2 > (self.col[:, a] - self.col[:, c]) ** 2 + (
-                self.row[:, a] - self.row[:, c]
-            ) ** 2
+            return (col[:, a] - col[:, b]) ** 2 + (row[:, a] - row[:, b]) ** 2 == (
+                col[:, a] - col[:, c]
+            ) ** 2 + (row[:, a] - row[:, c]) ** 2
+
+        elif match("([1-9]) is_further_from ([1-9]) than_from ([1-9])"):
+            return (col[:, a] - col[:, b]) ** 2 + (row[:, a] - row[:, b]) ** 2 > (
+                col[:, a] - col[:, c]
+            ) ** 2 + (row[:, a] - row[:, c]) ** 2
+
+        elif match("([1-9]) is_closer_to ([1-9]) than_to ([1-9])"):
+            return (col[:, a] - col[:, b]) ** 2 + (row[:, a] - row[:, b]) ** 2 < (
+                col[:, a] - col[:, c]
+            ) ** 2 + (row[:, a] - row[:, c]) ** 2

 
         elif match("([1-9]) ([1-9]) ([1-9]) form_a_right_angle"):
 
         elif match("([1-9]) ([1-9]) ([1-9]) form_a_right_angle"):

-            return (self.col[:, a] - self.col[:, b]) * (
-                self.col[:, c] - self.col[:, b]
-            ) + (self.row[:, a] - self.row[:, b]) * (
-                self.row[:, c] - self.row[:, b]
-            ) == 0
+            return (col[:, a] - col[:, b]) * (col[:, c] - col[:, b]) + (
+                row[:, a] - row[:, b]
+            ) * (row[:, c] - row[:, b]) == 0

 
         else:
             raise ValueError(f"Unknown type of constraint {constraint}")
 
         else:
             raise ValueError(f"Unknown type of constraint {constraint}")


@@ -184,13 +176,138 @@ class FormalGrid:
                 v += " ".join(["-" if n == 0 else str(n.item()) for n in r]) + "\n"
             yield v
 
                 v += " ".join(["-" if n == 0 else str(n.item()) for n in r]) + "\n"
             yield v
 

+    def random_property(self):
+        a, b, c = random.sample(list(range(1, self.nb_symbols + 1)), 3)
+
+        sb, sc = min(b, c), max(b, c)
+
+        ta, tb, tc = sorted((a, b, c))
+
+        l = (
+            [
+                f"{a} is_in_top_half",
+                f"{a} is_in_bottom_half",
+                f"{a} is_on_left_side",
+                f"{a} is_on_right_side",
+            ]
+            + [
+                f"{a} is_below {b}",
+                f"{a} is_above {b}",
+                f"{a} is_left_of {b}",
+                f"{a} is_right_of {b}",
+                f"{sb} next_to {sc}",
+            ]
+            + [
+                f"{sb} {sc} is_parallel_to_diagonal",
+                f"{sb} {sc} is_vertical",
+                f"{sb} {sc} is_horizontal",
+            ]
+            * 2
+            + [
+                f"{ta} {tb} {tc} are_aligned",
+                f"{a} middle_of {sb} {sc}",
+                f"{ta} {tb} {tc} form_a_right_angle",
+            ]
+            * 3
+            + [
+                f"{a} is_equidistant_from {sb} and {sc}",
+                f"{a} is_further_from {b} than_from {c}",
+                f"{a} is_closer_to {b} than_to {c}",
+            ]
+        )
+
+        return random.choice(l)
+

 
 ######################################################################
 
 if __name__ == "__main__":
 
 ######################################################################
 
 if __name__ == "__main__":

-    device = torch.device("cuda" if torch.cuda.is_available() else "cpu")

 
 

-    grid = FormalGrid(grid_height=8, grid_width=8, nb_symbols=4, device=device)
+    if torch.cuda.is_available():
+        device = torch.device("cuda")
+    elif torch.backends.mps.is_available():
+        device = torch.device("mps")
+    else:
+        device = torch.device("cpu")
+
+    # grid = FormalGrid(grid_height=7, grid_width=7, nb_symbols=4, device=device)
+    # grid_set = grid.new_grid_set(["4 is_equidistant_from 2 and 3", "2 4 is_parallel_to_diagonal"])
+    # print(next(iter(grid.views(grid_set))))
+    # exit(0)
+
+    def proof_depth(steps, c):
+        a = steps.get(c)
+        if a is None:
+            return 0
+        else:
+            c1, c2 = a
+            return max(proof_depth(steps, c1), proof_depth(steps, c2))
+
+    def generate_proof(grid):
+        while True:
+            constraints = [grid.random_property() for _ in range(10)]
+            grid_set = grid.new_grid_set(constraints)
+            if grid_set.any():
+                break
+
+        mg = grid.master_grid_set
+
+        print(constraints)
+
+        initial = constraints.copy()
+
+        steps = {}
+
+        for _ in range(1000):
+            c1, c2 = random.sample(constraints, 2)
+            f1, f2 = grid.constraint_to_fun(c1), grid.constraint_to_fun(c2)
+            for _ in range(100):
+                c = grid.random_property()
+                if c not in constraints:
+                    f = grid.constraint_to_fun(c)
+                    if (
+                        (mg & f1 & ~f).any()
+                        and (mg & f2 & ~f).any()
+                        and (mg & f1 & f2 & f).any()
+                        and not (mg & f1 & f2 & ~f).any()
+                    ):
+                        constraints.append(c)
+                        print(c1, "and", c2, "=>", c)
+                        steps[c] = (c1, c2)
+                        # print(next(iter(grid.views(grid.new_grid_set([c1, c2])))))
+                        # print("we have", constraints)
+                        # proof.append(c1 + " and " + c2 + " hence " + c)
+                        break
+
+            if steps.keys() and max([proof_depth(steps, c) for c in steps.keys()]) >= 3:
+
+                break
+
+        return initial, steps
+
+    grid = FormalGrid(grid_height=7, grid_width=7, nb_symbols=4, device=device)
+
+    initial, steps = generate_proof(grid)
+
+    print(" ; ".join(initial))
+
+    def proof(c, indent=""):
+        a = steps.get(c)
+        if a is None:
+            print(f"{indent}{c} is given")
+        else:
+            print(f"{indent}{c} since")
+            c1, c2 = a
+            proof(c1, indent + "  ")
+            proof(c2, indent + "  ")
+
+    print(" ; ".join(initial))
+
+    for c in steps.keys():
+        proof(c)
+        print()
+
+    exit(0)

 
     # grid_set = grid.new_grid_set(
     # [
 
     # grid_set = grid.new_grid_set(
     # [


@@ -208,6 +325,9 @@ if __name__ == "__main__":
             "2 3 is_parallel_to_diagonal",
             "4 1 is_vertical",
             "3 4 is_horizontal",
             "2 3 is_parallel_to_diagonal",
             "4 1 is_vertical",
             "3 4 is_horizontal",

+            "3 is_left_of 2",
+            "1 is_below 4",
+            "2 is_right_of 4",

         ],
     )
 
         ],
     )
 

diff --git a/picocrafter.py b/picocrafter.py
index 23d93b2..001bb81 100755 (executable)
--- a/picocrafter.py
+++ b/picocrafter.py
@@ -227,9 +227,9 @@ class PicroCrafterEnvironment:
         r = u.sort(dim=-1, descending=True).indices[:, : len(z)]
 
         q *= self.tile2id["#"]
         r = u.sort(dim=-1, descending=True).indices[:, : len(z)]
 
         q *= self.tile2id["#"]

-        q[
-            torch.arange(q.size(0), device=q.device)[:, None].expand_as(r), r
-        ] = torch.tensor([self.tile2id[c] for c in z], device=q.device)[None, :]
+        q[torch.arange(q.size(0), device=q.device)[:, None].expand_as(r), r] = (
+            torch.tensor([self.tile2id[c] for c in z], device=q.device)[None, :]
+        )

 
         if world_margin > 0:
             r = m.new_full(
 
         if world_margin > 0:
             r = m.new_full(

diff --git a/tinyae.py b/tinyae.py
index 0baa5a2..806559e 100755 (executable)
--- a/tinyae.py
+++ b/tinyae.py
@@ -92,8 +92,8 @@ class AutoEncoder(nn.Module):
         return self.decoder(z.view(z.size(0), -1, 1, 1))
 
     def forward(self, x):
         return self.decoder(z.view(z.size(0), -1, 1, 1))
 
     def forward(self, x):

-        x = self.encoder(x)
-        x = self.decoder(x)
+        x = self.encode(x)
+        x = self.decode(x)

         return x
 
 
         return x
 
 

diff --git a/tinymnist.py b/tinymnist.py
index f662be6..19b9387 100755 (executable)
--- a/tinymnist.py
+++ b/tinymnist.py
@@ -1,5 +1,8 @@
 #!/usr/bin/env python
 
 #!/usr/bin/env python
 

+# @XREMOTE_HOST: elk.fleuret.org
+# @XREMOTE_PRE: source ~/venv/pytorch/bin/activate
+

 # Any copyright is dedicated to the Public Domain.
 # https://creativecommons.org/publicdomain/zero/1.0/
 
 # Any copyright is dedicated to the Public Domain.
 # https://creativecommons.org/publicdomain/zero/1.0/
 


@@ -14,7 +17,12 @@ lr, nb_epochs, batch_size = 1e-1, 10, 100
 
 data_dir = os.environ.get("PYTORCH_DATA_DIR") or "./data/"
 
 
 data_dir = os.environ.get("PYTORCH_DATA_DIR") or "./data/"
 

-device = torch.device("cuda" if torch.cuda.is_available() else "cpu")
+if torch.cuda.is_available():
+    device = torch.device("cuda")
+elif torch.backends.mps.is_available():
+    device = torch.device("mps")
+else:
+    device = torch.device("cpu")

 
 ######################################################################
 
 
 ######################################################################
 


@@ -52,7 +60,7 @@ model = SomeLeNet()
 
 nb_parameters = sum(p.numel() for p in model.parameters())
 
 
 nb_parameters = sum(p.numel() for p in model.parameters())
 

-print(f"nb_parameters {nb_parameters}")
+print(f"device {device} nb_parameters {nb_parameters}")

 
 optimizer = torch.optim.SGD(model.parameters(), lr=lr)
 criterion = nn.CrossEntropyLoss()
 
 optimizer = torch.optim.SGD(model.parameters(), lr=lr)
 criterion = nn.CrossEntropyLoss()


@@ -83,17 +91,23 @@ for k in range(nb_epochs):
         loss.backward()
         optimizer.step()
 
         loss.backward()
         optimizer.step()
 

+    acc_test_loss = 0.0

     nb_test_errors = 0
     for input, targets in zip(
         test_input.split(batch_size), test_targets.split(batch_size)
     ):
     nb_test_errors = 0
     for input, targets in zip(
         test_input.split(batch_size), test_targets.split(batch_size)
     ):

-        wta = model(input).argmax(1)
+        output = model(input)
+        loss = criterion(output, targets)
+        acc_test_loss += loss.item() * input.size(0)
+
+        wta = output.argmax(1)

         nb_test_errors += (wta != targets).long().sum()
         nb_test_errors += (wta != targets).long().sum()

+

     test_error = nb_test_errors / test_input.size(0)
     duration = time.perf_counter() - start_time
 
     print(
     test_error = nb_test_errors / test_input.size(0)
     duration = time.perf_counter() - start_time
 
     print(

-        f"loss {k} {duration:.02f}s {acc_train_loss/train_input.size(0):.02f} {test_error*100:.02f}%"
+        f"loss {k} {duration:.02f}s acc_train_loss {acc_train_loss/train_input.size(0):.02f} test_loss {acc_test_loss/test_input.size(0):.02f} test_error {test_error*100:.02f}%"

     )
 
 ######################################################################
     )
 
 ######################################################################