Skip to content

Grounding LLM mathematical reasoning with proof assistants.

License

Notifications You must be signed in to change notification settings

atroyn/math-llm

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

5 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Math LLM

This is a prototype project for grounding mathematical reasoning for large language models, using software proof assistants.

This repo is highly experimental, and anything might break at any time or not work for you.

Contributions are welcome.

Installation

You will need the coqtop command line application. This is a CLI for interacting with the Coq proof assistant software. I used the default installation path and it worked out of the box following the instructions in the included README.

You will need an OpenAI API Key set in the OPENAI_API_KEY environment variable.

Then run pip install -r requirements.txt

Run

python main.py

Roadmap

  • Interactively use Coq from Python
  • Use LLM to generate proofs in a readable format
  • Execute generated Coq
  • Use LLM to evaluate proofs for logical consistency
  • Store proof results in memory
  • Generate new conjectures
  • Break down proofs recursively into sub-goals
  • ...

About

Grounding LLM mathematical reasoning with proof assistants.

Resources

License

Stars

Watchers

Forks

Languages