A Reality Check of Language Models as Formalizers on Constraint Satisfaction Problems
Di cosa parla
Si è provato a far tradurre ai modelli linguistici la descrizione di problemi con vincoli in programmi formali che un programma esterno esegue, per vedere se questo facilita la soluzione. Il risultato mostra che questa strada non semplifica il compito: spesso funziona peggio rispetto a far risolvere direttamente il modello, peggiora con la complessità e talvolta i modelli inseriscono passaggi simili a soluzioni preconfezionate che causano errori.
Cosa permette di osservare
Permette di esplorare se tradurre problemi in codice può offrire risultati più controllabili e spiegabili rispetto all'approccio diretto, e di capire quali ostacoli emergono quando i problemi diventano più complessi e i modelli tentano di imitare il ragionamento umano.
Dalla fonte
Recent work shows superior performance when using large language models (LLMs) as formalizers instead of as end-to-end solvers for symbolic reasoning problems. Given the problem description, the LLM generates a formal program that derives a solution via an external solver. We systematically investigate the formalization capability of LLMs on real-life constraint satisfaction problems on 4 benchmarks, 6 LLMs, and 2 types of formal languages. We show that LLM-as-formalizer by no means trivializes the problem but underperforms LLM-as-solver in 15 out of 24 model-dataset combinations, despite the former's verifiability and interpretability. Although the formalization space is magnitudes smaller than the search space, our scaling analysis shows that LLM-as-formalizer still drastically degrades as problem complexity increases similar to LLM-as-solver. To better understand this limitation, we…