search

albertqjiang / INT

Official code for paper: INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving
MIT License
37 stars 5 forks source link

observation_to_source throws error if the observation is already proved #14

Open fzyzcjy opened 1 year ago

fzyzcjy commented 1 year ago

e.g.


Traceback (most recent call last):
  File "/home/jychen/.conda/envs/jychen_main/lib/python3.10/site-packages/IPython/core/interactiveshell.py", line 3433, in run_code
    exec(code_obj, self.user_global_ns, self.user_ns)
  File "/tmp/ipykernel_21573/176925322.py", line 1, in <module>
    evaluate.interact_with_prover_sequentially(
  File "/data/jychen/research/code/research_mono/neural_theorem_prover/evaluate.py", line 186, in interact_with_prover_sequentially
    print('obs_after_action', prover.get_observation_string())
  File "/data/jychen/research/code/research_mono/neural_theorem_prover/wrapped_prover.py", line 25, in get_observation_string
    return self.inner.parser.observation_to_source(self.inner.get_observation())
  File "/data/jychen/research/code/third_party/INT/int_environment/proof_system/graph_seq_conversion.py", line 101, in observation_to_source
    source = source + logic_statement_to_seq_string(observation["objectives"][0])
IndexError: list index out of range