LeanDojoChatGPT
linc
LeanDojoChatGPT | linc | |
---|---|---|
2 | 1 | |
99 | 46 | |
- | - | |
5.3 | 4.4 | |
about 2 months ago | 5 months ago | |
Python | Jupyter Notebook | |
MIT License | - |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
LeanDojoChatGPT
-
'A-Team' of Math Proves a Critical Link Between Addition and Sets
Check out this paper:
https://leandojo.org/
People have already trained models to assist suggestion tactics. They then linked it up to ChatGPT to interactively solve proofs.
In this scenario, ChatGPT asks the model for tactic suggestions, applies it to the proof and uses the feedback from Lean to then proceed with the next step.
FYI, The programmatic interface to Lean was written by an OpenAI employee who was on the Lean team a few years ago.
Also, check out Lean’s roadmap. They aspire to position Lean to becoming a target for LLMs because it has been designed for verification from the ground up.
As math and compsci nerds contribute to mathlib, all of those proofs are also building up a huge corpus that will likely be leveraged for both verification and optimization.
If AI can make verification a lot easier, then we’re likely going to see verification change programming similarly to the way it changed electronics.
-
Formalizing 100 Theorems
Good questions!
Nowadays, there is indeed a movement towards interoperability between the various proof assistants, one of these bridge-building projects is called Dedukti: https://deducteam.github.io/ It's a challenging project because the different proof assistants which are currently in use differ in their foundational perspectives and their idioms. The question how to best formalize mathematics is still an open research problem, just as the question how to best develop programs, but we already have quite a good understanding of many important issues in this area.
Also, by now there are attempts to use AI for discovering proofs, see for instance https://leandojo.org/ or https://github.com/lean-dojo/LeanDojoChatGPT.
linc
-
'A-Team' of Math Proves a Critical Link Between Addition and Sets
Recent work on combining LLMs with theorem provers with promising initial results:
https://paperswithcode.com/paper/linc-a-neurosymbolic-approa...
> Logical reasoning, i.e., deductively inferring the truth value of a conclusion from a set of premises, is an important task for artificial intelligence with wide potential impacts on science, mathematics, and society. While many prompting-based strategies have been proposed to enable Large Language Models (LLMs) to do such reasoning more effectively, they still appear unsatisfactory, often failing in subtle and unpredictable ways. In this work, we investigate the validity of instead reformulating such tasks as modular neurosymbolic programming, which we call LINC: Logical Inference via Neurosymbolic Computation. In LINC, the LLM acts as a semantic parser, translating premises and conclusions from natural language to expressions in first-order logic. These expressions are then offloaded to an external theorem prover, which symbolically performs deductive inference. Leveraging this approach, we observe significant performance gains on FOLIO and a balanced subset of ProofWriter for three different models in nearly all experimental conditions we evaluate. On ProofWriter, augmenting the comparatively small open-source StarCoder+ (15.5B parameters) with LINC even outperforms GPT-3.5 and GPT-4 with Chain-of-Thought (CoT) prompting by an absolute 38% and 10%, respectively. When used with GPT-4, LINC scores 26% higher than CoT on ProofWriter while performing comparatively on FOLIO. Further analysis reveals that although both methods on average succeed roughly equally often on this dataset, they exhibit distinct and complementary failure modes. We thus provide promising evidence for how logical reasoning over natural language can be tackled through jointly leveraging LLMs alongside symbolic provers. All corresponding code is publicly available at https://github.com/benlipkin/linc
What are some alternatives?
upgini - Data search & enrichment library for Machine Learning → Easily find and add relevant features to your ML & AI pipeline from hundreds of public and premium external data sources, including open & commercial LLMs
marqo - Unified embedding generation and search engine. Also available on cloud - cloud.marqo.ai
FlexGen - Running large language models on a single GPU for throughput-oriented scenarios.
set.mm - Metamath source file for logic and set theory
FlexGen - Running large language models like OPT-175B/GPT-3 on a single GPU. Focusing on high-throughput generation. [Moved to: https://github.com/FMInference/FlexGen]
ChatGPT-API-Python - Building a Chatbot in Python using OpenAI's Official ChatGPT API
PIXIU - This repository introduces PIXIU, an open-source resource featuring the first financial large language models (LLMs), instruction tuning data, and evaluation benchmarks to holistically assess financial LLMs. Our goal is to continually push forward the open-source development of financial artificial intelligence (AI).