search

wiio12 / LEGO-Prover

Code for the paper LEGO-Prover: Neural Theorem Proving with Growing Libraries
MIT License
54 stars 4 forks source link

TypeError on Prover Queue Completion? #5

Open ikb-a opened 2 months ago

ikb-a commented 2 months ago

Hi! I've been running the Lego-Prover on a subset of the problems for testing and I've run into some weird behaviour: is the Prover process supposed to exit with a TypeError upon completion of the queue?

Specifically, once the task queue is done I get the following error: (my apologies that the line numbers do not match the repo; I applied the black formatter to the code)

Process Process-1:
Traceback (most recent call last):
  File "/pkgs/python-3.10.12/lib/python3.10/multiprocessing/process.py", line 314, in _bootstrap
    self.run()
  File "/pkgs/python-3.10.12/lib/python3.10/multiprocessing/process.py", line 108, in run
    self._target(*self._args, **self._kwargs)
  File "/fs01/home/ianberlot/initiatives/tool_creation/source/LEGO-Prover/run_multiprocess.py", line 160, in run_prover
    prover.learn()
  File "/fs01/home/ianberlot/initiatives/tool_creation/source/LEGO-Prover/lego_prover/prover.py", line 382, in learn
    messages, reward, done, info = self.rollout(
  File "/fs01/home/ianberlot/initiatives/tool_creation/source/LEGO-Prover/lego_prover/prover.py", line 320, in rollout
    self.reset(task=task, context=context, reset_env=reset_env)
  File "/fs01/home/ianberlot/initiatives/tool_creation/source/LEGO-Prover/lego_prover/prover.py", line 147, in reset
    self.retrieved_skills = self.skill_manager.retrieve_skills_with_context(
  File "/fs01/home/ianberlot/initiatives/tool_creation/source/LEGO-Prover/lego_prover/agents/skill.py", line 236, in retrieve_skills_with_context
    query = context["formal_statement"]
TypeError: 'NoneType' object is not subscriptable

Taking a closer look, it seems to be that the context is retrieved by the curriculum agent https://github.com/wiio12/LEGO-Prover/blob/357672c7751cd0c84aff6bf72a3d1bf97614e81d/lego_prover/prover.py#L346 which is created in queue mode https://github.com/wiio12/LEGO-Prover/blob/357672c7751cd0c84aff6bf72a3d1bf97614e81d/run_multiprocess.py#L125

In this case, it seems to be that the curriculum returns None as the context once the queue is completed: https://github.com/wiio12/LEGO-Prover/blob/357672c7751cd0c84aff6bf72a3d1bf97614e81d/lego_prover/agents/curriculum.py#L66-L69

Based on the above, this seems to be the unavoidable behaviour -- is this actually how the Lego-Prover is meant to terminate its Prover processes, or have I somehow introduced a new bug?

Thanks for the help!