연구자료실
설비 연결, 품질 검사, 생산 분석과 제조 업무에 관련된 외부 논문입니다.
연구자료 검색
논문 목록
T14. 산업용 프로토콜 번역, 코드 생성, 프로그램 합성
- T14-5구조대응2025년 이후
Training LLMs for Generating IEC 61131-3 Structured Text with Online Feedback
한국어 검토 보기
해결 문제
- IEC 61131-3 정형 텍스트는 공개 학습 데이터가 적다. 문법도 까다롭다. 그래서 일반 모델이 잘 못 쓴다.
핵심 구조
- 선호 기반 학습을 온라인으로 돌린다. 컴파일러 피드백과 LLM 기반 전문가 평가를 매 회 반영해 미세조정한다.
주요 결과
- 컴파일 성공률이 올라갔다. 기존 모델보다 나은 성능을 보고한다.
한계
- 컴파일 성공이 곧 현장 안전성은 아니다. 평가자 역할을 다른 LLM이 맡아 편향 가능성이 있다.
우리 기능과의 연결
- 회사 연결: 실행 결과를 다시 학습 신호로 넣는 구조는 설비 데이터 수집 드라이버 코드나 변환 규칙을 스스로 고쳐가는 방식에 대응할 수 있다.
- T14-3구조대응
LLM4PLC: Harnessing Large Language Models for Verifiable Programming of PLCs in Industrial Control Systems
한국어 검토 보기
해결 문제
- GPT-4나 LLaMa2를 그냥 쓰면 산업 제어용으로 쓸 수 있는 프로그램이 나오지 않는다.
핵심 구조
- 생성과 검증을 반복하는 파이프라인이다. 문법 검사기, 컴파일러, SMV 모델 검증기를 붙인다. 프롬프트 설계와 LoRA 미세조정을 함께 쓴다. LoRA는 모델 일부만 저비용으로 학습시키는 방법이다.
주요 결과
- 생성 성공률이 47퍼센트에서 72퍼센트로 올랐다. 전문가 설문 기준 코드 품질이 2.25점에서 7.75점(10점 만점)으로 올랐다. FischerTechnik 제조 실습 장비에서 실제로 돌려 확인했다.
한계
- 검증 도구가 존재하는 언어와 도메인에서만 성립한다. 실습 장비 규모라 대형 라인 검증은 아니다.
우리 기능과의 연결
- 회사 연결: 생성한 결과를 컴파일러와 검증기로 되먹여 고치는 구조는 AI 기준정보 생성과 AI 보고서의 자동 검증 단계에 대응할 수 있다.
- T14-10구조대응
Automated Attack Synthesis by Extracting Finite State Machines from Protocol Specification Documents
한국어 검토 보기
해결 문제
- 프로토콜 사양이 영어 산문(RFC 문서)으로만 있다. 이걸 사람이 상태 기계로 옮기면 오래 걸리고 논리 오류가 난다.
핵심 구조
- 세 단계 혼합 방식이다. 첫째, 기술 문서용 대규모 단어 표현 학습이다. 둘째, 사양 문장을 프로토콜과 무관한 중간 표현으로 옮기는 제로샷 학습이다. 셋째, 중간 표현을 특정 프로토콜의 상태 기계로 바꾸는 규칙 기반 변환이다.
주요 결과
- BGPv4, DCCP, LTP, PPTP, SCTP, TCP 여섯 개 프로토콜로 검증했다. TCP와 DCCP에서는 뽑아낸 상태 기계로 공격 시나리오 합성까지 자동화했다.
한계
- 규칙 기반 마지막 단계가 프로토콜마다 손이 간다. 문서가 애매하게 쓰인 부분은 복원이 어렵다.
우리 기능과의 연결
- 회사 연결: 사람이 읽는 사양 문서에서 기계가 쓰는 모델을 뽑아내는 구조라, 설비 매뉴얼과 규격서에서 기준정보와 수집 규칙을 만드는 작업에 대응할 수 있다.
- T14-11구조대응
Syntax-Guided Synthesis
한국어 검토 보기
해결 문제
- 프로그램 합성은 원래 "논리식으로 준 정확성 사양을 만족하는 프로그램을 찾아라"였다. 프로그램 합성은 사양만 주면 프로그램을 자동으로 만들어내는 기술이다. 그런데 찾을 공간이 너무 넓어 잘 안 풀린다.
핵심 구조
- 논리 사양에 더해 후보 프로그램의 모양을 문법으로 제한하는 문제 틀을 정의한다. 입력은 배경 이론, 만족해야 할 논리식, 후보 식의 집합을 정하는 문법 세 가지다. 출력은 그 문법이 허용하는 식 중 논리식을 만족하는 것이다.
주요 결과
- 흩어져 있던 여러 합성 연구를 하나의 표준 문제 정의로 묶었다. 이 정의를 바탕으로 표준 입력 형식, 벤치마크 모음, 해법 경진대회(SyGuS-COMP)가 만들어졌다. 공식 사이트는 https://www.sygus.org 다.
한계
- 문법을 사람이 잘 짜 줘야 한다. 문법이 너무 넓으면 안 풀리고 너무 좁으면 답이 아예 없다. 논리로 검증 가능한 이론 안에서만 성립한다.
우리 기능과의 연결
- 회사 연결: 이 분야의 표준 문제 정의 틀이다. 이 계열의 앞 고리는 13번 Combinatorial Sketching이다. 후보 공간을 문법으로 좁히고 사양을 만족하는 변환식을 찾는 구조라, 설비 태그와 코드 체계를 표준 기준정보로 바꾸는 변환 규칙 생성에 대응할 수 있다. 아래 12번 FlashFill이 이 틀의 대표 사례다.
- T14-12구조대응
Automating string processing in spreadsheets using input-output examples
한국어 검토 보기
해결 문제
- 일반 사용자가 표 안의 문자열 데이터를 정리하려면 프로그램을 짜야 한다. 그걸 못 하니 손으로 반복한다.
핵심 구조
- 제한된 정규식과 조건, 반복을 담은 작은 문자열 처리 언어를 설계한다. 입력과 출력 예시 몇 개만으로 그 언어의 프로그램을 합성하는 알고리즘을 제시한다.
주요 결과
- 사용자들이 어려워하는 다양한 문자열 변환 작업을 예시 몇 개로 자동화했다. 나중에 엑셀의 빠른 채우기 기능으로 제품화됐다.
한계
- 문자열 도메인에 한정된다. 예시가 애매하면 의도와 다른 프로그램이 나온다.
우리 기능과의 연결
- 회사 연결: 예시 몇 개로 변환 규칙을 만들어내는 구조라, 설비별 태그명과 코드 체계를 표준 기준정보로 바꾸는 AI 기준정보 생성에 대응할 수 있다.
- T14-13구조대응
Combinatorial Sketching for Finite Programs
한국어 검토 보기
해결 문제
- 프로그램 합성기는 그때까지 도메인별 규칙을 사람이 넣어줘야 돌았다. 규칙을 안 넣으면 후보 공간이 너무 넓어 못 푼다.
핵심 구조
- 스케치라는 방식을 쓴다. 프로그래머가 뼈대만 있는 부분 프로그램을 쓰고, 어려운 조각은 구멍(hole)으로 비워둔다. 원하는 동작은 따로 사양으로 준다. SKETCH 언어와 합성기가 구멍을 채운다. 채우는 방법은 도메인 규칙이 아니라 일반화된 불리언 만족성(SAT) 기반 조합 탐색이다. 해법 후보를 찾는 SAT 풀이기와 그 후보가 모든 입력에서 사양과 같은지 확인하는 SAT 풀이기를 짝지어 돌린다. 반례가 나오면 입력 집합에 넣고 다시 돈다.
주요 결과
- AES 암호 알고리즘의 효율적 구현을 합성했다. 가장 복잡한 부분을 합성기가 만들었고 약 한 시간 걸렸다. 유한 프로그램 부류에서는 원리상 항상 스케치를 완성할 수 있다고 밝힌다.
한계
- 유한 프로그램에 한정된다. 구멍의 자리와 모양을 사람이 잡아줘야 한다. 탐색 문제 자체가 계산량이 크다(2QBF).
우리 기능과의 연결
- 회사 연결: 골격과 구멍으로 후보 공간을 좁혀 합성하는 방식의 원조 논문이다. 위 11번 Syntax-Guided Synthesis가 이 계열을 하나의 표준 문제 정의로 묶었다. 변환 규칙의 틀을 사람이 잡고 빈칸만 기계가 채우는 구조라, 설비 태그를 표준 기준정보로 바꾸는 변환 규칙 생성에 대응할 수 있다.
검토 메모
- 참고: 논문 표지의 저자 순서는 Saraswat이 Seshia보다 앞이다. dblp는 Seshia를 앞에 적는다. 저자 다섯 명은 같다.
연구에서 제품 적용까지
운영 중인 기능, 시범 적용과 개발 중인 기술을 구분해 정리했습니다.
보유기술 보기