first commit

.github/workflows/CompatHelper.yml

@@ -0,0 +1,16 @@
+name: CompatHelper
+on:
+  schedule:
+    - cron: 0 0 * * *
+  workflow_dispatch:
+jobs:
+  CompatHelper:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Pkg.add("CompatHelper")
+        run: julia -e 'using Pkg; Pkg.add("CompatHelper")'
+      - name: CompatHelper.main()
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          COMPATHELPER_PRIV: ${{ secrets.DOCUMENTER_KEY }}
+        run: julia -e 'using CompatHelper; CompatHelper.main()'

.github/workflows/DocPreviewCleanup.yml

@@ -0,0 +1,28 @@
+name: DocPreviewCleanup
+
+on:
+  pull_request:
+    types: [closed]
+
+jobs:
+  doc-preview-cleanup:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout gh-pages branch
+        uses: actions/checkout@v2
+        with:
+          ref: gh-pages
+
+      - name: Delete preview and history
+        run: |
+            git config user.name "Documenter.jl"
+            git config user.email "[email protected]"
+            git rm -rf "previews/PR$PRNUM"
+            git commit -m "delete preview"
+            git branch gh-pages-new $(echo "delete history" | git commit-tree HEAD^{tree})
+        env:
+            PRNUM: ${{ github.event.number }}
+
+      - name: Push changes
+        run: |
+            git push --force origin gh-pages-new:gh-pages

.github/workflows/Documentation.yml

@@ -0,0 +1,24 @@
+name: Documentation
+
+on:
+  push:
+    branches:
+      - main
+    tags: '*'
+  pull_request:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v2
+      - uses: julia-actions/setup-julia@latest
+        with:
+          version: '1.6'
+      - name: Install dependencies
+        run: julia --project=. -e 'using Pkg; Pkg.instantiate()'
+      - name: Build and deploy
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} # For authentication with GitHub Actions token
+          DOCUMENTER_KEY: ${{ secrets.DOCUMENTER_KEY }} # For authentication with SSH deploy key
+        run: julia --project=. docs/make.jl

.github/workflows/JuliaFormatter.yml

@@ -0,0 +1,29 @@
+name: JuliaFormatter
+on:
+  schedule:
+    - cron: '0 0 * * *'
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v2
+      - name: Install JuliaFormatter and format
+        run: |
+          julia  -e 'import Pkg; Pkg.add("JuliaFormatter")'
+          julia  -e 'using JuliaFormatter; format(".")'
+      # https://github.com/marketplace/actions/create-pull-request
+      # https://github.com/peter-evans/create-pull-request#reference-example
+      - name: Create Pull Request
+        id: cpr
+        uses: peter-evans/create-pull-request@v3
+        with:
+          token: ${{ secrets.GITHUB_TOKEN }}
+          commit-message: Format .jl files
+          title: 'Automatic JuliaFormatter.jl run'
+          branch: auto-juliaformatter-pr
+          delete-branch: true
+          labels: formatting, automated pr, no changelog
+      - name: Check outputs
+        run: |
+          echo "Pull Request Number - ${{ steps.cpr.outputs.pull-request-number }}"
+          echo "Pull Request URL - ${{ steps.cpr.outputs.pull-request-url }}"

.github/workflows/TagBot.yml

@@ -0,0 +1,15 @@
+name: TagBot
+on:
+  issue_comment:
+    types:
+      - created
+  workflow_dispatch:
+jobs:
+  TagBot:
+    if: github.event_name == 'workflow_dispatch' || github.actor == 'JuliaTagBot'
+    runs-on: ubuntu-latest
+    steps:
+      - uses: JuliaRegistries/TagBot@v1
+        with:
+          token: ${{ secrets.GITHUB_TOKEN }}
+          ssh: ${{ secrets.DOCUMENTER_KEY }}

.gitignore

@@ -0,0 +1,8 @@
+/Manifest.toml
+data/
+runs/
+notebooks/.ipynb_checkpoints/
+docs/build/
+sbatch*.sh
+*.bin
+.DS_Store

Artifacts.toml

@@ -0,0 +1,11 @@
+[MiniSCAN]
+git-tree-sha1 = "4ca27a7e7d3ff3229e1c26bfccb8f218759240b5"
+
+[RuleTaker]
+git-tree-sha1 = "d70478825f8f7f558bc5c02165ce13b39610883f"
+
+[SCAN]
+git-tree-sha1 = "150c6b3c7ff99528b858607893ed2d9bd892a838"
+
+["SIGMORPHON 2018"]
+git-tree-sha1 = "19c102b7ea014308f41013df01eedde4cfb88997"

LICENSE

@@ -0,0 +1,24 @@
+BSD 2-Clause License
+
+Copyright (c) 2023, Princeton Vision & Learning Lab
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+1. Redistributions of source code must retain the above copyright notice, this
+   list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright notice,
+   this list of conditions and the following disclaimer in the documentation
+   and/or other materials provided with the distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

Project.toml

@@ -0,0 +1,38 @@
+name = "MetaQNL"
+uuid = "3cf0c2d0-60f4-44e0-ad1c-f938ae5d47cf"
+authors = ["Kaiyu Yang <[email protected]>"]
+version = "0.1.0"
+
+[deps]
+ArgParse = "c7e460c6-2fb9-53a9-8c5b-16f535851c63"
+BenchmarkTools = "6e4b80f9-dd63-53aa-95a3-0cdb28fa8baf"
+Bijections = "e2ed5e7c-b2de-5872-ae92-c73ca462fb04"
+Combinatorics = "861a8166-3701-5b0c-9a16-15d98fcdc6aa"
+Coverage = "a2441757-f6aa-5fb2-8edb-039e3f45d037"
+DataStructures = "864edb3b-99cc-5e75-8d2d-829cb0a9cfe8"
+Documenter = "e30172f5-a6a5-5a46-863b-614d45cd2de4"
+Downloads = "f43a241f-c20a-4ad4-852c-f6b1247861c6"
+IJulia = "7073ff75-c697-5162-941a-fcdaad2a7d2a"
+JSON3 = "0f8b85d8-7281-11e9-16c2-39a750bddbf1"
+JuliaFormatter = "98e50ef6-434e-11e9-1051-2b60c6c9e899"
+Julog = "5d8bcb5e-2b2c-4a96-a2b1-d40b3d3c344f"
+LibGit2 = "76f85450-5226-5b5a-8eaa-529ad045b433"
+LightGraphs = "093fc24a-ae57-5d10-9952-331d41423f4d"
+ParserCombinator = "fae87a5f-d1ad-5cf0-8f61-c941e1580b46"
+Pkg = "44cfe95a-1eb2-52ea-b672-e2afdf69b78f"
+ProgressMeter = "92933f4c-e287-5a05-a399-4b506db050ca"
+Random = "9a3f8284-a2c9-5f02-9a11-845980a1fd5c"
+Reexport = "189a3867-3050-52da-a836-e630ba90ab69"
+Revise = "295af30f-e4ad-537b-8983-00126c2a3abe"
+SHA = "ea8e919c-243c-51af-8825-aaa63cd721ce"
+Serialization = "9e88b42a-f829-5b0c-bbe9-9e923198166b"
+Statistics = "10745b16-79ce-11e8-11f9-7d13ad32a3b2"
+Tar = "a4e569a6-e804-4fa4-b0f3-eef7a1d5b13e"
+Z3 = "06b161dc-0161-11ea-0f74-41f836f4024b"
+ZipFile = "a5390f91-8eb1-5f08-bee0-b1d1ffed6cea"
+
+[extras]
+Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40"
+
+[targets]
+test = ["Test"]

README.md

@@ -0,0 +1,74 @@
+# Learning Symbolic Rules for Reasoning in Quasi-Natural Language
+
+![Example proof](images/proof.jpg)
+
+Code for the paper:  
+
+[Learning Symbolic Rules for Reasoning in Quasi-Natural Language](https://arxiv.org/abs/2111.12038)      
+Transactions on Machine Learning Research (TMLR), 2023  
+[Kaiyu Yang](https://www.cs.princeton.edu/~kaiyuy/) and [Jia Deng](https://www.cs.princeton.edu/~jiadeng/)     
+```bibtex
+@article{yang2023metaqnl,
+  title={Learning Symbolic Rules for Reasoning in Quasi-Natural Language},
+  author={Yang, Kaiyu and Deng, Jia},
+  journal={Transactions on Machine Learning Research (TMLR)},
+  year={2023},
+}
+```
+
+
+## Requirements
+
+1. [1.3 <= Julia < nightly](https://julialang.org/).
+1. Install the Julia packages in [Project.toml](./Project.toml): `julia --project=. -e 'import Pkg; Pkg.instantiate()'`.
+1. Install the [Open-WBO](http://sat.inesc-id.pt/open-wbo/) MAX-SAT solver. This step is not necessary if you want to use only Z3. But some of our experiments use OpenWBO since it can be faster in certain cases. 
+
+
+## Documentation
+
+`julia --project=. --color=yes docs/make.jl` will build the documentation at `docs/build/`.
+
+
+## Training
+
+Use [scripts/train.jl](scripts/train.jl) for training. Datasets will be downloaded automatically. Run `julia --project=. scripts/train.jl --help` for command line options.
+
+
+## Experiments on MiniSCAN
+```bash
+julia --project=. scripts/train.jl --dataset MiniSCAN --weight-candidate 0.4 --weight-existing 0.3 --maxsat-solver Z3
+```
+
+## Experiments on SCAN
+
+The `simple` split:
+```bash
+julia --project=. scripts/train.jl --dataset SCAN --split simple --num-train-examples 400 --weight-candidate 0.15 --weight-existing 0.15 --maxsat-solver Z3
+```
+
+The `length` split:
+```bash
+julia --project=. scripts/train.jl --dataset SCAN --split length --num-train-examples 400 --weight-candidate 0.15 --weight-existing 0.15 --maxsat-solver Z3
+```
+
+The `addprim_jump` split:
+```bash
+julia --project=. scripts/train.jl --dataset SCAN --split addprim_jump --num-train-examples 400 --weight-candidate 0.15 --weight-existing 0.15 --maxsat-solver Z3
+```
+
+The `addprim_turn_left` split:
+```bash
+julia --project=. scripts/train.jl --dataset SCAN --split addprim_turn_left --num-train-examples 400 --weight-candidate 0.15 --weight-existing 0.15 --maxsat-solver Z3
+```
+
+
+## Experiments on RuleTaker
+```bash
+julia --project=. scripts/train.jl --dataset RuleTaker --split depth-1 --num-train-examples 10000 --weight-candidate 0.5 --weight-existing 0.5 --maxsat-solver Z3
+julia --project=. scripts/train.jl --dataset RuleTaker --split depth-3 --num-train-examples 10000 --weight-candidate 0.25 --weight-existing 0.25 --maxsat-solver Z3 --lambda-provable 1.28 --lambda-unprovable 1.28
+```
+
+## Experiments on SIGMORPHON 2018:
+```bash
+julia --project=. scripts/train.jl --dataset Sigmorphon --lang spanish --split hard --copy 0 --weight-candidate 1.0 --weight-existing 1.0 --num-epochs 8
+```

docs/make.jl

@@ -0,0 +1,17 @@
+# push!(LOAD_PATH, "../src/")
+using MetaQNL
+using Documenter
+
+DocMeta.setdocmeta!(MetaQNL, :DocTestSetup, :(using MetaQNL); recursive = true)
+doctest(MetaQNL)
+makedocs(
+    sitename = "MetaQNL.jl",
+    format = Documenter.HTML(prettyurls = get(ENV, "CI", nothing) == "true"),
+)
+#=
+Uncomment when the repo becomes public
+deploydocs(
+    repo = "github.com/princeton-vl/MetaQNL.jl.git",
+    devbranch="main",
+)
+=#

docs/src/index.md

@@ -0,0 +1,9 @@
+# MetaQNL.jl Documentation
+
+```@contents
+```
+
+## Index
+
+```@index
+```

docs/src/meta_language.md

@@ -0,0 +1,5 @@
+# MetaLanguage
+
+```@autodocs
+Modules = [MetaLanguage]
+```

docs/src/model.md

@@ -0,0 +1,5 @@
+# Model
+
+```@autodocs
+Modules = [Model]
+```

docs/src/optimization.md

@@ -0,0 +1,5 @@
+# Optimization
+
+```@autodocs
+Modules = [Optimization]
+```

docs/src/task.md

@@ -0,0 +1,5 @@
+# Task
+
+```@autodocs
+Modules = [MetaQNL.Task]
+```

docs/src/theorem_proving.md

@@ -0,0 +1,5 @@
+# TheoremProving
+
+```@autodocs
+Modules = [TheoremProving]
+```

scripts/coverage.jl

@@ -0,0 +1,8 @@
+using Coverage
+
+coverage = process_folder()
+covered_lines, total_lines = get_summary(coverage)
+@info "Total lines: $total_lines"
+@info "Covered lines: $covered_lines"
+# @show get_summary(process_file(joinpath("src", "MyPkg.jl")))
+@info "Percentage covered: $(covered_lines / total_lines)"