Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - feat(Tactic/Linarith): Simplex Algorithm oracle #12014

Closed
wants to merge 27 commits into from

Conversation

vasnesterov
Copy link
Collaborator

@vasnesterov vasnesterov commented Apr 8, 2024

  • Reduce the linarith certificate search problem to some Linear Programming problem and implement the Simplex Algorithm to solve it.
  • Set the default oracle for linarith to this.
  • Remove unnecessary hypotheses in Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean and Mathlib/Analysis/Distribution/SchwartzSpace.lean which were needed with the Fourier-Motzkin oracle.
  • Adjust the definition of CerficateOracle to enable dot notation to choose between oracles.

This addresses #2717 and #8875 (except when the user overrides the oracle)

Also, this oracle is far more efficient:
The example below takes lots of time with the Fourier-Motzkin oracle: I waited 5 minutes and still didn't get it. But with the just implemented Linarith.SimplexAlgo.produceCertificate oracle the proof succeeds in less than a second.

import Mathlib.Tactic.Linarith

example (x0 x1 x2 x3 x4 : ℚ) :
  3 * x0 - 15 * x1 - 30 * x2 + 20 * x3 + 12 * x4 ≤ 035 * x0 - 30 * x1 + 12 * x2 - 15 * x3 + 18 * x4 ≤ 05 * x0 + 20 * x1 + 24 * x2 + 20 * x3 + 9 * x4 ≤ 0 →
  -2 * x0 - 30 * x1 + 30 * x2 - 10 * x3 - 12 * x4 ≤ 0 →
  -4 * x0 - 25 * x1 + 6 * x2 - 20 * x3 ≤ 025 * x1 + 30 * x2 - 25 * x3 + 12 * x4 ≤ 010 * x1 - 18 * x2 - 30 * x3 + 18 * x4 ≤ 04 * x0 + 10 * x1 - 18 * x2 - 15 * x3 + 15 * x4 ≤ 0 →
  -4 * x0 + 15 * x1 - 30 * x2 + 15 * x3 + 6 * x4 ≤ 0 →
  -2 * x0 - 5 * x1 + 18 * x2 - 25 * x3 - 161 * x4 ≤ 0 →
  -6 * x0 + 30 * x1 + 6 * x2 - 15 * x3 ≤ 03 * x0 + 10 * x1 - 30 * x2 + 25 * x3 + 12 * x4 ≤ 02 * x0 + 10 * x1 - 24 * x2 - 15 * x3 + 3 * x4 ≤ 082 * x1 + 36 * x2 + 20 * x3 + 9 * x4 ≤ 02 * x0 - 30 * x1 - 30 * x2 - 15 * x3 + 6 * x4 ≤ 04 * x0 - 15 * x1 + 25 * x2 < 0 →
  -4 * x0 - 10 * x1 + 30 * x2 - 15 * x3 ≤ 02 * x0 + 6 * x2 + 133 * x3 + 12 * x4 ≤ 03 * x0 + 15 * x1 - 6 * x2 - 15 * x3 - 15 * x4 ≤ 010 * x1 + 6 * x2 - 25 * x3 + 3 * x4 ≤ 0 →
  -2 * x0 + 5 * x1 + 12 * x2 - 20 * x3 + 12 * x4 ≤ 0 →
  -5 * x0 - 25 * x1 + 30 * x3 - 12 * x4 ≤ 0 →
  -6 * x0 - 30 * x1 - 36 * x2 + 20 * x3 + 12 * x4 ≤ 05 * x0 - 5 * x1 + 6 * x2 - 25 * x3 ≤ 0 →
  -3 * x0 - 20 * x1 - 30 * x2 + 5 * x3 + 3 * x4 ≤ 0 →
  False := by intros; linarith (config := {oracle := Linarith.FourierMotzkin.produceCertificate})

I am planning to prove the "completeness" of the oracle in the next PRs, but so far I have run a stress test on randomly generated examples of various sizes, and it seems that everything is OK.


Open in Gitpod

@github-actions github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Apr 8, 2024
@vasnesterov vasnesterov added t-meta Tactics, attributes or user commands awaiting-review new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! and removed new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! labels Apr 8, 2024
@eric-wieser
Copy link
Member

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 5567bba.
There were significant changes against commit 1c351ac:

  Benchmark                                  Metric         Change
  ================================================================
+ ~Mathlib.Analysis.Normed.Group.AddCircle   instructions   -65.0%

@eric-wieser
Copy link
Member

At first glance this looks great! Could you add the examples from the two issues this closes as test cases in the test directory? Simply creating them is enough for them to be picked up as tests.

It's unfortunate that over mathlib as a whole this has almost no performance impact (besides the outlier Mathlib.Analysis.Normed.Group.AddCircle), but perhaps it only makes a difference on very large states; certainly this is not an argument against this PR :)

@vasnesterov
Copy link
Collaborator Author

@eric-wieser Thank you for your feedback! I have addressed your comments and slightly revised the code, making it shorter and (I hope) easier to read.

Mathlib/Tactic.lean Outdated Show resolved Hide resolved
Mathlib/Tactic.lean Outdated Show resolved Hide resolved
@eric-wieser
Copy link
Member

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 6bff856.
The entire run failed.
Found no significant differences.

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 7, 2024
@vasnesterov
Copy link
Collaborator Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 18974fc.
There were significant changes against commit 78e447b:

  Benchmark                                     Metric         Change
  ===================================================================
+ ~Mathlib.Analysis.Normed.Group.AddCircle      instructions   -62.6%
- ~Mathlib.Geometry.Manifold.Instances.Sphere   instructions     7.0%

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 9, 2024
@kim-em
Copy link
Contributor

kim-em commented May 9, 2024

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels May 9, 2024
mathlib-bors bot pushed a commit that referenced this pull request May 9, 2024
- Reduce the `linarith` certificate search problem to some Linear Programming problem and implement the Simplex Algorithm to solve it. 
- Set the default oracle for `linarith` to this.
- Remove unnecessary hypotheses in `Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean` and `Mathlib/Analysis/Distribution/SchwartzSpace.lean` which were needed with the Fourier-Motzkin oracle.
- Adjust the definition of `CerficateOracle` to enable dot notation to choose between oracles.

This addresses #2717 and #8875 (except when the user overrides the oracle)

Also, this oracle is far more efficient:
The example below takes lots of time with the Fourier-Motzkin oracle: I waited 5 minutes and still didn't get it. But with the just implemented `Linarith.SimplexAlgo.produceCertificate` oracle the proof succeeds in less than a second.
```lean
import Mathlib.Tactic.Linarith

example (x0 x1 x2 x3 x4 : ℚ) :
  3 * x0 - 15 * x1 - 30 * x2 + 20 * x3 + 12 * x4 ≤ 0 →
  35 * x0 - 30 * x1 + 12 * x2 - 15 * x3 + 18 * x4 ≤ 0 →
  5 * x0 + 20 * x1 + 24 * x2 + 20 * x3 + 9 * x4 ≤ 0 →
  -2 * x0 - 30 * x1 + 30 * x2 - 10 * x3 - 12 * x4 ≤ 0 →
  -4 * x0 - 25 * x1 + 6 * x2 - 20 * x3 ≤ 0 →
  25 * x1 + 30 * x2 - 25 * x3 + 12 * x4 ≤ 0 →
  10 * x1 - 18 * x2 - 30 * x3 + 18 * x4 ≤ 0 →
  4 * x0 + 10 * x1 - 18 * x2 - 15 * x3 + 15 * x4 ≤ 0 →
  -4 * x0 + 15 * x1 - 30 * x2 + 15 * x3 + 6 * x4 ≤ 0 →
  -2 * x0 - 5 * x1 + 18 * x2 - 25 * x3 - 161 * x4 ≤ 0 →
  -6 * x0 + 30 * x1 + 6 * x2 - 15 * x3 ≤ 0 →
  3 * x0 + 10 * x1 - 30 * x2 + 25 * x3 + 12 * x4 ≤ 0 →
  2 * x0 + 10 * x1 - 24 * x2 - 15 * x3 + 3 * x4 ≤ 0 →
  82 * x1 + 36 * x2 + 20 * x3 + 9 * x4 ≤ 0 →
  2 * x0 - 30 * x1 - 30 * x2 - 15 * x3 + 6 * x4 ≤ 0 →
  4 * x0 - 15 * x1 + 25 * x2 < 0 →
  -4 * x0 - 10 * x1 + 30 * x2 - 15 * x3 ≤ 0 →
  2 * x0 + 6 * x2 + 133 * x3 + 12 * x4 ≤ 0 →
  3 * x0 + 15 * x1 - 6 * x2 - 15 * x3 - 15 * x4 ≤ 0 →
  10 * x1 + 6 * x2 - 25 * x3 + 3 * x4 ≤ 0 →
  -2 * x0 + 5 * x1 + 12 * x2 - 20 * x3 + 12 * x4 ≤ 0 →
  -5 * x0 - 25 * x1 + 30 * x3 - 12 * x4 ≤ 0 →
  -6 * x0 - 30 * x1 - 36 * x2 + 20 * x3 + 12 * x4 ≤ 0 →
  5 * x0 - 5 * x1 + 6 * x2 - 25 * x3 ≤ 0 →
  -3 * x0 - 20 * x1 - 30 * x2 + 5 * x3 + 3 * x4 ≤ 0 →
  False := by intros; linarith (config := {oracle := Linarith.FourierMotzkin.produceCertificate})
```

I am planning to prove the "completeness" of the oracle in the next PRs, but so far I have run a stress test on randomly generated examples of various sizes, and it seems that everything is OK.



Co-authored-by: Eric Wieser <[email protected]>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented May 9, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Tactic/Linarith): Simplex Algorithm oracle [Merged by Bors] - feat(Tactic/Linarith): Simplex Algorithm oracle May 9, 2024
@mathlib-bors mathlib-bors bot closed this May 9, 2024
@mathlib-bors mathlib-bors bot deleted the vasnesterov_linarith_simplex_algo branch May 9, 2024 23:04
apnelson1 pushed a commit that referenced this pull request May 12, 2024
- Reduce the `linarith` certificate search problem to some Linear Programming problem and implement the Simplex Algorithm to solve it. 
- Set the default oracle for `linarith` to this.
- Remove unnecessary hypotheses in `Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean` and `Mathlib/Analysis/Distribution/SchwartzSpace.lean` which were needed with the Fourier-Motzkin oracle.
- Adjust the definition of `CerficateOracle` to enable dot notation to choose between oracles.

This addresses #2717 and #8875 (except when the user overrides the oracle)

Also, this oracle is far more efficient:
The example below takes lots of time with the Fourier-Motzkin oracle: I waited 5 minutes and still didn't get it. But with the just implemented `Linarith.SimplexAlgo.produceCertificate` oracle the proof succeeds in less than a second.
```lean
import Mathlib.Tactic.Linarith

example (x0 x1 x2 x3 x4 : ℚ) :
  3 * x0 - 15 * x1 - 30 * x2 + 20 * x3 + 12 * x4 ≤ 0 →
  35 * x0 - 30 * x1 + 12 * x2 - 15 * x3 + 18 * x4 ≤ 0 →
  5 * x0 + 20 * x1 + 24 * x2 + 20 * x3 + 9 * x4 ≤ 0 →
  -2 * x0 - 30 * x1 + 30 * x2 - 10 * x3 - 12 * x4 ≤ 0 →
  -4 * x0 - 25 * x1 + 6 * x2 - 20 * x3 ≤ 0 →
  25 * x1 + 30 * x2 - 25 * x3 + 12 * x4 ≤ 0 →
  10 * x1 - 18 * x2 - 30 * x3 + 18 * x4 ≤ 0 →
  4 * x0 + 10 * x1 - 18 * x2 - 15 * x3 + 15 * x4 ≤ 0 →
  -4 * x0 + 15 * x1 - 30 * x2 + 15 * x3 + 6 * x4 ≤ 0 →
  -2 * x0 - 5 * x1 + 18 * x2 - 25 * x3 - 161 * x4 ≤ 0 →
  -6 * x0 + 30 * x1 + 6 * x2 - 15 * x3 ≤ 0 →
  3 * x0 + 10 * x1 - 30 * x2 + 25 * x3 + 12 * x4 ≤ 0 →
  2 * x0 + 10 * x1 - 24 * x2 - 15 * x3 + 3 * x4 ≤ 0 →
  82 * x1 + 36 * x2 + 20 * x3 + 9 * x4 ≤ 0 →
  2 * x0 - 30 * x1 - 30 * x2 - 15 * x3 + 6 * x4 ≤ 0 →
  4 * x0 - 15 * x1 + 25 * x2 < 0 →
  -4 * x0 - 10 * x1 + 30 * x2 - 15 * x3 ≤ 0 →
  2 * x0 + 6 * x2 + 133 * x3 + 12 * x4 ≤ 0 →
  3 * x0 + 15 * x1 - 6 * x2 - 15 * x3 - 15 * x4 ≤ 0 →
  10 * x1 + 6 * x2 - 25 * x3 + 3 * x4 ≤ 0 →
  -2 * x0 + 5 * x1 + 12 * x2 - 20 * x3 + 12 * x4 ≤ 0 →
  -5 * x0 - 25 * x1 + 30 * x3 - 12 * x4 ≤ 0 →
  -6 * x0 - 30 * x1 - 36 * x2 + 20 * x3 + 12 * x4 ≤ 0 →
  5 * x0 - 5 * x1 + 6 * x2 - 25 * x3 ≤ 0 →
  -3 * x0 - 20 * x1 - 30 * x2 + 5 * x3 + 3 * x4 ≤ 0 →
  False := by intros; linarith (config := {oracle := Linarith.FourierMotzkin.produceCertificate})
```

I am planning to prove the "completeness" of the oracle in the next PRs, but so far I have run a stress test on randomly generated examples of various sizes, and it seems that everything is OK.



Co-authored-by: Eric Wieser <[email protected]>
callesonne pushed a commit that referenced this pull request May 16, 2024
- Reduce the `linarith` certificate search problem to some Linear Programming problem and implement the Simplex Algorithm to solve it. 
- Set the default oracle for `linarith` to this.
- Remove unnecessary hypotheses in `Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean` and `Mathlib/Analysis/Distribution/SchwartzSpace.lean` which were needed with the Fourier-Motzkin oracle.
- Adjust the definition of `CerficateOracle` to enable dot notation to choose between oracles.

This addresses #2717 and #8875 (except when the user overrides the oracle)

Also, this oracle is far more efficient:
The example below takes lots of time with the Fourier-Motzkin oracle: I waited 5 minutes and still didn't get it. But with the just implemented `Linarith.SimplexAlgo.produceCertificate` oracle the proof succeeds in less than a second.
```lean
import Mathlib.Tactic.Linarith

example (x0 x1 x2 x3 x4 : ℚ) :
  3 * x0 - 15 * x1 - 30 * x2 + 20 * x3 + 12 * x4 ≤ 0 →
  35 * x0 - 30 * x1 + 12 * x2 - 15 * x3 + 18 * x4 ≤ 0 →
  5 * x0 + 20 * x1 + 24 * x2 + 20 * x3 + 9 * x4 ≤ 0 →
  -2 * x0 - 30 * x1 + 30 * x2 - 10 * x3 - 12 * x4 ≤ 0 →
  -4 * x0 - 25 * x1 + 6 * x2 - 20 * x3 ≤ 0 →
  25 * x1 + 30 * x2 - 25 * x3 + 12 * x4 ≤ 0 →
  10 * x1 - 18 * x2 - 30 * x3 + 18 * x4 ≤ 0 →
  4 * x0 + 10 * x1 - 18 * x2 - 15 * x3 + 15 * x4 ≤ 0 →
  -4 * x0 + 15 * x1 - 30 * x2 + 15 * x3 + 6 * x4 ≤ 0 →
  -2 * x0 - 5 * x1 + 18 * x2 - 25 * x3 - 161 * x4 ≤ 0 →
  -6 * x0 + 30 * x1 + 6 * x2 - 15 * x3 ≤ 0 →
  3 * x0 + 10 * x1 - 30 * x2 + 25 * x3 + 12 * x4 ≤ 0 →
  2 * x0 + 10 * x1 - 24 * x2 - 15 * x3 + 3 * x4 ≤ 0 →
  82 * x1 + 36 * x2 + 20 * x3 + 9 * x4 ≤ 0 →
  2 * x0 - 30 * x1 - 30 * x2 - 15 * x3 + 6 * x4 ≤ 0 →
  4 * x0 - 15 * x1 + 25 * x2 < 0 →
  -4 * x0 - 10 * x1 + 30 * x2 - 15 * x3 ≤ 0 →
  2 * x0 + 6 * x2 + 133 * x3 + 12 * x4 ≤ 0 →
  3 * x0 + 15 * x1 - 6 * x2 - 15 * x3 - 15 * x4 ≤ 0 →
  10 * x1 + 6 * x2 - 25 * x3 + 3 * x4 ≤ 0 →
  -2 * x0 + 5 * x1 + 12 * x2 - 20 * x3 + 12 * x4 ≤ 0 →
  -5 * x0 - 25 * x1 + 30 * x3 - 12 * x4 ≤ 0 →
  -6 * x0 - 30 * x1 - 36 * x2 + 20 * x3 + 12 * x4 ≤ 0 →
  5 * x0 - 5 * x1 + 6 * x2 - 25 * x3 ≤ 0 →
  -3 * x0 - 20 * x1 - 30 * x2 + 5 * x3 + 3 * x4 ≤ 0 →
  False := by intros; linarith (config := {oracle := Linarith.FourierMotzkin.produceCertificate})
```

I am planning to prove the "completeness" of the oracle in the next PRs, but so far I have run a stress test on randomly generated examples of various sizes, and it seems that everything is OK.



Co-authored-by: Eric Wieser <[email protected]>
eric-wieser pushed a commit that referenced this pull request May 19, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 16, 2024
This PR updates the documentation following the integration of the oracle based on the Simplex Algorithm, as merged in PRs #12014, #13535, #12819, and #13800. Additionally, it moves the `SimplexAlgorithm` folder into the `Oracle` directory.



Co-authored-by: Rob Lewis <[email protected]>
AntoineChambert-Loir pushed a commit that referenced this pull request Jun 20, 2024
This PR updates the documentation following the integration of the oracle based on the Simplex Algorithm, as merged in PRs #12014, #13535, #12819, and #13800. Additionally, it moves the `SimplexAlgorithm` folder into the `Oracle` directory.



Co-authored-by: Rob Lewis <[email protected]>
kbuzzard pushed a commit that referenced this pull request Jun 26, 2024
This PR updates the documentation following the integration of the oracle based on the Simplex Algorithm, as merged in PRs #12014, #13535, #12819, and #13800. Additionally, it moves the `SimplexAlgorithm` folder into the `Oracle` directory.



Co-authored-by: Rob Lewis <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! ready-to-merge This PR has been sent to bors. t-meta Tactics, attributes or user commands
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants