GIL-Zaragoza at SemEval 2026 Task 11: Comparing Classification, Autoformalization, and Ontologies for Formal Reasoning Capabilities
Summary
The paper describes a team's entry to SemEval-2026 Task 11. The task checks whether models can judge if a syllogism is logically valid without being swayed by whether its content matches real-world knowledge. The team worked only on Subtask 1, which uses English syllogisms with no distractor premises, and compared three strategies:
- Supervised classification: TF-IDF features with classical classifiers, plus a fine-tuned BERT debiased with GroupDRO.
- Autoformalization: DPO-aligned Llama3 models translate each syllogism into first-order logic, and Prover9 checks the inference.
- Neuro-symbolic: GPT writes OWL 2 ontologies, which the HermiT reasoner evaluates.
The simplest method won. A Logistic Regression submission placed 40th out of 45 teams, scoring 72.25% on accuracy and 20.37 on the combined metric. The classical models were less sensitive to content than BERT. The symbolic pipelines were held back by poor translations, mismatches between generated logic and solver syntax, and error-prone serialization. The authors conclude that autoformalization is still a weak point for LLMs and that external solvers need robust syntax parsing. Lightweight classifiers remain useful because they show little content bias.
Key points
- Evaluation metric: the official ranking metric (PRM) combines Accuracy with Total Content Effect (TCE), which measures sensitivity to plausible versus implausible content. The best official run had a TCE of 11.77.
- Development results (80/20 split): Naive Bayes reached the highest PRM (32.61), ahead of Logistic Regression (31.96) and SVM (29.71). BERT with GroupDRO scored 21.92 because of its higher TCE (8.09).
- Autoformalization models: four DPO checkpoints trained on FOLIO were used (Kurosawama/Llama-3.1-8B/3.2-3B, vanilla and Instruct "LogLim"). Instruct variants made fewer errors.
- Autoformalization errors: the models produced XOR operators that Prover9 rejects, which excluded roughly 27% of answers for one checkpoint. They also sometimes dropped the conclusion entirely.
- Ontology approach: using gpt-4o-mini, it scored 48.69 accuracy, 27.08 TCE and 11.23 PRM. The authors blame limited prompt exploration and the verbose RDF/XML format required by OwlReady2.
Institutions
Cite
@inproceedings{lopezponce2026gil,
title = {{GIL-Zaragoza at SemEval 2026 Task 11: Comparing Classification, Autoformalization, and Ontologies for Formal Reasoning Capabilities}},
author = {Lopez-Ponce, Francisco and Pitarch, Lucia and Martínez, Iván Saavedra and Huitzil, Ignacio and Trueba, Sergio Ojeda and Bobillo, Fernando and Bel-Enguix, Gemma},
booktitle = {Proceedings of the 20th International Workshop on Semantic Evaluation (2026)},
year = {2026},
doi = {10.18653/v1/2026.semeval-1.308},
url = {https://doi.org/10.18653/v1/2026.semeval-1.308}
}References
- Marah Abdin, Jyoti Aneja, Harkirat Behl, Sébastien Bubeck, Ronen Eldan, Suriya Gunasekar, Michael Harrison, Russell J. Hewett, Mojan Javaheripi, Piero Kauffmann, James R. Lee, Yin Tat Lee, Yuanzhi Li, Weishung Liu, Caio C. T. Mendes, Anh Nguyen, Eric Price, Gustavo de Rosa, Olli Saarikivi, and 8 oth… find our card
- Mislav Balunović, Jasper Dekoninck, Ivo Petrov, Nikola Jovanović, and Martin Vechev. 2025. Matharena: Evaluating llms on uncontaminated math competitions. find
- Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, Christopher Hesse, and John Schulman. 2021. Training verifiers to solve math word problems. arXiv preprint arXiv:2110.14168. find our card
- Ishita Dasgupta, Andrew K. Lampinen, Stephanie C. Y. Chan, Hannah R. Sheahan, Antonia Creswell, Dharshan Kumaran, James L. McClelland, and Felix Hill. 2024. Language models show human-like content effects on reasoning tasks. Preprint, arXiv:2207.07051. find
- DeepSeek-AI. 2025. Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning. Preprint, arXiv:2501.12948. find our card
- DeepSeek-AI, Aixin Liu, Bei Feng, Bing Xue, Bingxuan Wang, Bochao Wu, Chengda Lu, Chenggang Zhao, Chengqi Deng, Chenyu Zhang, Chong Ruan, Damai Dai, Daya Guo, Dejian Yang, Deli Chen, Dongjie Ji, Erhang Li, Fangyun Lin, Fucong Dai, and 181 others. 2025. Deepseek-v3 technical report. Preprint, arXiv:2… find
- Aaron Grattafiori, Abhimanyu Dubey, Abhinav Jauhri, Abhinav Pandey, Abhishek Kadian, Ahmad Al-Dahle, Aiesha Letman, Akhil Mathur, Alan Schelten, Alex Vaughan, Amy Yang, Angela Fan, Anirudh Goyal, Anthony Hartshorn, Aobo Yang, Archi Mitra, Archie Sravankumar, Artem Korenev, Arthur Hinsvark, and 542 o… find
- Simeng Han, Hailey Schoelkopf, Yilun Zhao, Zhenting Qi, Martin Riddell, Wenfei Zhou, James Coady, David Peng, Yujie Qiao, Luke Benson, Lucy Sun, Alexander Wardle-Solano, Hannah Szabó, Ekaterina Zubova, Matthew Burtell, Jonathan Fan, Yixin Liu, Brian Wong, Malcolm Sailor, and 16 others. 2024. FOLIO:… find our card
- Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. 2021. Measuring mathematical problem solving with the math dataset. arXiv preprint arXiv:2103.03874. find our card
- Francisco F. López-Ponce and Gemma Bel-Enguix. 2025. Into the limits of logic: Alignment methods for formal logical reasoning. In Proceedings of The 3rd Workshop on Mathematical Natural Language Processing (MathNLP 2025), pages 112–123, Suzhou, China. Association for Computational Linguistics. find
- W. McCune. 2005–2010. Prover9 and mace4. http://www.cs.unm.edu/~mccune/prover9/. ↗
- OpenAI. 2025. gpt-oss-120b & gpt-oss-20b model card. Preprint, arXiv:2508.10925. find our card
- Liangming Pan, Alon Albalak, Xinyi Wang, and William Wang. 2023. Logic-LM: Empowering large language models with symbolic solvers for faithful logical reasoning. In Findings of the Association for Computational Linguistics: EMNLP 2023, pages 3806–3824, Singapore. Association for Computational Lingui… find our card
- Auguste Poiroux, Gail Weiss, Viktor Kunčak, and Antoine Bosselut. 2025. Reliable evaluation and benchmarks for statement autoformalization. In Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing, pages 17947–17969, Suzhou, China. Association for Computational Ling… find
- Xin Quan, Marco Valentino, Louise A. Dennis, and Andre Freitas. 2024. Verification and refinement of natural language explanations through LLM-symbolic theorem proving. In Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, pages 2933–2958, Miami, Florida, USA. As… find
- Rafael Rafailov, Archit Sharma, Eric Mitchell, Stefano Ermon, Christopher D. Manning, and Chelsea Finn. 2024. Direct preference optimization: Your language model is secretly a reward model. Preprint, arXiv:2305.18290. find our card
- Szegedy. 2022. Autoformalization with large language models. Preprint, arXiv:2205.12615. find our card
- Shunyu Yao, Dian Yu, Jeffrey Zhao, Izhak Shafran, Thomas L. Griffiths, Yuan Cao, and Karthik Narasimhan. 2023. Tree of thoughts: Deliberate problem solving with large language models. Preprint, arXiv:2305.10601. find
- Yang Yue, Zhiqi Chen, Rui Lu, Andrew Zhao, Zhaokai Wang, Yang Yue, Shiji Song, and Gao Huang. 2025. Does reinforcement learning really incentivize reasoning capacity in llms beyond the base model? arXiv preprint arXiv:2504.13837. find our card
This page in Markdown → https://md.research.elamur.ai/free/en/papers/ponce-2026-gil-zaragoza-semeval-2026-task/