명세로부터 코드의 정확성을 추론하는 방법

Inferring Code Correctness from Specification

대규모 언어 모델(LLM)은 현대 소프트웨어 개발에 필수적인 요소가 되었으며, 대규모 자동 코드 생성을 가능하게 합니다. 그러나 LLM이 생성한 코드의 정확성을 검증하는 것은 여전히 중요한 과제이며, 대부분 해결되지 않았습니다. 기존 방법들은 여러 후보 코드에 대한 동적 합의에 의존하여 비용이 많이 들고 확장하기 어렵거나, 정적 추론을 사용하지만 이는 실행 시 발생하는 오류나 순서 편향에 취약합니다. 본 논문에서는 TRAILS (Targeted Reasoning Agreement via Inputs and Specifications)라는 접근 방식을 제안합니다. TRAILS는 LLM의 추론을 구체적인 (입력, 출력) 쌍과 연결하여 수행합니다. TRAILS는 먼저 명세를 기반으로 범주 분할을 통해 다양한 테스트 입력을 생성하고, 이를 후보 코드에 실행한 다음, LLM에게 결과적으로 생성된 입력-출력 쌍이 명세와 일치하는지 평가하도록 요청합니다. 이때 LLM은 코드 자체를 추론하지 않습니다. 입력별 점수를 집계하여 프로그램의 정확성을 판단합니다. 우리는 TRAILS를 LiveCodeBench 및 CoCoClaNeL 두 데이터셋에서, Qwen3Coder-30B, Devstral-Small-24B 및 Olmo3.1-Instruct 세 개의 LLM을 사용하여 평가하고, HoarePrompt와 Zero-Shot Chain-of-Thought baseline과 비교했습니다. TRAILS는 Zero-Shot COT에 비해 Matthew Correlation Coefficient를 최대 39% 향상시켰으며, 일관적으로 HoarePrompt보다 성능이 우수했습니다. 정확성 외에도 TRAILS는 시드된 실행에서 더 큰 안정성을 보여주며, LLM의 비결정성에 대한 민감도를 줄이고, 경쟁적인 접근 방식보다 더 많은 고유한 코드 샘플에 대해 올바른 레이블을 할당합니다.

Large language models (LLMs) have become integral to modern software development, enabling automated code generation at scale. However, validating the correctness of LLM-generated code remains a critical and largely unsolved challenge. Existing approaches either rely on dynamic consensus across multiple code candidates - making them costly and difficult to scale - or on static reasoning that is susceptible to dynamic bugs and order bias. In this paper, we propose TRAILS~ (Targeted Reasoning Agreement via Inputs and Specifications), an approach that grounds LLM reasoning with concrete (input, output) pairs. TRAILS~ first generates diverse test inputs via category partitioning based on the specification, then executes them against the candidate code and prompts LLMs to assess whether the resulting input-output pairs conform to the specification - without ever reasoning over the code itself. Scores are aggregated across inputs, to determines whether the program is likely correct. We evaluate TRAILS~ on two datasets, LiveCodeBench and CoCoClaNeL, across three LLMs (Qwen3Coder-30B, Devstral-Small-24B, and Olmo3.1-Instruct), comparing against HoarePrompt and a Zero-Shot Chain-of-Thought baseline. TRAILS~ improves Matthew Correlation Coefficient by up to 39\% relative to Zero-Shot COT and consistently outperforms HoarePrompt. Beyond accuracy, TRAILS~ demonstrates greater stability across seeded runs, reducing sensitivity to LLM non-determinism, and assigns correct labels to a larger set of unique code samples than competing approaches.