1$ and set the objective:\n", "$$\n", " \\mathcal{G}^\\ast = \\mathrm{argmin}_{\\mathcal{G}_\\theta} (\\mathcal{G}_\\theta(\\phi) + \\mathrm{penalty}(\\mathcal{G}_\\theta,q))\n", "$$\n", "\n", "The penalty $c$ ($>1$) is higher than any potential reduction in $\\mathcal{G}(\\phi)$ ($\\leq 1$). $\\mathcal{G}^\\ast$ should satisfy in priority $\\mathcal{G}^*(\\mathcal{K}) \\geq q$ before reducing $\\mathcal{G}^*(\\phi)$.\n", "- If $\\mathcal{G}^\\ast(\\mathcal{K}) < q$ : Then for all $\\mathcal{G}_\\theta$, $\\mathcal{G}_\\theta(\\mathcal{K}) < q$ and therefore $(\\mathcal{K},\\mathcal{G}(\\ \\cdot\\mid \\theta), \\Theta)\\models_q\\phi$.\n", "- If $\\mathcal{G}^\\ast(\\mathcal{K}) \\geq q \\ \\text{and}\\ \\mathcal{G}^\\ast(\\phi) \\geq q$ : Then for all $\\mathcal{G}_\\theta$ with $\\mathcal{G}_\\theta(\\mathcal{K}) \\geq q$, we have that $\\mathcal{G}_\\theta(\\phi) \\geq \\mathcal{G}^\\ast(\\phi) \\geq q$ and therefore $(\\mathcal{K},\\mathcal{G}(\\ \\cdot\\mid\\theta),\\Theta)\\models_q\\phi$. \n", "- If $\\mathcal{G}^\\ast(\\mathcal{K}) \\geq q \\ \\text{and}\\ \\mathcal{G}^\\ast(\\phi) < q$ : Then $(\\mathcal{K},\\mathcal{G}(\\ \\cdot\\mid\\theta),\\Theta) \\nvDash_q\\phi$.\n", "\n", "### Soft constraint\n", "\n", "However, as $\\mathrm{penalty}(\\mathcal{G}_\\theta,q)$ is a constant function on the continuous parts of its domain (zero gradients), it cannot be used directly as an objective to reach via gradient descent optimization.Instead, one should approximate the penalty with a soft constraint.\n", "\n", "We use $\\mathtt{elu}(\\alpha,\\beta (q-\\mathcal{G}_\\theta(\\mathcal{K})))=\\begin{cases}\n", " \\beta (q-\\mathcal{G}_\\theta(\\mathcal{K}))\\ &\\text{if}\\ \\mathcal{G}_\\theta(\\mathcal{K}) \\leq 0,\\\\\n", " \\alpha (e^{q-\\mathcal{G}_\\theta(\\mathcal{K})}-1) \\ &\\text{otherwise},\n", "\\end{cases}$ where $\\alpha \\geq 0$ and $\\beta \\geq 0$ are two hyper-parameters:\n", "- When $\\mathcal{G}_\\theta(\\mathcal{K}) < q$, the penalty is linear in $(q-\\mathcal{G}_\\theta(\\mathcal{K}))$ with a slope of $\\beta$. \n", "Setting $\\beta$ high, the gradients for $\\mathcal{G}_\\theta(\\mathcal{K})$ will be high in absolute value if the knowledgebase in not satisfied; the minimizer will prioritize increasing the satisfaction of the knowledgebase.\n", "- When $\\mathcal{G}_\\theta(\\mathcal{K}) > q$, the penalty is a negative exponential that converges to $-\\alpha$.\n", "Setting $\\alpha$ low but non zero ensures that, while the penalty plays an insignificant role when the knowledgebase is satisfied, the gradients do not vanish." ], "metadata": {} }, { "cell_type": "code", "execution_count": 3, "source": [ "trainable_variables = ltn.as_tensors([A,B])\n", "optimizer = tf.keras.optimizers.Adam(learning_rate=0.001)\n", "\n", "# hyperparameters of the soft constraint\n", "alpha = 0.05\n", "beta = 10\n", "# satisfaction threshold\n", "q = 0.95\n", "\n", "for epoch in range(4000):\n", " with tf.GradientTape() as tape:\n", " sat_KB = axioms()\n", " sat_phi = phi()\n", " penalty = tf.keras.activations.elu(beta*(q-sat_KB),alpha=alpha)\n", " loss = sat_phi + penalty\n", " grads = tape.gradient(loss, trainable_variables)\n", " optimizer.apply_gradients(zip(grads, trainable_variables))\n", " if epoch%400 == 0:\n", " print(\"Epoch %d: Sat Level Knowledgebase %.3f Sat Level phi %.3f\"%(epoch, axioms(), phi()))\n", "print(\"Training finished at Epoch %d with Sat Level Knowledgebase %.3f Sat Level phi %.3f\"%(epoch, axioms(), phi()))" ], "outputs": [ { "output_type": "stream", "name": "stdout", "text": [ "Epoch 0: Sat Level Knowledgebase 0.002 Sat Level phi 0.001\n", "Epoch 400: Sat Level Knowledgebase 0.591 Sat Level phi 0.358\n", "Epoch 800: Sat Level Knowledgebase 0.862 Sat Level phi 0.610\n", "Epoch 1200: Sat Level Knowledgebase 0.950 Sat Level phi 0.705\n", "Epoch 1600: Sat Level Knowledgebase 0.950 Sat Level phi 0.615\n", "Epoch 2000: Sat Level Knowledgebase 0.951 Sat Level phi 0.485\n", "Epoch 2400: Sat Level Knowledgebase 0.962 Sat Level phi 0.319\n", "Epoch 2800: Sat Level Knowledgebase 0.998 Sat Level phi 0.116\n", "Epoch 3200: Sat Level Knowledgebase 1.000 Sat Level phi 0.000\n", "Epoch 3600: Sat Level Knowledgebase 1.000 Sat Level phi 0.000\n", "Training finished at Epoch 3999 with Sat Level Knowledgebase 1.000 Sat Level phi 0.000\n" ] } ], "metadata": {} }, { "cell_type": "markdown", "source": [ "At the end of training, the optimizer has found a grounding that satisfies $A \\lor B$ but not $A$ (given the satisfaction threshold $q=0.95$). This is a counterexample to the logical consequence, proving that $A \\lor B \\nvDash A$" ], "metadata": {} } ], "metadata": { "kernelspec": { "name": "python3", "display_name": "Python 3.9.6 64-bit ('tf-py39': conda)" }, "language_info": { "codemirror_mode": { "name": "ipython", "version": 3 }, "file_extension": ".py", "mimetype": "text/x-python", "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", "version": "3.9.6" }, "interpreter": { "hash": "889985fd10eb245a43f2ae5f5aa0c555254f5b898fe16071f1c89d06fa8d76a2" } }, "nbformat": 4, "nbformat_minor": 4 }