How are the declarations, constraints, queries, additional_constraints, queries_function generated?

[AyushSingh1722]

The preprocessing/ directory is explicitly ignored, which means the preprocessing code exists but wasn't included in the public release. The code is built upon Logic-LLM, but Logic-LLM generates only declarations, how you generated queries, additional_constraints and constraints?

Can you please push the preprocessing directory as well, so that we can understand the details.

[Hyun-Ryu]

Hi @AyushSingh1722,

For declarations and target sentences, I just use the output of Logic-LM.
When you look at the code of Logic-LM, they prompt a language model to generate target FOL formulas and their corresponding target NL sentences. The reason I explicitly ignore this preprocessing directory is that I did not clean the code yet :) I'll push the codes ASAP. If you have any other questions or issues, please let me know!

[AyushSingh1722]

Thanks for the quick reply! If I'm understanding right, you're using LogicLM for preprocessing—specifically, you're picking the declarations, constraints listed in natural language, and the satisfiability function selection from the LogicLM outputs, correct? Are the additional constraints also generated from LogicLM?

I also wanted some clarifications about the error types mentioned in your paper. In Figure 3, if you're indeed using LogicLM for preprocessing, why does CLOVER show slightly more preprocessing errors compared to LogicLM? Additionally, aside from syntax errors, how exactly are you distinguishing between logical errors, function selection errors, and preprocessing errors once the script (tmp.py) runs successfully?

[Hyun-Ryu]

Hi @AyushSingh1722,

For AR-LSAT, I simply picked declarations and constraints from Logic-LM outputs as you said. There are additional tricks to get queries, additional constraints, and SAT functions.

1. Prompt a LM to convert original question and 5 multiple choices into 5 declarative queries.
2. Prompt a LM to extract additional constraints from the original question. (As you can see in the AR-LSAT dataset, about 5-6 questions share the same context, and there are some cases where additional constraints exist in the question. That's why I introduce additional constraints here.)
3. Prompt a LM to predict SAT functions as I mentioned in Appendix E in the paper.

For other datasets, we don't need any of these additional tricks.

For your questions regarding error types, I can't remember how I did exactly at that time right now. I think I could look into the details and could answer your questions in a few days. Stay tuned!

[zhliang-work]

Hi, there. Any updates here?